From 1d7aa9ba2ff1dfd0f1419361b4d595ab7fb69616 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sat, 31 Oct 2015 18:53:40 +0000
Subject: [PATCH] Fixed rewriter bug in theory_fpa.

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

diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 7b8a83520..100ece48c 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -558,9 +558,10 @@ namespace smt {
         expr_ref bv_atom(m);
         bv_atom = convert_atom(atom);
         SASSERT(is_app(bv_atom) && m.is_bool(bv_atom));
-        bv_atom = m.mk_and(bv_atom, mk_side_conditions());
-
-        assert_cnstr(m.mk_iff(atom, bv_atom));
+        expr_ref constr(m);
+        constr = m.mk_iff(atom, m.mk_and(bv_atom, mk_side_conditions()));
+        m_th_rw(constr);
+        assert_cnstr(constr);
         return true;
     }