diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-11 12:59:13 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-11 13:07:55 -0600 |
| commit | e2f28f39b3a3749a5eeed5294f25bec1e210b129 (patch) | |
| tree | 6bd5fc8c198139bdf518ad3ae443d87eac13816f /test/regress/regress0/bv | |
| parent | 4ee85fbbe8f1bbc6261b804916f897b26d500fbf (diff) | |
Add simple inferences for extended bitvector functions, add a few related options. Use bv2nat, int2bv as triggers. Add regressions.
Diffstat (limited to 'test/regress/regress0/bv')
| -rw-r--r-- | test/regress/regress0/bv/Makefile.am | 6 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bv-int-collapse1.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bv-int-collapse2-sat.smt2 | 8 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bv-int-collapse2.smt2 | 7 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bv2nat-simp-range.smt2 | 7 |
5 files changed, 34 insertions, 1 deletions
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index f65fbf9a9..2aeb7a220 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -96,7 +96,11 @@ SMT_TESTS = \ unsound1-reduced.smt2 \ bv2nat-ground.smt2 \ bv2nat-ground-c.smt2 \ - cmu-rdk-3.smt2 + cmu-rdk-3.smt2 \ + bv2nat-simp-range.smt2 \ + bv-int-collapse1.smt2 \ + bv-int-collapse2.smt2 \ + bv-int-collapse2-sat.smt2 # Regression tests for SMT2 inputs SMT2_TESTS = divtest.smt2 diff --git a/test/regress/regress0/bv/bv-int-collapse1.smt2 b/test/regress/regress0/bv/bv-int-collapse1.smt2 new file mode 100644 index 000000000..5b631a7fd --- /dev/null +++ b/test/regress/regress0/bv/bv-int-collapse1.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-fun t () (_ BitVec 16)) +(assert (not (= t ((_ int2bv 16) (bv2nat t))))) +(check-sat) diff --git a/test/regress/regress0/bv/bv-int-collapse2-sat.smt2 b/test/regress/regress0/bv/bv-int-collapse2-sat.smt2 new file mode 100644 index 000000000..1a355a495 --- /dev/null +++ b/test/regress/regress0/bv/bv-int-collapse2-sat.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-fun t () Int) +(assert (> t 0)) +(assert (not (= t (bv2nat ((_ int2bv 16) t))))) +(check-sat) diff --git a/test/regress/regress0/bv/bv-int-collapse2.smt2 b/test/regress/regress0/bv/bv-int-collapse2.smt2 new file mode 100644 index 000000000..a630049cb --- /dev/null +++ b/test/regress/regress0/bv/bv-int-collapse2.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-fun t () Int) +(assert (= (+ t 1) (bv2nat ((_ int2bv 16) t)))) +(check-sat) diff --git a/test/regress/regress0/bv/bv2nat-simp-range.smt2 b/test/regress/regress0/bv/bv2nat-simp-range.smt2 new file mode 100644 index 000000000..e5ea20885 --- /dev/null +++ b/test/regress/regress0/bv/bv2nat-simp-range.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-fun t () (_ BitVec 16)) +(assert (not (and (<= 0 (bv2nat t)) (< (bv2nat t) 65536)))) +(check-sat) |