mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Code simplification
This commit is contained in:
parent
ba70ab9ad2
commit
14d2356a32
|
@ -739,7 +739,7 @@ namespace smt {
|
|||
converted = m.mk_and(convert(e), mk_side_conditions());
|
||||
|
||||
expr_ref cnstr(m);
|
||||
cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(m.mk_not(e), m.mk_not(converted));
|
||||
cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(converted, e);
|
||||
m_th_rw(cnstr);
|
||||
assert_cnstr(cnstr);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue