Merge

3 files changed, 108 insertions, 172 deletions

diff --git a/Test/extractloops/runtest.bat b/Test/extractloops/runtest.bat
index 84422acd..4fbed727 100644
--- a/Test/extractloops/runtest.bat
+++ b/Test/extractloops/runtest.bat
@@ -5,15 +5,15 @@ set BGEXE=..\..\Binaries\Boogie.exe
 rem set BGEXE=mono ..\..\Binaries\Boogie.exe

 

 echo ----- Running regression test t1.bpl

-%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 t1.bpl

+%BGEXE% %* /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 t1.bpl

 echo -----

 echo ----- Running regression test t2.bpl

-%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 t2.bpl

+%BGEXE% %* /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 t2.bpl

 echo -----

 echo ----- Running regression test t3.bpl with recursion bound 2

-%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /recursionBound:2 t3.bpl

+%BGEXE% %* /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /recursionBound:2 t3.bpl

 echo -----

 echo ----- Running regression test t3.bpl with recursion bound 4

-%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /recursionBound:4 t3.bpl

+%BGEXE% %* /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /recursionBound:4 t3.bpl

 echo -----

 

diff --git a/Test/stratifiedinline/runtest.bat b/Test/stratifiedinline/runtest.bat
index 2bb3cbd5..d260708b 100644
--- a/Test/stratifiedinline/runtest.bat
+++ b/Test/stratifiedinline/runtest.bat
@@ -5,33 +5,33 @@ set BGEXE=..\..\Binaries\Boogie.exe
 rem set BGEXE=mono ..\..\Binaries\Boogie.exe

 

 echo ----- Running regression test bar1.bpl

-%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar1.bpl

+%BGEXE% %* /stratifiedInline:1 bar1.bpl

 echo -----

 echo ----- Running regression test bar2.bpl

-%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar2.bpl

+%BGEXE% %* /stratifiedInline:1 bar2.bpl

 echo -----

 echo ----- Running regression test bar3.bpl

-%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar3.bpl

+%BGEXE% %* /stratifiedInline:1 bar3.bpl

 echo -----

 echo ----- Running regression test bar4.bpl

-%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar4.bpl

+%BGEXE% %* /stratifiedInline:1 bar4.bpl

 echo -----

 echo ----- Running regression test bar6.bpl

-%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar6.bpl

+%BGEXE% %* /stratifiedInline:1 bar6.bpl

 echo -----

 echo ----- Running regression test bar7.bpl

-%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /nonUniformUnfolding bar7.bpl

+%BGEXE% %* /stratifiedInline:1 /nonUniformUnfolding bar7.bpl

 echo -----

 echo ----- Running regression test bar8.bpl

-%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /nonUniformUnfolding bar8.bpl

+%BGEXE% %* /stratifiedInline:1 /nonUniformUnfolding bar8.bpl

 echo -----

 echo ----- Running regression test bar9.bpl

-%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /nonUniformUnfolding bar9.bpl

+%BGEXE% %* /stratifiedInline:1 /nonUniformUnfolding bar9.bpl

 echo -----

 echo ----- Running regression test bar10.bpl

-%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 /nonUniformUnfolding bar10.bpl

+%BGEXE% %* /stratifiedInline:1 /nonUniformUnfolding bar10.bpl

 echo -----

 echo ----- Running regression test bar11.bpl

-%BGEXE% %* /noinfer /doNotUseLabels /stratifiedInline:1 bar11.bpl

+%BGEXE% %* /stratifiedInline:1 bar11.bpl

 echo -----

 

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 4e3886aa..56c247c2 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -1,51 +1,30 @@
 

 -------------------- NullInModel --------------------

-Z3 error model: 

-partitions:

-*0 {%lbl%+24 %lbl%+37} -> true

-*1 {%lbl%@47} -> false

-*2 {s null} 

-*3 {refType} 

-*4 {intType} 

-*5 {boolType} 

-*6 -> 0:int

-*7 -> 1:int

-*8 -> 2:int

-*9 

-function interpretations:

+*** MODEL

+s -> T@U!val!0

+%lbl%+24 -> true

