From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Wed, 13 Jun 2012 15:50:56 +0000 (+0000)
Subject: enabling regressions from last night, all fixed
X-Git-Tag: cvc5-1.0.0~8040
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b5e8317b54db8c68281ab6889e8ec7ad21270876;p=cvc5.git

enabling regressions from last night, all fixed
---

diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am
index be01286e2..263795814 100644
--- a/test/regress/regress0/aufbv/Makefile.am
+++ b/test/regress/regress0/aufbv/Makefile.am
@@ -27,7 +27,9 @@ TESTS =	\
 	fuzz03.delta01.smt \
 	fuzz03.smt \
 	fuzz04.delta01.smt \
-	fuzz04.smt
+	fuzz04.smt \
+	fuzz05.delta01.smt \
+	fuzz05.smt
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/aufbv/fuzz05.delta01.smt b/test/regress/regress0/aufbv/fuzz05.delta01.smt
index b2dfdceff..7b6addb3b 100644
--- a/test/regress/regress0/aufbv/fuzz05.delta01.smt
+++ b/test/regress/regress0/aufbv/fuzz05.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_AUFBV
 :extrafuns ((a2 Array[12:9]))
-:status sast
+:status sat
 :formula
 (let (?n1 bv0[13])
 (let (?n2 (bvsdiv ?n1 ?n1))
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 954050a97..481a19ef3 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -73,6 +73,13 @@ SMT_TESTS = \
 	fuzz36.smt \
 	fuzz37.delta01.smt \
 	fuzz37.smt \
+	fuzz38.delta01.smt \
+	fuzz38.smt \
+	fuzz39.delta01.smt \
+	fuzz39.smt \
+	fuzz40.delta01.smt \
+	fuzz40.smt \
+	fuzz41.smt \
 	calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt
 
 # Regression tests for SMT2 inputs