summaryrefslogtreecommitdiff
path: root/test/regress/regress0/arith/div.05.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/div.05.smt2
parentea8e9af7e428930898ba42d9a80ad725dee43cc7 (diff)
Enable non-linear solve by default, update regressions.
Diffstat (limited to 'test/regress/regress0/arith/div.05.smt2')
-rw-r--r--test/regress/regress0/arith/div.05.smt24
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress0/arith/div.05.smt2 b/test/regress/regress0/arith/div.05.smt2
index 9e4972e38..fd3e4ae48 100644
--- a/test/regress/regress0/arith/div.05.smt2
+++ b/test/regress/regress0/arith/div.05.smt2
@@ -1,7 +1,7 @@
-; EXPECT: unknown
+; EXPECT: sat
(set-logic QF_NRA)
(set-info :smt-lib-version 2.0)
-(set-info :status unknown)
+(set-info :status sat)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun n () Real)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback