From 03f658c3c702e805c89a5f10e5778ee4d8213d55 Mon Sep 17 00:00:00 2001
From: Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>
Date: Thu, 7 Mar 2013 16:32:26 -0800
Subject: added support for linear sets without useArrayTheory (but there is
 some incompletness)

---
 Source/Provers/SMTLib/SMTLibLineariser.cs | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

(limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')

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;
-- 
cgit v1.2.3