diff options
author | Valentin Wüstholz <wuestholz@gmail.com> | 2015-11-19 11:18:42 -0600 |
---|---|---|
committer | Valentin Wüstholz <wuestholz@gmail.com> | 2015-11-19 11:18:42 -0600 |
commit | 261c125776d911fda9b545094cb182f3ceb0cdd2 (patch) | |
tree | 41d83c3b1461ee65ed2639ffa0bab86b6b4ed38d /Test/optimization/Optimization3.bpl | |
parent | 51d0b71fa4fd0795c56f1cddbd85b49625c6c91e (diff) |
Add a test.
Diffstat (limited to 'Test/optimization/Optimization3.bpl')
-rw-r--r-- | Test/optimization/Optimization3.bpl | 20 |
1 files changed, 20 insertions, 0 deletions
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); +} |