mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-18 09:12:16 +00:00
Code Activity

disable the assert that can fire because of the cube heuristic

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-06-27 13:16:48 -07:00
parent 902a223b34
commit 8d318e81b9
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1405,11 +1405,9 @@ std::ostream& core::print_terms(std::ostream& out) const {
print_term(t, out) << std::endl; print_term(t, out) << std::endl;
lpvar j = m_lar_solver.external_to_local(ext); lpvar j = m_lar_solver.external_to_local(ext);
SASSERT(j + 1); SASSERT(j + 1);
SASSERT(value(t) == val(j));
print_var(j, out);
out << "term again "; print_term(t, out) << std::endl;
auto e = mk_expr(t); auto e = mk_expr(t);
out << "e= " << e << "\n"; out << "e= " << e << "\n";
print_var(j, out);
} }
return out; return out;
} }