diff options
author | qadeer <unknown> | 2013-12-28 08:56:24 -0800 |
---|---|---|
committer | qadeer <unknown> | 2013-12-28 08:56:24 -0800 |
commit | 97d289bddf594c2d363e589a2370a6140e8bcee5 (patch) | |
tree | b97d7426ff00c30718f9978914ebc9cbef316467 /Source/Provers | |
parent | 40b2941e5dd2a06b5da146bc7a72472e5a3b6eba (diff) |
fixed vc generation so that even when builtin array functions are used,
the program can be verified without the use of /useArrayTheory
Diffstat (limited to 'Source/Provers')
-rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 9 |
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;
|