summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/extractloops/Answer5
-rw-r--r--Test/extractloops/detLoopExtract1.bpl30
-rw-r--r--Test/extractloops/runtest.bat3
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 -----