From 84d4546e5a66cf37775b769e7456f0f4a86c4cf0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 10 Mar 2020 13:54:11 -0500 Subject: [PATCH] Remove assertion in resolution bound inferences (#3980) * Fix assertion in resolution bound inferences * Format * Minor Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> --- src/theory/arith/nonlinear_extension.cpp | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index af384be49..72f570f67 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -2673,18 +2673,26 @@ std::vector NonlinearExtension::checkMonomialInferResBounds() { // if they have common factors std::map::iterator ita = d_mono_diff[a].find(b); if (ita != d_mono_diff[a].end()) { + Trace("nl-ext-rbound") << "Get resolution inferences for [a] " << a + << " vs [b] " << b << std::endl; std::map::iterator itb = d_mono_diff[b].find(a); Assert(itb != d_mono_diff[b].end()); Node mv_a = d_model.computeAbstractModelValue(ita->second); Assert(mv_a.isConst()); int mv_a_sgn = mv_a.getConst().sgn(); - Assert(mv_a_sgn != 0); + if (mv_a_sgn == 0) + { + // we don't compare monomials whose current model value is zero + continue; + } Node mv_b = d_model.computeAbstractModelValue(itb->second); Assert(mv_b.isConst()); int mv_b_sgn = mv_b.getConst().sgn(); - Assert(mv_b_sgn != 0); - Trace("nl-ext-rbound") << "Get resolution inferences for [a] " - << a << " vs [b] " << b << std::endl; + if (mv_b_sgn == 0) + { + // we don't compare monomials whose current model value is zero + continue; + } Trace("nl-ext-rbound") << " [a] factor is " << ita->second << ", sign in model = " << mv_a_sgn << std::endl; -- 2.30.2