mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

fix expression dereference error in theory_str::gen_assign_unroll_Str2Reg

Browse source
This commit is contained in:
Murphy Berzish 2016-08-18 17:03:32 -04:00
parent 54d7e4bbb5
commit 3c8b833eeb
1 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_str.cpp
View file

@ -7772,10 +7772,11 @@ expr * theory_str::gen_assign_unroll_Str2Reg(expr * n, std::set<expr*> & unrolls
if (canHaveNonEmptyAssign) { if (canHaveNonEmptyAssign) {
return gen_unroll_conditional_options(n, unrolls, lcmStr); return gen_unroll_conditional_options(n, unrolls, lcmStr);
} else { } else {
expr * implyL = mk_and(litems); expr_ref implyL(mk_and(litems), mgr);
expr * implyR = ctx.mk_eq_atom(n, m_strutil.mk_string("")); expr_ref implyR(ctx.mk_eq_atom(n, m_strutil.mk_string("")), mgr);
// want to return (implyL -> implyR) // want to return (implyL -> implyR)
return mgr.mk_or(mgr.mk_not(implyL), implyR); expr * final_axiom = rewrite_implication(implyL, implyR);
return final_axiom;
} }
} }