mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 07:43:41 +00:00
Code Activity

disable assertion that checks nl lemmas if using nra core

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-05-30 14:47:31 +01:00
parent 2fc3b0730d
commit 7f5427b839
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/nla_core.cpp
View file

@ -1047,7 +1047,7 @@ new_lemma::new_lemma(core& c, char const* name):name(name), c(c) {
new_lemma& new_lemma::operator|=(ineq const& ineq) { new_lemma& new_lemma::operator|=(ineq const& ineq) {
if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) { if (!c.explain_ineq(*this, ineq.term(), ineq.cmp(), ineq.rs())) {
CTRACE(nla_solver, c.ineq_holds(ineq), c.print_ineq(ineq, tout) << "\n";); CTRACE(nla_solver, c.ineq_holds(ineq), c.print_ineq(ineq, tout) << "\n";);
SASSERT(!c.ineq_holds(ineq)); SASSERT(c.m_use_nra_model || !c.ineq_holds(ineq));
current().push_back(ineq); current().push_back(ineq);
} }
return *this; return *this;