From 97d289bddf594c2d363e589a2370a6140e8bcee5 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Sat, 28 Dec 2013 08:56:24 -0800
Subject: fixed vc generation so that even when builtin array functions are
 used, the program can be verified without the use of /useArrayTheory

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

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

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 1f4b6a7f..1bea4633 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -166,6 +166,12 @@ namespace Microsoft.Boogie.SMTLib
       if (retVal == null) {
         retVal = f.FindStringAttribute("builtin");
       }
+
+      if (retVal != null && !CommandLineOptions.Clo.UseArrayTheory && SMTLibOpLineariser.ArrayOps.Contains(retVal))
+      {
+          retVal = null;
+      }
+
       return retVal;
     }
 
@@ -743,6 +749,9 @@ namespace Microsoft.Boogie.SMTLib
         }
       }
 
+      public static HashSet<string> ArrayOps = new HashSet<string>(new string[] { 
+          "MapConst", "MapAdd", "MapSub", "MapMul", "MapDiv", "MapMod", "MapEq", "MapIff", "MapGt", "MapGe", "MapLt", "MapLe", "MapOr", "MapAnd", "MapNot", "MapImp", "MapIte" });
+
       private static string CheckMapApply(string name, VCExprNAry node) {
         if (name == "MapConst") {
           Type type = node.Type;
-- 
cgit v1.2.3