diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
index 63c14f297..8cefee8da 100644
--- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp
+++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
@@ -218,7 +218,7 @@ protected:
                     else if (m.is_bool(arg)) {
                         res = local_simplify(a, n, id, i);
                         TRACE("ctx_solver_simplify_tactic", 
-                              tout << "Already cached: " << path_r.first << " " << mk_pp(res, m) << "\n";);
+                              tout << "Already cached: " << path_r.first << " " << mk_pp(arg, m) << " |-> " << mk_pp(res, m) << "\n";);
                         args.push_back(res);
                     }
                     else {
@@ -327,7 +327,7 @@ protected:
         tmp = m.mk_eq(result, n);
         m_solver.assert_expr(tmp);
         if (!simplify_bool(n2, result)) {
-            result = a;
+            result = a->get_arg(index);
         }
         m_solver.pop(1);
         return result;
diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp
index 234c343b8..ff24d1ceb 100644
--- a/src/tactic/fpa/fpa2bv_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_converter.cpp
@@ -2437,7 +2437,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     t = m_bv_util.mk_bv_sub(t, lz); 
     t = m_bv_util.mk_bv_sub(t, m_bv_util.mk_sign_extend(2, e_min));
     expr_ref TINY(m);
-    TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral(-1, ebits+2));
+    TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral((unsigned)-1, ebits+2));
     
     TRACE("fpa2bv_dbg", tout << "TINY = " << mk_ismt2_pp(TINY, m) << std::endl;);
     SASSERT(is_well_sorted(m, TINY));
@@ -2481,7 +2481,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     m_simp.mk_ite(sigma_le_cap, sigma_neg, sigma_cap, sigma_neg_capped);
     dbg_decouple("fpa2bv_rnd_sigma_neg", sigma_neg);
     dbg_decouple("fpa2bv_rnd_sigma_neg_capped", sigma_neg_capped);
-    sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral(-1, sigma_size));
+    sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral((unsigned)-1, sigma_size));
     dbg_decouple("fpa2bv_rnd_sigma_lt_zero", sigma_lt_zero);
 
     sig_ext = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_size));