From ba70ab9ad24378c9ee67e7b23ffbaeaa9d42dfb9 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 2 Nov 2015 19:08:52 +0000
Subject: [PATCH] Bugfix for theory_fpa

---
 src/smt/theory_fpa.cpp | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 7c637309f..73cab556e 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -737,10 +737,11 @@ namespace smt {
 
         expr_ref converted(m);
         converted = m.mk_and(convert(e), mk_side_conditions());
-        if (is_true)
-            assert_cnstr(m.mk_implies(e, converted));
-        else
-            assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted)));
+
+        expr_ref cnstr(m);
+        cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(m.mk_not(e), m.mk_not(converted));
+        m_th_rw(cnstr);
+        assert_cnstr(cnstr);
     }
 
     void theory_fpa::relevant_eh(app * n) {