From 3c8b833eebd7ac8c946958720d3f95c14840355a Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 18 Aug 2016 17:03:32 -0400 Subject: [PATCH] fix expression dereference error in theory_str::gen_assign_unroll_Str2Reg --- src/smt/theory_str.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index ae002f979..05cbe8803 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -7772,10 +7772,11 @@ expr * theory_str::gen_assign_unroll_Str2Reg(expr * n, std::set & unrolls if (canHaveNonEmptyAssign) { return gen_unroll_conditional_options(n, unrolls, lcmStr); } else { - expr * implyL = mk_and(litems); - expr * implyR = ctx.mk_eq_atom(n, m_strutil.mk_string("")); + expr_ref implyL(mk_and(litems), mgr); + expr_ref implyR(ctx.mk_eq_atom(n, m_strutil.mk_string("")), mgr); // want to return (implyL -> implyR) - return mgr.mk_or(mgr.mk_not(implyL), implyR); + expr * final_axiom = rewrite_implication(implyL, implyR); + return final_axiom; } }