mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

fix build warnings for theory_str_mc

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-10 09:02:14 -08:00
parent c36a980eb7
commit d770b5135d
1 changed files with 6 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/smt/theory_str_mc.cpp
View file

@ -267,9 +267,8 @@ namespace smt {
ast_manager & sub_m = subsolver.m();
context & sub_ctx = subsolver.get_context();
expr * full;
expr * pref;
u.str.is_prefix(f, pref, full);
expr * pref = nullptr, *full = nullptr;
VERIFY(u.str.is_prefix(f, pref, full));
expr_ref haystack(full, m);
expr_ref needle(pref, m);
@ -384,9 +383,8 @@ namespace smt {
ast_manager & sub_m = subsolver.m();
context & sub_ctx = subsolver.get_context();
expr * full;
expr * small;
u.str.is_contains(f, full, small);
expr * small = nullptr, *full = nullptr;
VERIFY(u.str.is_contains(f, full, small));
expr_ref haystack(full, m);
expr_ref needle(small, m);
@ -1048,10 +1046,8 @@ namespace smt {
// do nothing
} else if (m.is_false(f_new)) {
context & ctx = get_context();
if (u.str.is_contains(f)) {
expr * haystack;
expr * needle;
u.str.is_contains(f, haystack, needle);
expr * needle = nullptr, *haystack = nullptr;
if (u.str.is_contains(f, haystack, needle)) {
expr_ref haystack_assignment(m);
expr_ref needle_assignment(m);
(*replacer)(haystack, haystack_assignment);