diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-09 13:31:45 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-09 20:31:45 +0000 |
commit | 6017579ab78cbc1390274290736ef311208a251b (patch) | |
tree | 70714952802ac299ae4cb3e15b35a86aeae80c9c /test | |
parent | 73a3f516e3179141a71d3201e908bebf3061ead0 (diff) |
Make `--solve-int-as-bv=X` robust to rewriting (#6722)
After commit 327a24508ed1d02a3fa233e680ffd0b30aa685a9, the int-to-bv
preprocessing pass is getting rewritten terms. As a result, the terms
can contain negative constants (instead of `(- c)`, i.e., `UMINUS` of a
positive constant) and `NONLINEAR_MULT`. The commit adds support for
those cases, does some minor cleanup, and adds regressions. The
regressions should allow us to detect if/when the preprocessing pass
breaks in the future.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 4 | ||||
-rw-r--r-- | test/regress/regress0/int-to-bv/basic.smt2 | 10 | ||||
-rw-r--r-- | test/regress/regress0/int-to-bv/neg-consts.smt2 | 9 | ||||
-rw-r--r-- | test/regress/regress0/int-to-bv/not-enough-bits.smt2 | 11 | ||||
-rw-r--r-- | test/regress/regress0/int-to-bv/overflow.smt2 | 9 |
5 files changed, 43 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 19c689b87..b94e06e47 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -645,6 +645,10 @@ set(regress_0_tests regress0/incorrect1.smtv1.smt2 regress0/ineq_basic.smtv1.smt2 regress0/ineq_slack.smtv1.smt2 + regress0/int-to-bv/basic.smt2 + regress0/int-to-bv/neg-consts.smt2 + regress0/int-to-bv/not-enough-bits.smt2 + regress0/int-to-bv/overflow.smt2 regress0/issue1063-overloading-dt-cons.smt2 regress0/issue1063-overloading-dt-fun.smt2 regress0/issue1063-overloading-dt-sel.smt2 diff --git a/test/regress/regress0/int-to-bv/basic.smt2 b/test/regress/regress0/int-to-bv/basic.smt2 new file mode 100644 index 000000000..1e30a7ee8 --- /dev/null +++ b/test/regress/regress0/int-to-bv/basic.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --solve-int-as-bv=5 --no-check-models +(set-logic QF_NIA) +(declare-const x Int) +(declare-const y Int) +; Tests the conversion of negative constants and non-linear multiplication +(assert (= (- 2) (* x y))) +; Operators with more than two children +(assert (= 8 (* x x x))) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress0/int-to-bv/neg-consts.smt2 b/test/regress/regress0/int-to-bv/neg-consts.smt2 new file mode 100644 index 000000000..46c08dad5 --- /dev/null +++ b/test/regress/regress0/int-to-bv/neg-consts.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --solve-int-as-bv=4 --no-check-models +(set-logic QF_NIA) +(declare-const x Int) +(declare-const y Int) +(assert (> (- 1) x)) +(assert (>= y x)) +(assert (< 0 y)) +(set-info :status sat) +(check-sat) diff --git a/test/regress/regress0/int-to-bv/not-enough-bits.smt2 b/test/regress/regress0/int-to-bv/not-enough-bits.smt2 new file mode 100644 index 000000000..49711ecc9 --- /dev/null +++ b/test/regress/regress0/int-to-bv/not-enough-bits.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --solve-int-as-bv=3 +; SCRUBBER: sed -n "s/.*\(Not enough bits\).*: 4.*/\1/p" +; EXPECT: Not enough bits +; EXIT: 1 +(set-logic QF_NIA) +(declare-const x Int) +(declare-const y Int) +; The negative constant fits, the positive does not +(assert (= (- 4) (* x y))) +(assert (= 4 (* x y))) +(check-sat) diff --git a/test/regress/regress0/int-to-bv/overflow.smt2 b/test/regress/regress0/int-to-bv/overflow.smt2 new file mode 100644 index 000000000..30e47adb3 --- /dev/null +++ b/test/regress/regress0/int-to-bv/overflow.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --solve-int-as-bv=4 +; EXPECT: unknown +(set-logic QF_NIA) +(declare-const x Int) +(declare-const y Int) +(assert (= (- 1) (+ x y))) +(assert (> x 0)) +(assert (> y 0)) +(check-sat) |