Add experimental support for optimization (requires Z3 build after changeset 9cba63c31f6f1466dd4ef442bb840d1ab84539c7).

7 files changed, 323 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.
diff --git a/Test/optimization/Optimization0.bpl.expect b/Test/optimization/Optimization0.bpl.expect
new file mode 100644
index 00000000..d2f9b606
--- /dev/null
+++ b/Test/optimization/Optimization0.bpl.expect
@@ -0,0 +1,182 @@
+*** MODEL
+%lbl%@280 -> false
+%lbl%+260 -> true
+%lbl%+39 -> true
+x@0 -> 43
+ControlFlow -> {
+  0 0 -> 260
+  0 260 -> 39
+  0 39 -> (- 280)
+  else -> 260
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  43 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(13,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(10,5): anon0
+*** MODEL
+%lbl%@328 -> false
+%lbl%+306 -> true
+%lbl%+66 -> true
+%lbl%+68 -> true
+x@0@@0 -> 24
+ControlFlow -> {
+  0 0 -> 306
+  0 306 -> 66
+  0 68 -> (- 328)
+  0 66 -> 68
+  else -> 306
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  24 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(25,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(20,7): anon0
+    Optimization0.bpl(21,5): anon3_Else
+    Optimization0.bpl(24,5): anon2
+*** MODEL
+%lbl%@360 -> false
+%lbl%+342 -> true
+%lbl%+95 -> true
+%lbl%+99 -> true
+x@0@@1 -> 10
+ControlFlow -> {
+  0 0 -> 342
+  0 342 -> 95
+  0 95 -> 99
+  0 99 -> (- 360)
+  else -> 342
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+*** END_MODEL
+Optimization0.bpl(37,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(32,7): anon0
+    Optimization0.bpl(33,5): anon3_LoopHead
+    Optimization0.bpl(33,5): anon3_LoopDone
+*** MODEL
+%lbl%@393 -> false
+%lbl%+122 -> true
+%lbl%+382 -> true
+x@0@@2 -> 41
+ControlFlow -> {
+  0 0 -> 382
+  0 382 -> 122
+  0 122 -> (- 393)
+  else -> 382
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  41 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(47,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(44,5): anon0
+*** MODEL
+%lbl%@421 -> false
+%lbl%+147 -> true
+%lbl%+151 -> true
+%lbl%+399 -> true
+x@0@@3 -> 42
+ControlFlow -> {
+  0 0 -> 399
+  0 399 -> 147
+  0 147 -> 151
+  0 151 -> (- 421)
+  else -> 399
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  42 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(59,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(54,7): anon0
+    Optimization0.bpl(56,11): anon3_Then
+    Optimization0.bpl(58,5): anon2
+*** MODEL
+%lbl%@453 -> false
+%lbl%+178 -> true
+%lbl%+182 -> true
+%lbl%+435 -> true
+x@0@@4 -> 1
+ControlFlow -> {
+  0 0 -> 435
+  0 435 -> 178
+  0 178 -> 182
+  0 182 -> (- 453)
+  else -> 435
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+*** END_MODEL
+Optimization0.bpl(71,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(66,7): anon0
+    Optimization0.bpl(67,5): anon3_LoopHead
+    Optimization0.bpl(67,5): anon3_LoopDone
+*** MODEL
+%lbl%@497 -> false
+%lbl%+209 -> true
+%lbl%+213 -> true
+%lbl%+475 -> true
+x@0@@5 -> 2
+ControlFlow -> {
+  0 0 -> 475
+  0 475 -> 209
+  0 209 -> 213
+  0 213 -> (- 497)
+  else -> 475
+}
+tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+may_fail -> {
+  2 -> false
+  else -> false
+}
+*** END_MODEL
+Optimization0.bpl(83,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Optimization0.bpl(78,7): anon0
+    Optimization0.bpl(80,11): anon3_Then
+    Optimization0.bpl(82,5): anon2
+
+Boogie program verifier finished with 0 verified, 7 errors
diff --git a/Test/optimization/Optimization1.bpl b/Test/optimization/Optimization1.bpl
new file mode 100644
index 00000000..60df1edd
--- /dev/null
+++ b/Test/optimization/Optimization1.bpl
@@ -0,0 +1,32 @@
+// RUN: %boogie /noVerify /printModel:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0(n: int)
+{
+    assume {:minimize} true;
+}
+
+procedure test1(n: int)
+{
+    assume {:maximize} true;
+}
+
+procedure test2(n: int)
+{
+    assume {:minimize n, n} true;
+}
+
+procedure test3(n: int)
+{
+    assume {:maximize n, n} true;
+}
+
+procedure test4(n: int)
+{
+    assume {:minimize true} true;
+}
+
+procedure test5(n: int)
+{
+    assume {:maximize true} true;
+}
diff --git a/Test/optimization/Optimization1.bpl.expect b/Test/optimization/Optimization1.bpl.expect
new file mode 100644
index 00000000..d8508807
--- /dev/null
+++ b/Test/optimization/Optimization1.bpl.expect
@@ -0,0 +1,5 @@
+Optimization1.bpl(6,11): Error: attributes :minimize and :maximize accept only one argument
+Optimization1.bpl(11,11): Error: attributes :minimize and :maximize accept only one argument
+Optimization1.bpl(16,11): Error: attributes :minimize and :maximize accept only one argument
+Optimization1.bpl(21,11): Error: attributes :minimize and :maximize accept only one argument
+4 name resolution errors detected in Optimization1.bpl
diff --git a/Test/optimization/Optimization2.bpl b/Test/optimization/Optimization2.bpl
new file mode 100644
index 00000000..7d80d735
--- /dev/null
+++ b/Test/optimization/Optimization2.bpl
@@ -0,0 +1,12 @@
+// RUN: %boogie /noVerify /printModel:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0(n: int)
+{
+    assume {:minimize true} true;
+}
+
+procedure test1(n: int)
+{
+    assume {:maximize true} true;
+}
diff --git a/Test/optimization/Optimization2.bpl.expect b/Test/optimization/Optimization2.bpl.expect
new file mode 100644
index 00000000..cab2fd3d
--- /dev/null
+++ b/Test/optimization/Optimization2.bpl.expect
@@ -0,0 +1,3 @@
+Optimization2.bpl(6,11): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv
+Optimization2.bpl(11,11): Error: attributes :minimize and :maximize accept only one argument of type int, real or bv
+2 type checking errors detected in Optimization2.bpl
diff --git a/Test/optimization/lit.local.cfg b/Test/optimization/lit.local.cfg
new file mode 100644
index 00000000..158a1e4d
--- /dev/null
+++ b/Test/optimization/lit.local.cfg
@@ -0,0 +1,3 @@
+# Do not run tests in this directory and below
+config.unsupported = True
+# TODO(wuestholz): Enable these tests once we can rely on Z3 4.4.2 or higher.