mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
parent
b0605a9d36
commit
dd27f7e937
|
@ -1542,8 +1542,8 @@ bool theory_seq::add_length_to_eqc(expr* e) {
|
|||
expr* o = n->get_expr();
|
||||
if (!has_length(o)) {
|
||||
expr_ref len(m_util.str.mk_length(o), m);
|
||||
ensure_enode(len);
|
||||
add_length(len);
|
||||
ensure_enode(len);
|
||||
change = true;
|
||||
}
|
||||
n = n->get_next();
|
||||
|
|
Loading…
Reference in a new issue