+%lbl%@47 -> false

+refType -> T@T!val!2

+intType -> T@T!val!0

+%lbl%+37 -> true

+boolType -> T@T!val!1

+null -> T@U!val!0

 tickleBool -> {

-  *0 -> *0

-  *1 -> *0

-  else -> #unspecified

+  true -> true

+  false -> true

+  else -> true

 }

 type -> {

-  *2 -> *3

-  else -> #unspecified

+  T@U!val!0 -> T@T!val!2

+  else -> T@T!val!2

 }

 Ctor -> {

-  *4 -> *6

-  *5 -> *7

-  *3 -> *8

-  else -> #unspecified

+  T@T!val!0 -> 0

+  T@T!val!1 -> 1

+  T@T!val!2 -> 2

+  else -> 0

 }

-END_OF_MODEL

-.

-identifierToPartition:

-%lbl%+24 : *0

-%lbl%+37 : *0

-%lbl%@47 : *1

-s : *2

-null : *2

-refType : *3

-intType : *4

-boolType : *5

-valueToPartition:

-True : *0

-False : *1

-0 : *6

-1 : *7

-2 : *8

-End of model.

+*** END_MODEL

 NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.

 Execution trace:

     NullInModel.bpl(2,3): anon0

@@ -53,41 +32,24 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- IntInModel --------------------

-Z3 error model: 

-partitions:

-*0 {%lbl%+29 %lbl%+23} -> true

-*1 {%lbl%@39} -> false

-*2 {intType} 

-*3 {boolType} 

-*4 {i} -> 0:int

-*5 -> 1:int

-*6 

-function interpretations:

+*** MODEL

+intType -> T@T!val!0

+boolType -> T@T!val!1

+%lbl%+29 -> true

+%lbl%+23 -> true

+i -> 0

+%lbl%@39 -> false

 tickleBool -> {

-  *0 -> *0

-  *1 -> *0

-  else -> #unspecified

+  true -> true

+  false -> true

+  else -> true

 }

 Ctor -> {

-  *2 -> *4

-  *3 -> *5

-  else -> #unspecified

+  T@T!val!0 -> 0

+  T@T!val!1 -> 1

+  else -> 0

 }

-END_OF_MODEL

-.

-identifierToPartition:

-%lbl%+29 : *0

-%lbl%+23 : *0

-%lbl%@39 : *1

-intType : *2

-boolType : *3

-i : *4

-valueToPartition:

-True : *0

-False : *1

-0 : *4

-1 : *5

-End of model.

+*** END_MODEL

 IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.

 Execution trace:

     IntInModel.bpl(2,3): anon0

@@ -95,62 +57,36 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- ModelTest --------------------

-Z3 error model: 

-partitions:

-*0 {%lbl%+64 %lbl%+119} -> true

-*1 {%lbl%@182} -> false

-*2 {s} 

-*3 {j@2} -> 4:int

-*4 {boolType} 

-*5 {intType} 

-*6 {refType} 

-*7 {i@0} -> 1:int

-*8 {j@0} -> 2:int

-*9 {j@1} -> 3:int

-*10 {r} 

-*11 -> 0:int

-*12 

-function interpretations:

+*** MODEL

+%lbl%+64 -> true

+s -> T@U!val!0

+j@2 -> 4

+%lbl%+119 -> true

+boolType -> T@T!val!1

+intType -> T@T!val!0

+refType -> T@T!val!2

+%lbl%@182 -> false

+i@0 -> 1

+j@0 -> 2

+j@1 -> 3

+r -> T@U!val!1

 tickleBool -> {

-  *0 -> *0

-  *1 -> *0

-  else -> #unspecified

+  true -> true

+  false -> true

+  else -> true

 }

 type -> {

-  *2 -> *6

-  *10 -> *6

-  else -> #unspecified

+  T@U!val!0 -> T@T!val!2

+  T@U!val!1 -> T@T!val!2

+  else -> T@T!val!2

 }

 Ctor -> {

-  *5 -> *11

-  *4 -> *7

-  *6 -> *8

-  else -> #unspecified

+  T@T!val!0 -> 0

+  T@T!val!1 -> 1

+  T@T!val!2 -> 2

+  else -> 0

 }

