diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-26 17:10:28 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-26 17:10:35 -0500 |
| commit | 9f9bb26c58f386dbcce92655e3159a7665dd9eb0 (patch) | |
| tree | 5e33d36480ce6b66c57644e8fc73c5d649fc3880 | |
| parent | 059b384c7aa7a54e5a6a321aa1a1c9caeb1d9118 (diff) | |
Enable bv2nat regressions
| -rw-r--r-- | test/regress/regress0/bv/Makefile.am | 5 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bv2nat-ground-c.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bv2nat-ground.smt2 | 2 |
3 files changed, 8 insertions, 1 deletions
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index 0b99024eb..f65fbf9a9 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -93,7 +93,10 @@ SMT_TESTS = \ calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt \ smtcompbug.smt \ unsound1.smt2 \ - unsound1-reduced.smt2 + unsound1-reduced.smt2 \ + bv2nat-ground.smt2 \ + bv2nat-ground-c.smt2 \ + cmu-rdk-3.smt2 # Regression tests for SMT2 inputs SMT2_TESTS = divtest.smt2 diff --git a/test/regress/regress0/bv/bv2nat-ground-c.smt2 b/test/regress/regress0/bv/bv2nat-ground-c.smt2 index 2bb09c2cf..aa5acde6e 100644 --- a/test/regress/regress0/bv/bv2nat-ground-c.smt2 +++ b/test/regress/regress0/bv/bv2nat-ground-c.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat (set-logic QF_BVLIA) (set-info :status unsat) (declare-const a (_ BitVec 32)) diff --git a/test/regress/regress0/bv/bv2nat-ground.smt2 b/test/regress/regress0/bv/bv2nat-ground.smt2 index f72228b28..bfc22850e 100644 --- a/test/regress/regress0/bv/bv2nat-ground.smt2 +++ b/test/regress/regress0/bv/bv2nat-ground.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores +; EXPECT: unsat (set-logic QF_BVLIA) (set-info :status unsat) (declare-const a (_ BitVec 32)) |