From 14d2356a320c51579c0657e5f89253dcd82f037d Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 2 Nov 2015 19:25:11 +0000
Subject: [PATCH] Code simplification

---
 src/smt/theory_fpa.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 73cab556e..66a1a6321 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -739,7 +739,7 @@ namespace smt {
         converted = m.mk_and(convert(e), mk_side_conditions());
 
         expr_ref cnstr(m);
-        cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(m.mk_not(e), m.mk_not(converted));
+        cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(converted, e);
         m_th_rw(cnstr);
         assert_cnstr(cnstr);
     }