mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
avoid useless false equality literals
This commit is contained in:
parent
1d8d58710c
commit
546e152837
|
@ -132,6 +132,8 @@ namespace smt {
|
|||
if (a == b) {
|
||||
return true_literal;
|
||||
}
|
||||
if (m.are_distinct(a, b))
|
||||
return false_literal;
|
||||
app_ref eq(ctx.mk_eq_atom(a, b), get_manager());
|
||||
TRACE("mk_var_bug", tout << "mk_eq: " << eq->get_id() << " " << a->get_id() << " " << b->get_id() << "\n";
|
||||
tout << mk_ll_pp(a, get_manager()) << "\n" << mk_ll_pp(b, get_manager()););
|
||||
|
|
Loading…
Reference in a new issue