diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-11-05 07:15:49 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-05 14:15:49 +0000 |
| commit | 71cab467df779fc1a52e8a5f981132f49d9d3182 (patch) | |
| tree | e375077c42c8c4a4388147fa282d8cb551596f0e /test/regress | |
| parent | 4669bb1ab2fce322cd8e3e172e57f0aa3006e1d7 (diff) | |
Remove quadratic solving in NlModel (#7542)
This PR removes obsolete code from NlModel concerned with solving quadratic equations. This code is only used on nonlinear real problems where the cad solver is not used.
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) |