diff options
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index cf125c76..da73dea1 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -709,15 +709,19 @@ namespace Microsoft.Boogie.SMTLib var builtin = ExtractBuiltin(op.Func);
var datatype = ExtractDatatype(op.Func);
if (builtin != null)
- printedName = builtin;
+ {
+ printedName = CheckMapApply(builtin, node);
+ }
else if (datatype != null)
- printedName = datatype;
+ {
+ printedName = datatype;
+ }
else
- printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);
+ {
+ printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);
+ }
Contract.Assert(printedName != null);
- printedName = CheckMapApply(printedName, node);
-
WriteApplication(printedName, node, options);
return true;
|