diff options
author | qadeer <unknown> | 2010-04-19 03:52:43 +0000 |
---|---|---|
committer | qadeer <unknown> | 2010-04-19 03:52:43 +0000 |
commit | e6e2ac05b16701ed0f033b468b00a1b026c49f74 (patch) | |
tree | b8441348dd3559b2419b1c37765e1bafa344fd8d /Source/Provers/Z3/Prover.ssc | |
parent | 65515f184fb181b4e6a3286f505607efde228633 (diff) |
1. Fixed an off-by-one error in parsing array partitions in Z3 models
2. Added code for printing array partitions
3. Set UseAbstractInterpretation=false in case lazy inlining is being used
Diffstat (limited to 'Source/Provers/Z3/Prover.ssc')
-rw-r--r-- | Source/Provers/Z3/Prover.ssc | 14 |
1 files changed, 13 insertions, 1 deletions
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 + "");
}
|