diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-08 10:57:38 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-19 19:09:27 -0400 |
| commit | 4ea1dce10aa9648b695c1249fbafc1255deadb1e (patch) | |
| tree | e90e5dffa2e28c22461da85478ea706c8c0ca62f /test | |
| parent | 7dd316a13b796d02985be63b1b03975a756fb624 (diff) | |
Fixes for miplib-trick application (and a new testcase)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/arith/miplib4.cvc | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test/regress/regress0/arith/miplib4.cvc b/test/regress/regress0/arith/miplib4.cvc index d56015222..2f7db1f54 100644 --- a/test/regress/regress0/arith/miplib4.cvc +++ b/test/regress/regress0/arith/miplib4.cvc @@ -5,9 +5,12 @@ tmp1 : INT; x, y : BOOLEAN; +% nonlinear combination, not eligible for miplib trick replacement ASSERT NOT x AND (NOT y AND TRUE) => tmp1 = 0; ASSERT x AND (NOT y AND TRUE) => tmp1 = 4; ASSERT NOT x AND ( y AND TRUE) => tmp1 = 6; ASSERT x AND ( y AND TRUE) => tmp1 = 12; +ASSERT tmp1 > 10; + CHECKSAT; |