enabling regressions from last night, all fixed

diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am
index be01286e26e413aaed13ba53c1c95969f7f38a64..2637958144c361f236c7918cd8985acc9e5b0349 100644 (file)
--- 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 b2dfdceffd36d70d80e2e6ea548465e2b24ba254..7b6addb3bba5050bf8a0d904c715296598752115 100644 (file)
--- 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 954050a971393e420ad56982a778bac6a4d6b1f2..481a19ef385f1ab6af959833c1d80dc7e9e6c8dc 100644 (file)
--- 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