1. Fix for free ensures in inlined procedures. Becomes a skip instead of an assume.

2. Fix for deterministic loop extraction, and a new regression.
3. All regressions (including Dafny) except houdini pass, it is most likely related to the free ensures change.

3 files changed, 38 insertions, 0 deletions

diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer
index b9083fae..48ca65e9 100644
--- a/Test/extractloops/Answer
+++ b/Test/extractloops/Answer
@@ -88,3 +88,8 @@ Stratified Inlining: Reached recursion bound of 4
 

 Boogie program verifier finished with 1 verified, 0 errors

 -----

+----- Running regression test detLoopExtract1.bpl with deterministicExtractLoops

+Stratified Inlining: Reached recursion bound of 4

+

+Boogie program verifier finished with 1 verified, 0 errors

+-----

diff --git a/Test/extractloops/detLoopExtract1.bpl b/Test/extractloops/detLoopExtract1.bpl
new file mode 100644
index 00000000..8388cd57
--- /dev/null
+++ b/Test/extractloops/detLoopExtract1.bpl
@@ -0,0 +1,30 @@
+var g:int;
+
+procedure {:entrypoint} Foo(a:int)
+requires a >= 0;
+modifies g;
+{
+   var b: int;
+   b := 0;
+   g := a;
+  
+LH:
+   goto L_true, L_false;
+
+L_true:
+   assume (b < a); 
+   goto L6;
+
+L6: 
+  b := b + 1;
+  g := 5;
+  goto LH;
+
+L_false:
+   assume (b >= a);	      
+   goto L_end;
+
+L_end:
+   assume (b != a); //modeling assert for stratified inlining
+   return;
+}
diff --git a/Test/extractloops/runtest.bat b/Test/extractloops/runtest.bat
index 05bfae55..6bd151cb 100644
--- a/Test/extractloops/runtest.bat
+++ b/Test/extractloops/runtest.bat
@@ -19,4 +19,7 @@ echo -----
 echo ----- Running regression test detLoopExtract.bpl with deterministicExtractLoops

 %BGEXE% %*  /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /deterministicExtractLoops /recursionBound:4 detLoopExtract.bpl

 echo -----

+echo ----- Running regression test detLoopExtract1.bpl with deterministicExtractLoops

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

+echo -----