From bcfefdd8ee6cd097df65d15813a8489b7408eeaa Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 28 Jan 2015 13:17:22 -0600
Subject: [PATCH] Bugfix for the FPA theory. Thanks to codeplex user smccamant
 for reporting this one.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/smt/theory_fpa.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 45cd60332..3bf9dadb8 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -463,7 +463,8 @@ namespace smt {
         switch (k) {
         case OP_FPA_TO_UBV:
         case OP_FPA_TO_SBV:
-        case OP_FPA_TO_REAL: {
+        case OP_FPA_TO_REAL: 
+        case OP_FPA_TO_IEEE_BV: {
             expr_ref conv(m);
             conv = convert(term);
             assert_cnstr(m.mk_eq(term, conv));