diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-17 09:38:59 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-17 09:38:59 -0700 |
commit | 899fea16546e71c377ff4923e8ac4998f6d7608c (patch) | |
tree | dd22a27678c0e47e62c829b6497cab92335fd57a /src/theory/arith/nl/nonlinear_extension.cpp | |
parent | d9f6d9b6a40975d69eefec8d4852e8c3cd82878a (diff) | |
parent | 63281fbfe093b1d5e375a378bb59761f77256d08 (diff) |
Merge branch 'master' into fixWinBuildfixWinBuild
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.cpp')
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 8221e18d5..7f97c4122 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -218,7 +218,7 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions) // relevance here, since we may have discarded literals that are relevant // that are entailed based on the techniques in getAssertions. std::vector<Node> passertions = assertions; - if (options::nlExt()) + if (options::nlExt() == options::NlExtMode::FULL) { // preprocess the assertions with the trancendental solver if (!d_trSlv.preprocessAssertionsCheckModel(passertions)) @@ -474,8 +474,8 @@ Result::Sat NonlinearExtension::modelBasedRefinement(const std::set<Node>& termS } // we are incomplete - if (options::nlExt() && options::nlExtIncPrecision() - && d_model.usedApproximate()) + if (options::nlExt() == options::NlExtMode::FULL + && options::nlExtIncPrecision() && d_model.usedApproximate()) { d_trSlv.incrementTaylorDegree(); needsRecheck = true; |