added support for linear sets without useArrayTheory (but there is some incompletness)

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;