mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-10 09:48:05 +00:00
Code Activity

remove the too early return

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-09-29 13:12:15 -07:00
parent 1582e4616e
commit cc957011f2
1 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/lp/nra_solver.cpp
View file

@ -355,7 +355,8 @@ struct solver::imp {
m_nla_core.set_use_nra_model(true); m_nla_core.set_use_nra_model(true);
break; break;
case l_false: case l_false:
return add_lemma(clause); r = add_lemma(clause);
break;
default: default:
break; break;
} }
@ -397,13 +398,14 @@ struct solver::imp {
UNREACHABLE(); UNREACHABLE();
return l_undef; return l_undef;
} }
// NSB review: what is this??? // Ignore a lemma which is satisfied
if (m_nla_core.ineq_holds(inq)) if (m_nla_core.ineq_holds(inq))
return l_undef; return l_undef;
lemma |= inq; lemma |= inq;
IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n");
return l_false;
} }
IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n");
m_nla_core.set_use_nra_model(true);
return l_false;
} }
void constraint_core2ex(lp::explanation& ex) { void constraint_core2ex(lp::explanation& ex) {