From 32e5c6ffd1d2743fd0bcddc75006cddb9316cbaf Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 4 Dec 2019 16:41:51 -0500 Subject: [PATCH] z3str3: missed instance of rewrite-then-assert --- src/smt/theory_str.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 4b36ad501..f304539f5 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -3638,7 +3638,7 @@ namespace smt { expr_ref conclusion(mk_or(arrangement_disjunction), mgr); if (m_params.m_StrongArrangements) { expr_ref ax_strong(ctx.mk_eq_atom(premise, conclusion), mgr); - assert_axiom(ax_strong); + assert_axiom_rw(ax_strong); } else { assert_implication(premise, conclusion); }