summaryrefslogtreecommitdiff
path: root/Test/optimization
diff options
context:
space:
mode:
authorGravatar Valentin Wüstholz <wuestholz@gmail.com>2015-11-19 11:18:42 -0600
committerGravatar Valentin Wüstholz <wuestholz@gmail.com>2015-11-19 11:18:42 -0600
commit261c125776d911fda9b545094cb182f3ceb0cdd2 (patch)
tree41d83c3b1461ee65ed2639ffa0bab86b6b4ed38d /Test/optimization
parent51d0b71fa4fd0795c56f1cddbd85b49625c6c91e (diff)
Add a test.
Diffstat (limited to 'Test/optimization')
-rw-r--r--Test/optimization/Optimization3.bpl20
-rw-r--r--Test/optimization/Optimization3.bpl.expect31
2 files changed, 51 insertions, 0 deletions
diff --git a/Test/optimization/Optimization3.bpl b/Test/optimization/Optimization3.bpl
new file mode 100644
index 00000000..c1dba49c
--- /dev/null
+++ b/Test/optimization/Optimization3.bpl
@@ -0,0 +1,20 @@
+// RUN: %boogie /printModel:4 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure test0()
+{
+ var x: int;
+
+ assume x < 42;
+ assume {:maximize x} true; // TODO(wuestholz): Currently, Z3 does not produce a model with "x == 41" here. It seems like this is due to the fact that it returns "unknown".
+ assert (exists y: int :: y < x);
+}
+
+procedure test1()
+{
+ var x: int;
+
+ assume x < 42;
+ assume {:maximize x} true;
+ assert (forall y: int :: y < x);
+}
diff --git a/Test/optimization/Optimization3.bpl.expect b/Test/optimization/Optimization3.bpl.expect
new file mode 100644
index 00000000..6f308d7d
--- /dev/null
+++ b/Test/optimization/Optimization3.bpl.expect
@@ -0,0 +1,31 @@
+*** MODEL
+%lbl%@80 -> false
+%lbl%+33 -> true
+%lbl%+61 -> true
+x -> (- 962)
+tickleBool -> {
+ true -> true
+ false -> true
+ else -> true
+}
+*** END_MODEL
+Optimization3.bpl(10,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Optimization3.bpl(8,5): anon0
+*** MODEL
+%lbl%@115 -> false
+%lbl%+105 -> true
+%lbl%+56 -> true
+x@@0 -> 41
+y@@0!1!1 -> 719
+tickleBool -> {
+ true -> true
+ false -> true
+ else -> true
+}
+*** END_MODEL
+Optimization3.bpl(19,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ Optimization3.bpl(17,5): anon0
+
+Boogie program verifier finished with 0 verified, 2 errors