From 72dbb2a51315e729cf6cadb515acad3b00359edc Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 10 Dec 2014 20:04:24 +0000
Subject: [PATCH] FPA API bugfix

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/api/dotnet/Context.cs      | 13 -------------
 src/ast/fpa/fpa2bv_converter.h |  2 +-
 2 files changed, 1 insertion(+), 14 deletions(-)

diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 19f6d582c..87090dcc9 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3788,19 +3788,6 @@ namespace Microsoft.Z3
             return new FPExpr(this, Native.Z3_mk_fpa_convert(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject));
         }
 
-        /// <summary>
-        /// Conversion of a floating point term to a bit-vector term in IEEE754 format.
-        /// </summary>
-        /// <remarks>
-        /// The size of the resulting bit-vector is automatically determined.
-        /// </remarks>
-        /// <param name="t">floating point term</param>    
-        public FPExpr MkFPToIEEEBV(FPExpr t) 
-        {
-            Contract.Ensures(Contract.Result<FPNum>() != null);
-            return new FPExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject));
-        }
-
         #endregion
 
         #region Miscellaneous
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index d033890be..08542cd40 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -73,7 +73,7 @@ public:
         SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1);
         SASSERT(m_bv_util.is_bv(significand));
         SASSERT(m_bv_util.is_bv(exponent));
-        result = m.mk_app(m_util.get_family_id(), OP_FLOAT_FP, sign, significand, exponent);
+        result = m.mk_app(m_util.get_family_id(), OP_FLOAT_TO_FP, sign, significand, exponent);
     }
 
     void mk_eq(expr * a, expr * b, expr_ref & result);