mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
parent
84520d53ea
commit
dd0b0b47b8
|
@ -770,7 +770,7 @@ void term_graph::mk_qe_lite_equalities(term &t, expr_ref_vector &out,
|
|||
it = &it->get_next()) { tout << *it << "\n"; };);
|
||||
DEBUG_CODE(
|
||||
for (term *it = &t.get_next(); it != &t; it = &it->get_next())
|
||||
SASSERT(!it->is_cgr() ||
|
||||
SASSERT(!it->is_cgr() || it->is_eq_or_neq() ||
|
||||
contains_nc(mk_app_core(it->get_expr()))););
|
||||
return;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue