diff options
Diffstat (limited to 'src/theory/arith/nonlinear_extension.cpp')
| -rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index c2ebc55b8..f790a9f1a 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -1553,6 +1553,13 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, // nt_lemmas.size() << std::endl; prioritize lemmas that do not // introduce new monomials lemmas_proc = flushLemmas(lemmas); + + if (options::nlExtTangentPlanes() && options::nlExtTangentPlanesInterleave()) + { + lemmas = checkTangentPlanes(); + lemmas_proc += flushLemmas(lemmas); + } + if (lemmas_proc > 0) { Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; @@ -1590,7 +1597,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, } //------------------------------------tangent planes - if (options::nlExtTangentPlanes()) + if (options::nlExtTangentPlanes() && !options::nlExtTangentPlanesInterleave()) { lemmas = checkTangentPlanes(); d_waiting_lemmas.insert( |