From 69cab61de3ed63d59828eed1636953e4c57db80b Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 28 Jan 2020 20:37:45 -0500 Subject: [PATCH] z3str3: fix str.contains bitvector reduction --- src/smt/theory_str_mc.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp index 0687c8a51..9b692a91a 100644 --- a/src/smt/theory_str_mc.cpp +++ b/src/smt/theory_str_mc.cpp @@ -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); }