From 71cab467df779fc1a52e8a5f981132f49d9d3182 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 5 Nov 2021 07:15:49 -0700 Subject: 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. --- test/regress/regress0/nl/sqrt2-value.smt2 | 2 +- test/regress/regress1/quantifiers/issue6607-witness-te.smt2 | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'test/regress') 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) -- cgit v1.2.3