partial fixes to these regressions

32 files changed, 82 insertions, 21 deletions

diff --git a/Test/z3api/Boog24.bpl b/Test/z3api/Boog24.bpl
index c5e2eea6..d3da775d 100644
--- a/Test/z3api/Boog24.bpl
+++ b/Test/z3api/Boog24.bpl
@@ -1,3 +1,4 @@
+type ref;

  

 function LIFT(a:bool) returns (int);

 axiom(forall a:bool :: {LIFT(a)} a <==> LIFT(a) != 0);

diff --git a/Test/z3api/boog0.bpl b/Test/z3api/boog0.bpl
index 1b9bee36..4206152b 100644
--- a/Test/z3api/boog0.bpl
+++ b/Test/z3api/boog0.bpl
@@ -1,3 +1,4 @@
+type ref;

 type Wicket;

 const w: Wicket;

 var favorite: Wicket;

@@ -6,7 +7,7 @@ function age(Wicket) returns (int);
 axiom age(w)==7;

 

 procedure NewFavorite(p: Wicket);

-  modifies favorite
;

+  modifies favorite;

 

   ensures favorite==p;

 

@@ -19,7 +20,7 @@ const myRef: ref;
 const v: Wicket;

 

 axiom 7 < 8;

-axiom 7 <= 8;


+axiom 7 <= 8;

 axiom 8 > 7;

 axiom 8 >= 7;

 axiom 6 != 7;

@@ -37,7 +38,7 @@ axiom ((7==7) && (8==8));
 

 var favorite2: Wicket;

 procedure SwapFavorites() 

-  modifies favorite,favorite2
;

