summaryrefslogtreecommitdiff
path: root/Test/doomed
diff options
context:
space:
mode:
Diffstat (limited to 'Test/doomed')
-rw-r--r--Test/doomed/doomed.bpl4
-rw-r--r--Test/doomed/notdoomed.bpl18
2 files changed, 21 insertions, 1 deletions
diff --git a/Test/doomed/doomed.bpl b/Test/doomed/doomed.bpl
index 77eec249..741a54c5 100644
--- a/Test/doomed/doomed.bpl
+++ b/Test/doomed/doomed.bpl
@@ -21,7 +21,9 @@ procedure evilbranch(x:int)
} else {
y := 2;
}
- assert y!=2;
+ assume y!=2;
+
+ assert x<0;
}
diff --git a/Test/doomed/notdoomed.bpl b/Test/doomed/notdoomed.bpl
index eb60536f..c3193a01 100644
--- a/Test/doomed/notdoomed.bpl
+++ b/Test/doomed/notdoomed.bpl
@@ -35,5 +35,23 @@ procedure c(x:int)
}
}
+procedure useCE(x:int)
+{
+ var y : int;
+
+ if(x<0) {
+ y := 1;
+ } else {
+ y := 2;
+ }
+ if(x<7) {
+ y := 5;
+ } else {
+ y := 6;
+ }
+
+}
+
+