diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2013-03-19 22:09:55 -0400 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2013-03-19 22:09:55 -0400 |
| commit | c30b3e2c03f9c3df51eb8d2e7cb6c72907cb77c0 (patch) | |
| tree | 35ffaacc7ba2b0d2d7b6b4e47112fcd41f560b2d /test/regress | |
| parent | 4cd63abf2ab901ad8d1b1c2cc2e84707736b5659 (diff) | |
| parent | 66175a0f0e8d9cf3bc89c3d422ef5b18b217a7da (diff) | |
merged master with dejan's constant evaluating equality engine
Diffstat (limited to 'test/regress')
| -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; |