summaryrefslogtreecommitdiff
path: root/test/regress/regress0/arith/bug547.2.smt2
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2017-06-28 13:37:18 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2017-06-28 13:37:18 -0500
commitae1d4e4f05fdc2db61d7de7efee5bd567363ceef (patch)
treec10153364551b0c0535b105a9397124af9fc1954 /test/regress/regress0/arith/bug547.2.smt2
parentea8e9af7e428930898ba42d9a80ad725dee43cc7 (diff)
Enable non-linear solve by default, update regressions.
Diffstat (limited to 'test/regress/regress0/arith/bug547.2.smt2')
-rw-r--r--test/regress/regress0/arith/bug547.2.smt22
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/arith/bug547.2.smt2 b/test/regress/regress0/arith/bug547.2.smt2
index f39262c08..b7d114eb3 100644
--- a/test/regress/regress0/arith/bug547.2.smt2
+++ b/test/regress/regress0/arith/bug547.2.smt2
@@ -1,5 +1,5 @@
; COMMAND-LINE: --rewrite-divk
-; EXPECT: unknown
+; EXPECT: sat
(set-logic QF_NIA)
(declare-fun x () Int)
(declare-fun y () Int)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback