From a51f4e6cba57b6711e36ef482f4e320c9cf0542f Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Wed, 18 Nov 2015 15:46:24 -0600
Subject: Add experimental support for optimization (requires Z3 build after
 changeset 9cba63c31f6f1466dd4ef442bb840d1ab84539c7).

---
 Test/optimization/Optimization1.bpl | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 Test/optimization/Optimization1.bpl

(limited to 'Test/optimization/Optimization1.bpl')

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