diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 1 | ||||
| -rw-r--r-- | Source/Provers/Z3/Prover.ssc | 14 |
2 files changed, 14 insertions, 1 deletions
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index e3b5293f..bab1d04b 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -1306,6 +1306,7 @@ namespace Microsoft.Boogie PrintErrorModel = 1;
TypeEncodingMethod = TypeEncoding.Monomorphic;
UseArrayTheory = true;
+ UseAbstractInterpretation = false;
}
}
diff --git a/Source/Provers/Z3/Prover.ssc b/Source/Provers/Z3/Prover.ssc index eb09576b..1da24532 100644 --- a/Source/Provers/Z3/Prover.ssc +++ b/Source/Provers/Z3/Prover.ssc @@ -444,7 +444,7 @@ namespace Microsoft.Boogie.Z3 } else if (s[j] == '{') {
// array
List<List<int>!> arrayModel = new List<List<int>!>();
- string array = s.Substring(j);
+ string array = s.Substring(j+1);
int index1, index2;
string from, to;
List<int> tuple = new List<int>();
@@ -851,6 +851,18 @@ namespace Microsoft.Boogie.Z3 writer.Write(" -> " + "false" + "");
} else if (tempPTVI is BigNum) {
writer.Write(" -> " + tempPTVI + ":int");
+ } else if (tempPTVI is List<List<int>!>) {
+ List<List<int>!> array = tempPTVI as List<List<int>!>;
+ assume array != null;
+ writer.Write(" -> {");
+ foreach(List<int> l in array) {
+ if (l.Count == 2) {
+ writer.Write("*"+l[0] + " -> " + "*"+l[1] + "; ");
+ } else {
+ assert (l.Count == 1);
+ writer.Write("else -> *"+l[0]+"}");
+ }
+ }
} else {
writer.Write(" -> " + tempPTVI + "");
}
|