+  modifies favorite,favorite2;

 

   ensures (favorite==old(favorite2)) && (favorite2==old(favorite));

 {

diff --git a/Test/z3api/boog1.bpl b/Test/z3api/boog1.bpl
index 6b6cce75..9f4d2349 100644
--- a/Test/z3api/boog1.bpl
+++ b/Test/z3api/boog1.bpl
@@ -1,3 +1,4 @@
+type ref;

 type Wicket;

 const w: Wicket;

 var favorite: Wicket;

@@ -7,7 +8,8 @@ function age(Wicket) returns (int);
 axiom age(w)==7;

 

 procedure NewFavorite(p: Wicket);

-  modifies favorite
;

+  modifies favorite

+;

 

   ensures favorite==p;

 

diff --git a/Test/z3api/boog10.bpl b/Test/z3api/boog10.bpl
index 5ac43287..075432d7 100644
--- a/Test/z3api/boog10.bpl
+++ b/Test/z3api/boog10.bpl
@@ -1,3 +1,4 @@
+type ref;

 // types

 type Color;

 const unique red: Color;

@@ -9,7 +10,8 @@ var myColor: Color;
 

 // procedure

 procedure SetTo(c: Color);

-  modifies myColor
;

+  modifies myColor

+;

 

   ensures myColor==c;

 

diff --git a/Test/z3api/boog11.bpl b/Test/z3api/boog11.bpl
index e66802ea..5b83de6a 100644
--- a/Test/z3api/boog11.bpl
+++ b/Test/z3api/boog11.bpl
@@ -1,10 +1,12 @@
+type ref;

 // types

 const top: ref;

 var myRef: ref;

 

 // procedure

 procedure SetTo(r: ref);

-  modifies myRef
;

+  modifies myRef

+;

 

   ensures myRef==r;

 

diff --git a/Test/z3api/boog12.bpl b/Test/z3api/boog12.bpl
index d20a8f35..c277a674 100644
--- a/Test/z3api/boog12.bpl
+++ b/Test/z3api/boog12.bpl
@@ -1,3 +1,4 @@
+type ref;

 // types

 type Color;

 const blue: Color;

@@ -7,7 +8,8 @@ var myMatrix:[int,int] Color;
 

 // procedure

 procedure SetTo(c: Color);

-  modifies myArray, myMatrix
;

+  modifies myArray, myMatrix

+;

 

   ensures myArray[0]==c;

 

diff --git a/Test/z3api/boog13.bpl b/Test/z3api/boog13.bpl
index a4f854f5..9cd873c6 100644
--- a/Test/z3api/boog13.bpl
+++ b/Test/z3api/boog13.bpl
@@ -1,3 +1,4 @@
+type ref;

 // types

 type Wicket;

 var favorite: Wicket;

@@ -6,14 +7,16 @@ var v: Wicket;
 function age(w:Wicket) returns (int);

 

 axiom (exists v:Wicket :: age(v)<8 && 

-          (forall v:Wicket
 :: age(v)==7) 

+          (forall v:Wicket

+ :: age(v)==7) 

 

       );

 

 

 // procedure

 procedure SetToSeven(p: Wicket);

-  modifies favorite
;

+  modifies favorite

+;

 

   ensures favorite==p;

 

diff --git a/Test/z3api/boog14.bpl b/Test/z3api/boog14.bpl
index c163ed18..41450d85 100644
--- a/Test/z3api/boog14.bpl
+++ b/Test/z3api/boog14.bpl
@@ -1,3 +1,4 @@
+type ref;

 function choose(a:bool, b:int, c:int) returns (x:int);

 axiom(forall a:bool, b:int, c:int :: {choose(a,b,c)} a ==> choose(a,b,c) == b);

 

diff --git a/Test/z3api/boog15.bpl b/Test/z3api/boog15.bpl
index ef792b2b..428c0f6e 100644
--- a/Test/z3api/boog15.bpl
+++ b/Test/z3api/boog15.bpl
@@ -1,3 +1,4 @@
+type ref;

 function AtLeast(int, int) returns ([int]bool);

 axiom(forall n:int, x:int :: {AtLeast(n,x)} AtLeast(n,x)[x]);

 

diff --git a/Test/z3api/boog16.bpl b/Test/z3api/boog16.bpl
index 48afd41d..a002c166 100644
--- a/Test/z3api/boog16.bpl
+++ b/Test/z3api/boog16.bpl
@@ -1,3 +1,4 @@
+type ref;

 function choose(a:bool, b:int, c:int) returns (x:int);

 axiom(forall a:bool, b:int, c:int :: 

   {choose(a,b,c)} !a ==> choose(a,b,c) == c);

diff --git a/Test/z3api/boog17.bpl b/Test/z3api/boog17.bpl
index 6f886f49..89159af1 100644
--- a/Test/z3api/boog17.bpl
+++ b/Test/z3api/boog17.bpl
@@ -1,3 +1,5 @@
+type name;

+type ref;

 const unique g : int;

 axiom(g != 0);

 

diff --git a/Test/z3api/boog18.bpl b/Test/z3api/boog18.bpl
index fe0cbc10..35f7d48a 100644
--- a/Test/z3api/boog18.bpl
+++ b/Test/z3api/boog18.bpl
@@ -1,3 +1,4 @@
+type ref;

 const A100INT4_name:int;

 

 function Match(a:int, t:int) returns (int);

diff --git a/Test/z3api/boog19.bpl b/Test/z3api/boog19.bpl
index 17b199dd..178bb04f 100644
--- a/Test/z3api/boog19.bpl
+++ b/Test/z3api/boog19.bpl
@@ -1,3 +1,5 @@
+type name;

+type ref;

 var alloc:[int]name;

 

 

diff --git a/Test/z3api/boog2.bpl b/Test/z3api/boog2.bpl
index 74c05a28..315c51af 100644
--- a/Test/z3api/boog2.bpl
+++ b/Test/z3api/boog2.bpl
@@ -1,10 +1,12 @@
+type ref;

 type Wicket;

 

 var favorite: Wicket;

 var hate: Wicket;

 

 procedure NewFavorite(p: Wicket);

-  modifies favorite
;

+  modifies favorite

+;

 

   ensures favorite==p;

 

diff --git a/Test/z3api/boog20.bpl b/Test/z3api/boog20.bpl
index fa714972..10181400 100644
--- a/Test/z3api/boog20.bpl
+++ b/Test/z3api/boog20.bpl
@@ -1,3 +1,4 @@
+type ref;

 

 function PLUS(int, int, int) returns (int);

 function Rep(int, int) returns (int);

diff --git a/Test/z3api/boog21.bpl b/Test/z3api/boog21.bpl
index 1f4fa6dc..8e3abde7 100644
--- a/Test/z3api/boog21.bpl
+++ b/Test/z3api/boog21.bpl
@@ -1,3 +1,4 @@
+type ref;

 

 function PLUS(int, int, int) returns (int);

 function Rep(int,int) returns (int);

@@ -5,7 +6,8 @@ function Rep(int,int) returns (int);
 

 // ERROR

 

-axiom(forall a:int, b:int, z:int :: Rep(a,b) == PLUS(a,b,z
));

+axiom(forall a:int, b:int, z:int :: Rep(a,b) == PLUS(a,b,z

+));

 axiom(forall n:int, x:int :: {Rep(n,x)} (exists k:int :: Rep(n,x) == x));

 // END ERROR

 

diff --git a/Test/z3api/boog22.bpl b/Test/z3api/boog22.bpl
index 95e45849..c255a3c5 100644
--- a/Test/z3api/boog22.bpl
+++ b/Test/z3api/boog22.bpl
@@ -1,3 +1,4 @@
+type ref;

 type W;

 

 function f1(W,int) returns (int);

diff --git a/Test/z3api/boog23.bpl b/Test/z3api/boog23.bpl
index 41c68790..4e0fc4d0 100644
--- a/Test/z3api/boog23.bpl
+++ b/Test/z3api/boog23.bpl
@@ -1,3 +1,5 @@
+type name;

+type ref;

 type byte;

 function OneByteToInt(byte) returns (int);

 function TwoBytesToInt(byte, byte) returns (int);

diff --git a/Test/z3api/boog25.bpl b/Test/z3api/boog25.bpl
index 0a8b5e92..0ee4163c 100644
--- a/Test/z3api/boog25.bpl
+++ b/Test/z3api/boog25.bpl
@@ -1,3 +1,5 @@
+type name;

+type ref;

 type byte;

 function OneByteToInt(byte) returns (int);

 function TwoBytesToInt(byte, byte) returns (int);

diff --git a/Test/z3api/boog28.bpl b/Test/z3api/boog28.bpl
index 989dbf75..ab7f4ad2 100644
--- a/Test/z3api/boog28.bpl
+++ b/Test/z3api/boog28.bpl
@@ -1,3 +1,4 @@
+type ref;

  

 function LIFT(x:bool) returns (int);

 axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0);

