mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix #5144
This commit is contained in:
parent
8d9be5322f
commit
878847179f
|
@ -144,7 +144,7 @@ bool theory_seq::propagate_ne2eq(unsigned idx, expr_ref_vector const& es) {
|
|||
expr_ref e(m), head(m), tail(m);
|
||||
e = mk_concat(es, es[0]->get_sort());
|
||||
m_sk.decompose(e, head, tail);
|
||||
propagate_eq(n.dep(), n.lits(), e, mk_concat(head, tail), false);
|
||||
propagate_eq(n.dep(), n.lits(), e, mk_concat(head, tail), true);
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue