Update test output after Nikolaj's enhancement in Z3.

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