From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 11 Jul 2011 20:42:39 +0000 (+0000)
Subject: status of examples
X-Git-Tag: cvc5-1.0.0~8497
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=972666e1ef81277b7a9c5c629524d1824f646c20;p=cvc5.git

status of examples
---

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))