summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress0/arrays/unsound1.minimized.smt2
-rw-r--r--test/regress/regress0/arrays/unsound1.smt2
2 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress0/arrays/unsound1.minimized.smt b/test/regress/regress0/arrays/unsound1.minimized.smt
index 222424fa5..360740310 100644
--- a/test/regress/regress0/arrays/unsound1.minimized.smt
+++ b/test/regress/regress0/arrays/unsound1.minimized.smt
@@ -4,7 +4,7 @@
:extrafuns ((v0 Array))
:extrafuns ((v3 Element))
:extrafuns ((v1 Index))
-:status unknown
+:status sat
:formula
(flet ($n1 true)
(let (?n2 (select v0 v2))
diff --git a/test/regress/regress0/arrays/unsound1.smt b/test/regress/regress0/arrays/unsound1.smt
index a184344b5..c7e779acd 100644
--- a/test/regress/regress0/arrays/unsound1.smt
+++ b/test/regress/regress0/arrays/unsound1.smt
@@ -1,6 +1,6 @@
(benchmark fuzzsmt
:logic QF_AX
-:status unknown
+:status sat
:extrafuns ((v0 Array))
:extrafuns ((v1 Index))
:extrafuns ((v2 Index))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback