Enable bv2nat regressions

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 0b99024eb94702e0b2b17f0f90b007868e00a927..f65fbf9a9f3485b24b868b3901a1f1ef6bbed6cb 100644 (file)
--- 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 2bb09c2cf73cd4129b36bc8d82b6241cd87e955b..aa5acde6eba483c42d7e6db6468a6acfc871c51a 100644 (file)
--- 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 f72228b28bd316072c629ad77bba9a1ac15b6ada..bfc22850e45eefbc7e410c63fa6825e7ea9a70fe 100644 (file)
--- 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))