diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-13 18:22:28 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-13 16:22:28 -0700 |
| commit | 1f09fa5f3de7c23ea4713984fce658d13e8e3e36 (patch) | |
| tree | 287539b7e6272689b246816ed6df2aa53ed6f5a4 /test | |
| parent | ef7e56f4217ece19b1caf743e5b1db0d3f549226 (diff) | |
Eliminate negative constant coefficients in div/mod (#2929)
Fixes #1399.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/arith/issue1399.smt2 | 12 |
2 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8d69a1a69..1ed879400 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -25,6 +25,7 @@ set(regress_0_tests regress0/arith/integers/ackermann6.smt2 regress0/arith/integers/arith-int-042.cvc regress0/arith/integers/arith-int-042.min.cvc + regress0/arith/issue1399.smt2 regress0/arith/leq.01.smtv1.smt2 regress0/arith/miplib.cvc regress0/arith/miplib2.cvc diff --git a/test/regress/regress0/arith/issue1399.smt2 b/test/regress/regress0/arith/issue1399.smt2 new file mode 100644 index 000000000..80305260e --- /dev/null +++ b/test/regress/regress0/arith/issue1399.smt2 @@ -0,0 +1,12 @@ +(set-logic LIA) +(set-info :status sat) + +(define-fun findIdx ((y1 Int)(y2 Int)(k1 Int)) Int (div (* (- 7) (mod y1 (- 5))) 2)) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun k () Int) + +(assert (not (and (=> (< x1 x2) (=> (< k x1) (= (findIdx x1 x2 k) 0))) + (=> (< x1 x2) (=> (> k x2) (= (findIdx x1 x2 k) 2))) + (=> (< x1 x2) (=> (and (> k x1) (< k x2)) (= (findIdx x1 x2 k) 1)))))) +(check-sat) |