diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-03-07 16:32:26 -0800 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-03-07 16:32:26 -0800 |
| commit | 03f658c3c702e805c89a5f10e5778ee4d8213d55 (patch) | |
| tree | 6ed6850c761df31e9e9153e4b547a334a02f3f70 /Source/Provers/SMTLib | |
| parent | 49fa63090f3b4d05e370f1e44606394c4d683c2e (diff) | |
added support for linear sets without useArrayTheory (but there is some incompletness)
Diffstat (limited to 'Source/Provers/SMTLib')
| -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;
|