diff --git a/Test/z3api/boog29.bpl b/Test/z3api/boog29.bpl
index 8a97944d..035e69fd 100644
--- a/Test/z3api/boog29.bpl
+++ b/Test/z3api/boog29.bpl
@@ -1,3 +1,4 @@
+type ref;

 

 function LIFT(x:bool) returns (int);

 axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0);

diff --git a/Test/z3api/boog3.bpl b/Test/z3api/boog3.bpl
index 9e04ac5b..207ddbd0 100644
--- a/Test/z3api/boog3.bpl
+++ b/Test/z3api/boog3.bpl
@@ -1,3 +1,4 @@
+type ref;

 type Wicket;

 

 procedure Dummy();

diff --git a/Test/z3api/boog30.bpl b/Test/z3api/boog30.bpl
index ae682156..81e04f20 100644
--- a/Test/z3api/boog30.bpl
+++ b/Test/z3api/boog30.bpl
@@ -1,3 +1,4 @@
+type ref;

 

 function LIFT(x:bool) returns (int);

 axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0);

diff --git a/Test/z3api/boog31.bpl b/Test/z3api/boog31.bpl
index 219effce..86386a90 100644
--- a/Test/z3api/boog31.bpl
+++ b/Test/z3api/boog31.bpl
@@ -1,3 +1,4 @@
+type ref;

 

 const b1:bool;

 const b2:bool;

diff --git a/Test/z3api/boog34.bpl b/Test/z3api/boog34.bpl
index 62e7e82b..88a587aa 100644
--- a/Test/z3api/boog34.bpl
+++ b/Test/z3api/boog34.bpl
@@ -1,3 +1,4 @@
+type ref;

 

 function Rep(int, int) returns (int);

 axiom(forall n:int, x:int :: {Rep(n,x)} 

diff --git a/Test/z3api/boog4.bpl b/Test/z3api/boog4.bpl
index 46eda549..95ec7011 100644
--- a/Test/z3api/boog4.bpl
+++ b/Test/z3api/boog4.bpl
@@ -1,3 +1,4 @@
+type ref;

 type Wicket;

 

 const w: Wicket;

@@ -10,7 +11,8 @@ function age(Wicket) returns (int);
 

 axiom age(w)==7;

 axiom 7 < 8;

-axiom 7 <= 8;


+axiom 7 <= 8;

+

 axiom 8 > 7;

 axiom 8 >= 7;

 axiom 6 != 7;

@@ -28,7 +30,8 @@ axiom 7!=7;
 

 

 procedure NewFavorite(p: Wicket);

-  modifies favorite
;

+  modifies favorite

+;

 

   ensures favorite==p;

 

diff --git a/Test/z3api/boog5.bpl b/Test/z3api/boog5.bpl
index 0db94bba..4b76fd22 100644
--- a/Test/z3api/boog5.bpl
+++ b/Test/z3api/boog5.bpl
@@ -1,3 +1,4 @@
+type ref;

 // types

 type Wicket;

 

@@ -23,7 +24,8 @@ axiom age(x)==4;
 

 // procedure

 procedure SetToSeven(p: Wicket);

-  modifies favorite
;

+  modifies favorite

+;

 

   ensures favorite==p;

 

@@ -32,7 +34,8 @@ implementation SetToSeven(l: Wicket) {
     favorite:=l;

   } else {

     favorite:=v;

-  }


+  }

