From 3e37476e15593fe7889b2644bcf389f90f985e35 Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Thu, 19 Nov 2015 14:19:25 -0600
Subject: Update test output after Nikolaj's enhancement in Z3.

---
 Test/optimization/Optimization3.bpl        | 2 +-
 Test/optimization/Optimization3.bpl.expect | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Test/optimization/Optimization3.bpl b/Test/optimization/Optimization3.bpl
index c1dba49c..02499c31 100644
--- a/Test/optimization/Optimization3.bpl
+++ b/Test/optimization/Optimization3.bpl
@@ -6,7 +6,7 @@ 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".
+    assume {:maximize x} true;
     assert (exists y: int :: y < x);
 }
 
diff --git a/Test/optimization/Optimization3.bpl.expect b/Test/optimization/Optimization3.bpl.expect
index 6f308d7d..6a0066fc 100644
--- a/Test/optimization/Optimization3.bpl.expect
+++ b/Test/optimization/Optimization3.bpl.expect
@@ -2,7 +2,7 @@
 %lbl%@80 -> false
 %lbl%+33 -> true
 %lbl%+61 -> true
-x -> (- 962)
+x -> 41
 tickleBool -> {
   true -> true
   false -> true
-- 
cgit v1.2.3