diff options
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
| -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;
|