summaryrefslogtreecommitdiff
path: root/test/regress/regress0/aufbv
diff options
context:
space:
mode:
authorDejan Jovanović <dejan.jovanovic@gmail.com>2012-06-13 15:50:56 +0000
committerDejan Jovanović <dejan.jovanovic@gmail.com>2012-06-13 15:50:56 +0000
commitb5e8317b54db8c68281ab6889e8ec7ad21270876 (patch)
tree95923fca6425e4d531b4ff223142fe362ea5667c /test/regress/regress0/aufbv
parent461acb36e53c8d3f59c7cdcf913e6fb92c58cb62 (diff)
enabling regressions from last night, all fixed
Diffstat (limited to 'test/regress/regress0/aufbv')
-rw-r--r--test/regress/regress0/aufbv/Makefile.am4
-rw-r--r--test/regress/regress0/aufbv/fuzz05.delta01.smt2
2 files changed, 4 insertions, 2 deletions
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))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback