From 4e05e93ecbadfae5cfa39b10313687c10a567c89 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 9 Nov 2015 11:52:44 +0000
Subject: [PATCH] Bugfix for FPA model generation/conversion.

Addresses #300
---
 src/smt/theory_fpa.cpp                    | 14 ++++++++++++--
 src/tactic/fpa/fpa2bv_model_converter.cpp |  5 ++---
 2 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 8b031ff27..65a66cf80 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -716,8 +716,8 @@ namespace smt {
         return;
     }
 
-    theory* theory_fpa::mk_fresh(context* new_ctx) { 
-        return alloc(theory_fpa, new_ctx->get_manager()); 
+    theory* theory_fpa::mk_fresh(context* new_ctx) {
+        return alloc(theory_fpa, new_ctx->get_manager());
     }
 
     void theory_fpa::push_scope_eh() {
@@ -863,6 +863,16 @@ namespace smt {
                   mk_ismt2_pp(a2, m) << " eq. cls. #" << get_enode(a2)->get_root()->get_owner()->get_id() << std::endl;);
             res = vp;
         }
+        else if (is_app_of(owner, get_family_id(), OP_FPA_INTERNAL_RM)) {
+            SASSERT(to_app(owner)->get_num_args() == 1);
+            app_ref a0(m);
+            a0 = to_app(owner->get_arg(0));
+            fpa_rm_value_proc * vp = alloc(fpa_rm_value_proc, this);
+            vp->add_dependency(ctx.get_enode(a0));
+            TRACE("t_fpa_detail", tout << "Depends on: " <<
+                mk_ismt2_pp(a0, m) << " eq. cls. #" << get_enode(a0)->get_root()->get_owner()->get_id() << std::endl;);
+            res = vp;
+        }
         else if (ctx.e_internalized(wrapped)) {
             if (m_fpa_util.is_rm(owner)) {
                 fpa_rm_value_proc * vp = alloc(fpa_rm_value_proc, this);
diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp
index 62ad363fd..fdbe54c4d 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_model_converter.cpp
@@ -177,7 +177,6 @@ expr_ref fpa2bv_model_converter::convert_bv2rm(expr * eval_v) const {
     rational bv_val(0);
     unsigned sz = 0;
 
-
     if (bu.is_numeral(eval_v, bv_val, sz)) {
         SASSERT(bv_val.is_uint64());
         switch (bv_val.get_uint64()) {
@@ -309,9 +308,9 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
         expr * bvval = to_app(val)->get_arg(0);
         expr_ref fv(m);
         fv = convert_bv2rm(bv_mdl, var, bvval);
-        TRACE("fpa2bv_mc", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << std::endl;);
+        TRACE("fpa2bv_mc", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << ")" << std::endl;);
         float_mdl->register_decl(var, fv);
-        seen.insert(to_app(val)->get_decl());
+        seen.insert(to_app(bvval)->get_decl());
     }
 
     for (obj_map<func_decl, func_decl*>::iterator it = m_uf2bvuf.begin();