-END_OF_MODEL

-.

-identifierToPartition:

-%lbl%+64 : *0

-%lbl%+119 : *0

-%lbl%@182 : *1

-s : *2

-j@2 : *3

-boolType : *4

-intType : *5

-refType : *6

-i@0 : *7

-j@0 : *8

-j@1 : *9

-r : *10

-valueToPartition:

-True : *0

-False : *1

-4 : *3

-1 : *7

-2 : *8

-3 : *9

-0 : *11

-End of model.

+*** END_MODEL

 ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.

 Execution trace:

     ModelTest.bpl(3,5): anon0

@@ -178,22 +114,22 @@ Execution trace:
     CaptureState.bpl(16,5): anon4_Then

     CaptureState.bpl(24,5): anon3

 *** MODEL

+m@3 -> -1

+this -> T@U!val!1

+intType -> T@T!val!0

 %lbl%+112 -> true

+Heap -> T@U!val!0

 %lbl%+116 -> true

 %lbl%+110 -> true

-%lbl%+189 -> true

-%lbl%@334 -> false

-m@3 -> -1

-m@2 -> -1

-this -> *3

-intType -> *4

-Heap -> *5

-FieldNameType -> *6

+FieldNameType -> T@T!val!3

 m@0 -> -2

+m@2 -> -1

 r@0 -> -2

-boolType -> *8

-RefType -> *9

-F -> *10

+boolType -> T@T!val!1

+%lbl%@334 -> false

+%lbl%+189 -> true

+RefType -> T@T!val!2

+F -> T@U!val!2

 @MV_state_const -> 6

 x@@4 -> 797

 y@@1 -> **y@@1

@@ -205,18 +141,18 @@ tickleBool -> {
   else -> true

 }

 type -> {

-  *5 -> *13

-  *3 -> *9

-  *10 -> *6

-  -2 -> *4

-  else -> *13

+  T@U!val!0 -> T@T!val!4

+  T@U!val!1 -> T@T!val!2

+  T@U!val!2 -> T@T!val!3

+  T@U!val!3 -> T@T!val!0

+  else -> T@T!val!4

 }

 Ctor -> {

-  *4 -> 0

-  *8 -> 1

-  *9 -> 3

-  *6 -> 4

-  *13 -> 2

+  T@T!val!0 -> 0

+  T@T!val!1 -> 1

+  T@T!val!2 -> 3

+  T@T!val!3 -> 4

+  T@T!val!4 -> 2

   else -> 0

 }

 @MV_state -> {

@@ -226,37 +162,37 @@ Ctor -> {
   6 5 -> true

   else -> true

 }

-[3] -> {

-  *5 *3 *10 -> -2

-  else -> -2

+MapType0Select -> {

+  T@U!val!0 T@U!val!1 T@U!val!2 -> T@U!val!3

+  else -> T@U!val!3

 }

 U_2_int -> {

-  -2 -> -2

+  T@U!val!3 -> -2

   else -> -2

 }

 MapType0TypeInv1 -> {

-  *13 -> *6

-  else -> *6

+  T@T!val!4 -> T@T!val!3

+  else -> T@T!val!3

 }

 MapType0Type -> {

-  *9 *6 *4 -> *13

-  else -> *13

+  T@T!val!2 T@T!val!3 T@T!val!0 -> T@T!val!4

+  else -> T@T!val!4

 }

 MapType0TypeInv2 -> {

-  *13 -> *4

-  else -> *4

+  T@T!val!4 -> T@T!val!0

+  else -> T@T!val!0

 }

 MapType0TypeInv0 -> {

-  *13 -> *9

-  else -> *9

+  T@T!val!4 -> T@T!val!2

+  else -> T@T!val!2

 }

 int_2_U -> {

-  -2 -> -2

-  else -> -2

+  -2 -> T@U!val!3

+  else -> T@U!val!3

 }

 *** STATE <initial>

-  Heap -> *5

-  this -> *3

+  Heap -> T@U!val!0

+  this -> T@U!val!1

   x -> 797

   y -> **y@@1

   r -> **r