From bfe6260c58c740c7efda919861ab3d4e5c8f70d9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 27 Nov 2017 08:39:20 -0800
Subject: [PATCH] fix #1376

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_seq.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 131d1fd1b..ca6ab048c 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2400,6 +2400,7 @@ bool theory_seq::add_stoi_axiom(expr* e) {
             nums[i] = m_autil.mk_mul(coeff, nums[i].get());
         }
         num = m_autil.mk_add(nums.size(), nums.c_ptr());
+        ctx.get_rewriter()(num);
         lits.push_back(mk_eq(e, num, false));
         ++m_stats.m_add_axiom;
         m_new_propagation = true;