summaryrefslogtreecommitdiff
path: root/Test/optimization/Optimization0.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/optimization/Optimization0.bpl')
-rw-r--r--Test/optimization/Optimization0.bpl86
1 files changed, 86 insertions, 0 deletions
diff --git a/Test/optimization/Optimization0.bpl b/Test/optimization/Optimization0.bpl
new file mode 100644
index 00000000..c704c855
--- /dev/null
+++ b/Test/optimization/Optimization0.bpl
@@ -0,0 +1,86 @@
+// RUN: %boogie /doNotUseLabels /printModel:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function may_fail(f: int) : bool;
+
+procedure test0()
+{
+ var x: int;
+
+ havoc x;
+ assume 42 < x;
+ assume {:minimize x} true;
+ assert may_fail(x);
+}
+
+procedure test1()
+{
+ var x: int;
+
+ x := 24;
+ if (*) {
+ x := 42;
+ }
+ assume {:minimize x} true;
+ assert may_fail(x);
+}
+
+procedure test2()
+{
+ var x: int;
+
+ x := 1;
+ while (*) {
+ x := x + 1;
+ }
+ assume {:minimize x} true;
+ assert x < 10;
+}
+
+procedure test3()
+{
+ var x: int;
+
+ havoc x;
+ assume x < 42;
+ assume {:maximize x} true;
+ assert may_fail(x);
+}
+
+procedure test4()
+{
+ var x: int;
+
+ x := 24;
+ if (*) {
+ x := 42;
+ }
+ assume {:maximize x} true;
+ assert may_fail(x);
+}
+
+procedure test5()
+{
+ var x: int;
+
+ x := 1;
+ while (*) {
+ x := x - 1;
+ }
+ assume {:maximize x} true;
+ assert x < 1;
+}
+
+procedure test6()
+{
+ var x: int;
+
+ x := 1;
+ if (*) {
+ x := 2;
+ }
+ assume {:maximize x} true;
+ assert may_fail(x);
+}
+
+// TODO(wuestholz): Make this work without the /doNotUseLabels flag.