summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bug590.smt2
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2014-10-31 11:35:11 +0100
committerajreynol <andrew.j.reynolds@gmail.com>2014-10-31 11:35:19 +0100
commit458b2b7eb5bdf09a1a886f4e2a165380d5fd918f (patch)
tree342d05bab92d0aa349ab833e6a4b60e887670295 /test/regress/regress0/bug590.smt2
parent5a285d5247b56b00895774c909f09c8ad1e3889c (diff)
Do not allow duplication of function definitions. Set incomplete flag in model builder.
Diffstat (limited to 'test/regress/regress0/bug590.smt2')
-rw-r--r--test/regress/regress0/bug590.smt22
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/bug590.smt2 b/test/regress/regress0/bug590.smt2
index 06dc1fe58..68665f629 100644
--- a/test/regress/regress0/bug590.smt2
+++ b/test/regress/regress0/bug590.smt2
@@ -2,7 +2,7 @@
(set-option :strings-exp true)
(set-option :produce-models true)
(set-info :smt-lib-version 2.0)
-(set-info :status sat)
+(set-info :status unknown)
(declare-fun text () String)
(declare-fun output () String)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback