diff options
Diffstat (limited to 'src/theory/arith/nl/cad_solver.cpp')
| -rw-r--r-- | src/theory/arith/nl/cad_solver.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index bb1ef9911..b1f0894fb 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -134,10 +134,12 @@ std::vector<NlLemma> CadSolver::checkPartial() premise = nm->mkNode(Kind::AND, interval.d_origins); } Node conclusion = - excluding_interval_to_lemma(first_var, interval.d_interval); - Node lemma = nm->mkNode(Kind::IMPLIES, premise, conclusion); - Trace("nl-cad") << "Excluding " << first_var << " -> " << interval.d_interval << " using " << lemma << std::endl; - lems.emplace_back(lemma, Inference::CAD_EXCLUDED_INTERVAL); + excluding_interval_to_lemma(first_var, interval.d_interval, false); + if (!conclusion.isNull()) { + Node lemma = nm->mkNode(Kind::IMPLIES, premise, conclusion); + Trace("nl-cad") << "Excluding " << first_var << " -> " << interval.d_interval << " using " << lemma << std::endl; + lems.emplace_back(lemma, Inference::CAD_EXCLUDED_INTERVAL); + } } } return lems; |