diff options
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) |