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.

1 files changed, 30 insertions, 0 deletions

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;
+}