summaryrefslogtreecommitdiff
path: root/Test/lazyinline
diff options
context:
space:
mode:
authorGravatar akashlal <unknown>2010-09-18 05:09:45 +0000
committerGravatar akashlal <unknown>2010-09-18 05:09:45 +0000
commitdbc59dc5f6dd703720df9815ed83158a351417fe (patch)
tree3eaa53ca9f398843cfc3295ea6d896dbd97a48c5 /Test/lazyinline
parent9a7c232927b5470fbefce15a835626008abb468d (diff)
Added test for loop extraction
Diffstat (limited to 'Test/lazyinline')
-rw-r--r--Test/lazyinline/fooret.bpl36
1 files changed, 36 insertions, 0 deletions
diff --git a/Test/lazyinline/fooret.bpl b/Test/lazyinline/fooret.bpl
new file mode 100644
index 00000000..c81baaf1
--- /dev/null
+++ b/Test/lazyinline/fooret.bpl
@@ -0,0 +1,36 @@
+
+procedure A()
+{
+ var x : int;
+ var y : int;
+ var nondet: bool;
+
+start:
+ x := 0;
+ assume y == 2;
+ goto lh;
+
+lh:
+ goto lab1, lab2;
+
+lab1:
+ assume x < y;
+ x := x + 1;
+ havoc nondet;
+ goto lab3, lab4;
+
+lab3:
+ assume !nondet;
+ goto lh;
+
+lab4:
+ assume nondet;
+ return;
+
+lab2:
+ assume x >= y;
+ assert false;
+
+}
+
+