status of examples

diff --git a/test/regress/regress0/arrays/unsound1.minimized.smt b/test/regress/regress0/arrays/unsound1.minimized.smt
index 222424fa52642f61891aff65ecbdfbc61c88f3c4..3607403108731b247fcc4a62993a03fb705f9e52 100644 (file)
--- 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 a184344b5cc1378b87b844b401979125bc656a4d..c7e779acde8e462deec37b5c9e8ef37a710758a9 100644 (file)
--- 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))