summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2011-07-11 18:50:44 +0000
committerMorgan Deters <mdeters@gmail.com>2011-07-11 18:50:44 +0000
commitfb28f98f229c281c8d3e074f1d0d8784574fefa6 (patch)
tree7f9b05ae408df8cca96ad02965c0c57c4634214a /test
parent4c428c8f74ae913f05287c0595c8887c31089520 (diff)
mark the new minimized benchmark as unsat
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress0/arrays/incorrect8.minimized.smt2
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/arrays/incorrect8.minimized.smt b/test/regress/regress0/arrays/incorrect8.minimized.smt
index 18067e654..d08b71e93 100644
--- a/test/regress/regress0/arrays/incorrect8.minimized.smt
+++ b/test/regress/regress0/arrays/incorrect8.minimized.smt
@@ -4,7 +4,7 @@
:extrafuns ((v3 Index))
:extrafuns ((v5 Element))
:extrafuns ((v1 Array))
-:status unknown
+:status unsat
:formula
(let (?n1 (store v1 v4 v5))
(let (?n2 (select ?n1 v3))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback