fixed vc generation so that even when builtin array functions are used,

the program can be verified without the use of /useArrayTheory

1 files changed, 9 insertions, 0 deletions

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;