From 826d2959813cfc97ebe6285159b83fd2f9c184b6 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 21 Jan 2015 19:29:31 +0000
Subject: [PATCH] build fixes and removed unused variables

---
 src/api/api_fpa.cpp              | 4 +---
 src/ast/fpa/fpa2bv_converter.cpp | 2 --
 src/smt/theory_fpa.h             | 4 ++--
 src/tactic/sls/sls_engine.cpp    | 2 ++
 4 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index 67ffe12d9..96c3e2eb6 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -723,8 +723,7 @@ extern "C" {
         LOG_Z3_fpa_get_numeral_exponent_string(c, t);
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
-        mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
-        unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
+        mpf_manager & mpfm = mk_c(c)->fpa_util().fm();        
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         scoped_mpf val(mpfm);
         bool r = plugin->is_numeral(to_expr(t), val);
@@ -749,7 +748,6 @@ extern "C" {
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
-        unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         scoped_mpf val(mpfm);
         bool r = plugin->is_numeral(to_expr(t), val);        
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index f8f283ee6..9f0591134 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2283,7 +2283,6 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
 
     unsigned ebits = m_util.get_ebits(f->get_range());
     unsigned sbits = m_util.get_sbits(f->get_range());
-    unsigned f_sz = sbits + ebits;
     unsigned bv_sz = m_bv_util.get_bv_size(x);
     SASSERT(m_bv_util.get_bv_size(rm) == 3);
 
@@ -2425,7 +2424,6 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
 
     unsigned ebits = m_util.get_ebits(f->get_range());
     unsigned sbits = m_util.get_sbits(f->get_range());
-    unsigned f_sz = sbits + ebits;
     unsigned bv_sz = m_bv_util.get_bv_size(x);
     SASSERT(m_bv_util.get_bv_size(rm) == 3);    
 
diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h
index 33733d7d9..c3d574179 100644
--- a/src/smt/theory_fpa.h
+++ b/src/smt/theory_fpa.h
@@ -97,7 +97,7 @@ namespace smt {
 
         public:
             fpa_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits) : 
-                m_th(*th), m_fu(th->m_fpa_util), m_bu(th->m_bv_util), m(th->get_manager()),
+                m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util),
                 m_ebits(ebits), m_sbits(sbits) {}
             
             virtual ~fpa_value_proc() {}
@@ -120,7 +120,7 @@ namespace smt {
 
         public:
             fpa_rm_value_proc(theory_fpa * th) : 
-                m_th(*th), m_fu(th->m_fpa_util), m_bu(th->m_bv_util), m(th->get_manager()) {}
+                m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) {}
 
             void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
 
diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp
index 162866ed6..98f659fe0 100644
--- a/src/tactic/sls/sls_engine.cpp
+++ b/src/tactic/sls/sls_engine.cpp
@@ -16,6 +16,8 @@ Author:
 Notes:
 
 --*/
+#include<float.h> // Need DBL_MAX
+
 #include"map.h"
 #include"ast_smt2_pp.h"
 #include"ast_pp.h"