From 261c125776d911fda9b545094cb182f3ceb0cdd2 Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Thu, 19 Nov 2015 11:18:42 -0600
Subject: Add a test.

---
 Test/optimization/Optimization3.bpl        | 20 +++++++++++++++++++
 Test/optimization/Optimization3.bpl.expect | 31 ++++++++++++++++++++++++++++++
 2 files changed, 51 insertions(+)
 create mode 100644 Test/optimization/Optimization3.bpl
 create mode 100644 Test/optimization/Optimization3.bpl.expect

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
-- 
cgit v1.2.3