diff options
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/nl/sqrt2-value.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue6607-witness-te.smt2 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress0/nl/sqrt2-value.smt2 b/test/regress/regress0/nl/sqrt2-value.smt2 index 078d8fcc7..37dcfaf7e 100644 --- a/test/regress/regress0/nl/sqrt2-value.smt2 +++ b/test/regress/regress0/nl/sqrt2-value.smt2 @@ -3,7 +3,7 @@ ; EXPECT: sat ; EXPECT: ((x (witness (set-option :produce-models true) -(set-logic ALL) +(set-logic QF_NRA) (declare-fun x () Real) (assert (= (* x x) 2)) (check-sat) diff --git a/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 b/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 index ff426c139..431512bf2 100644 --- a/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 +++ b/test/regress/regress1/quantifiers/issue6607-witness-te.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --no-check-models -(set-logic ALL) +(set-logic NRA) (set-info :status sat) (assert (exists ((skoY Real)) (forall ((skoX Real)) (or (= 0.0 (* skoY skoY)) (and (< skoY 0.0) (or (= skoY skoX) (= 2 (* skoY skoY)))))))) (check-sat) |