+

 

 }

 

diff --git a/Test/z3api/boog6.bpl b/Test/z3api/boog6.bpl
index 55c1dc7e..f6c3c23f 100644
--- a/Test/z3api/boog6.bpl
+++ b/Test/z3api/boog6.bpl
@@ -1,3 +1,4 @@
+type ref;

 // types

 type Wicket;

 

@@ -10,7 +11,8 @@ axiom b==true;
 

 // procedure

 procedure SetToSeven(p: Wicket);

-  modifies favorite
;

+  modifies favorite

+;

 

   ensures favorite==p;

 

diff --git a/Test/z3api/boog7.bpl b/Test/z3api/boog7.bpl
index 36f952d1..78e5e3e6 100644
--- a/Test/z3api/boog7.bpl
+++ b/Test/z3api/boog7.bpl
@@ -1,3 +1,4 @@
+type ref;

 // consts

 const w: int;

 

@@ -7,7 +8,8 @@ var favorite: int;
 

 // procedure

 procedure SetToSeven(p: int);

-  modifies favorite
;

+  modifies favorite

+;

 

   ensures favorite==p;

 

diff --git a/Test/z3api/boog8.bpl b/Test/z3api/boog8.bpl
index 0ac4f163..121f27cf 100644
--- a/Test/z3api/boog8.bpl
+++ b/Test/z3api/boog8.bpl
@@ -1,3 +1,4 @@
+type ref;

 // types

 type Wicket;

 var favorite: Wicket;

@@ -12,7 +13,8 @@ axiom myBool==true;
 

 // procedure

 procedure SetToSeven(p: Wicket);

-  modifies favorite
;

+  modifies favorite

+;

 

   ensures favorite==p;

 

diff --git a/Test/z3api/boog9.bpl b/Test/z3api/boog9.bpl
index 55897a1d..3bd6ff63 100644
--- a/Test/z3api/boog9.bpl
+++ b/Test/z3api/boog9.bpl
@@ -1,3 +1,4 @@
+type ref;

 // types

 type Wicket;

 var favorite: Wicket;

@@ -9,7 +10,8 @@ axiom (exists v:Wicket :: age(v)<8);
 

 // procedure

 procedure SetToSeven(p: Wicket);

-  modifies favorite
;

+  modifies favorite

+;

 

   ensures favorite==p;

 

diff --git a/Test/z3api/runtest.bat b/Test/z3api/runtest.bat
index 5daa36c0..08a27b9b 100644
--- a/Test/z3api/runtest.bat
+++ b/Test/z3api/runtest.bat
@@ -3,8 +3,18 @@ setlocal
 

 set BGEXE=..\..\Binaries\Boogie.exe

 

-for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog12.bpl boog13.bpl boog14.bpl boog15.bpl boog16.bpl boog17.bpl boog18.bpl boog19.bpl boog20.bpl boog21.bpl boog22.bpl boog23.bpl boog24.bpl boog25.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do (

+for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog9.bpl boog10.bpl boog11.bpl boog13.bpl boog18.bpl boog20.bpl boog21.bpl boog22.bpl boog24.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do (

   echo.

   echo -------------------- %%f --------------------

-  %BGEXE% %* /nologo /prover:z3api %%f

+  %BGEXE% %* /nologo /typeEncoding:m /prover:z3api %%f

 )

+REM boog8.bpl

+REM boog12.bpl

+REM boog14.bpl

+REM boog15.bpl

+REM boog16.bpl

+REM boog17.bpl

+

+REM boog19.bpl

+REM boog23.bpl

+REM boog25.bpl
\ No newline at end of file