diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp
index 9b6af92ff..1ae8a2a2c 100644
--- a/src/ast/float_decl_plugin.cpp
+++ b/src/ast/float_decl_plugin.cpp
@@ -750,8 +750,10 @@ bool float_decl_plugin::is_value(app * e) const {
     case OP_FLOAT_MINUS_ZERO:
     case OP_FLOAT_NAN:
         return true;
-    case OP_FLOAT_TO_FP:
-        return m_manager->is_value(e->get_arg(0));
+    case OP_FLOAT_FP:
+        return m_manager->is_value(e->get_arg(0)) &&
+               m_manager->is_value(e->get_arg(1)) &&
+               m_manager->is_value(e->get_arg(2));
     default:
         return false;
     }
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index ba53dc20f..3c6b18349 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -24,11 +24,11 @@ Revision History:
 
 namespace smt {
 
-    class mk_atom_trail : public trail<theory_fpa> {
+    class fpa_atom_trail : public trail<theory_fpa> {
         bool_var m_var;
     public:
-        mk_atom_trail(bool_var v) : m_var(v) {}
-        virtual ~mk_atom_trail() {}
+        fpa_atom_trail(bool_var v) : m_var(v) {}
+        virtual ~fpa_atom_trail() {}
         virtual void undo(theory_fpa & th) {
             theory_fpa::atom * a = th.get_bv2a(m_var);
             a->~atom();
@@ -87,7 +87,7 @@ namespace smt {
         ctx.set_var_theory(l.var(), get_id());
         pred_atom * a = new (get_region()) pred_atom(l, def);
         insert_bv2a(l.var(), a);
-        m_trail_stack.push(mk_atom_trail(l.var()));
+        m_trail_stack.push(fpa_atom_trail(l.var()));
         
         if (!ctx.relevancy()) {
             ctx.mk_th_axiom(get_id(), l, ~def);
@@ -257,7 +257,7 @@ namespace smt {
     }
 
     void theory_fpa::pop_scope_eh(unsigned num_scopes) {
-        TRACE("bv", tout << num_scopes << "\n";);
+        TRACE("t_fpa", tout << num_scopes << "\n";);        
         m_trail_stack.pop_scope(num_scopes);
         unsigned num_old_vars = get_old_num_vars(num_scopes);
         for (unsigned i = num_old_vars; i < get_num_vars(); i++) {
diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h
index c833f2be3..41374fd8f 100644
--- a/src/smt/theory_fpa.h
+++ b/src/smt/theory_fpa.h
@@ -27,7 +27,11 @@ Revision History:
 namespace smt {
 
     class theory_fpa : public theory {
-        typedef trail_stack<theory_fpa> th_trail_stack;
+        class th_trail_stack : public trail_stack<theory_fpa> {
+        public: 
+            th_trail_stack(theory_fpa & th) : trail_stack<theory_fpa>(th) {}
+            virtual ~th_trail_stack() {}
+        };
 
     public:
         class atom {