From b8f2cf5b0bf8b40d16647892db7ee273ba0ccbf5 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Thu, 28 Nov 2019 12:36:49 -0500
Subject: [PATCH] z3str3: rewrite strong arrangement axiom to avoid assertion
 violation

---
 src/smt/theory_str.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index a3e260435..d7a074ba7 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -4184,6 +4184,7 @@ namespace smt {
 
                 if (m_params.m_StrongArrangements) {
                     expr_ref ax_strong(ctx.mk_eq_atom(ax_l, mk_and(r_items)), mgr);
+                    ctx.get_rewriter()(ax_strong);
                     assert_axiom(ax_strong);
                 } else {
                     assert_implication(ax_l, mk_and(r_items));