From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 26 Oct 2016 22:10:28 +0000 (-0500)
Subject: Enable bv2nat regressions
X-Git-Tag: cvc5-1.0.0~6019
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9f9bb26c58f386dbcce92655e3159a7665dd9eb0;p=cvc5.git

Enable bv2nat regressions
---

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