mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix unsound rewrite
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
0a29002c2f
commit
9d6728aa71
|
@ -960,7 +960,7 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
|
|||
result = m_util.str.mk_empty(m().get_sort(a));
|
||||
}
|
||||
else {
|
||||
result = a2;
|
||||
result = a;
|
||||
}
|
||||
return BR_DONE;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue