3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

z3str3: fix str.contains bitvector reduction

This commit is contained in:
Murphy Berzish 2020-01-28 20:37:45 -05:00 committed by Nikolaj Bjorner
parent 883c5df109
commit 69cab61de3

View file

@ -362,7 +362,7 @@ namespace smt {
// needle[j] == haystack[i+j]
ENSURE(i+j < haystack_chars.size());
expr_ref cLHS(needle_chars.get(j), sub_m);
expr_ref cRHS(haystack_chars.get(j), sub_m);
expr_ref cRHS(haystack_chars.get(i+j), sub_m);
expr_ref _e(sub_ctx.mk_eq_atom(cLHS, cRHS), sub_m);
branch.push_back(_e);
}
@ -421,7 +421,7 @@ namespace smt {
// needle[j] == haystack[i+j]
ENSURE(i+j < haystack_chars.size());
expr_ref cLHS(needle_chars.get(j), sub_m);
expr_ref cRHS(haystack_chars.get(j), sub_m);
expr_ref cRHS(haystack_chars.get(i+j), sub_m);
expr_ref _e(sub_ctx.mk_eq_atom(cLHS, cRHS), sub_m);
branch.push_back(_e);
}