diff options
| -rw-r--r-- | Test/optimization/Optimization3.bpl | 2 | ||||
| -rw-r--r-- | 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 |