diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index afa4cf98f..28300e569 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -99,7 +99,7 @@ public:
         m_ctx(0),
         m_callback(0) {
         updt_params_core(p);
-        TRACE("smt_tactic", tout << this << "\np: " << p << "\n";);
+        TRACE("smt_tactic", tout << "p: " << p << "\n";);
     }
 
     virtual tactic * translate(ast_manager & m) {
@@ -120,13 +120,12 @@ public:
     }
 
     virtual void updt_params(params_ref const & p) {
-        TRACE("smt_tactic", tout << this << "\nupdt_params: " << p << "\n";);
+        TRACE("smt_tactic", tout << "updt_params: " << p << "\n";);
         updt_params_core(p);
         fparams().updt_params(p);
-        symbol logic = p.get_sym(symbol("logic"), symbol::null);
-        if (logic != symbol::null) {
-            if (m_ctx) m_ctx->set_logic(logic);
-            m_logic = logic;
+        m_logic = p.get_sym(symbol("logic"), m_logic);
+        if (m_logic != symbol::null && m_ctx) {
+            m_ctx->set_logic(m_logic);
         }
         SASSERT(p.get_bool("auto_config", fparams().m_auto_config) == fparams().m_auto_config);
     }
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index f661ca184..5235be230 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -128,8 +128,8 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
     ast_manager & m = m_assertions.m();
     m_result = alloc(simple_check_sat_result, m);
     m_tactic->cleanup();
-    m_tactic->updt_params(m_params);
     m_tactic->set_logic(m_logic);
+    m_tactic->updt_params(m_params); // parameters are allowed to overwrite logic.
     goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores);
 
     unsigned sz = m_assertions.size();
diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp
index 610eee564..0c1744a09 100644
--- a/src/util/mpn.cpp
+++ b/src/util/mpn.cpp
@@ -226,7 +226,7 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum,
                                   mpn_sbuffer & n_denom) const
 {    
     size_t d = 0;
-    while (((denom[lden-1] << d) & MASK_FIRST) == 0) d++;
+    while (lden > 0 && ((denom[lden-1] << d) & MASK_FIRST) == 0) d++;
     SASSERT(d < DIGIT_BITS);
     
     n_numer.resize(lnum+1);
@@ -239,7 +239,8 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum,
         for (size_t i = 0; i < lden; i++)
             n_denom[i] = denom[i];
     }
-    else {
+    else if (lnum != 0) {
+        SASSERT(lden > 0);
         mpn_digit q = FIRST_BITS(d, numer[lnum-1]);
         n_numer[lnum] = q;
         for (size_t i = lnum-1; i > 0; i--)
@@ -249,6 +250,9 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum,
             n_denom[i] = denom[i] << d | FIRST_BITS(d, denom[i-1]);
         n_denom[0] = denom[0] << d;   
     }
+    else {
+        d = 0;
+    }
 
     TRACE("mpn_norm", tout << "Normalized: n_numer="; display_raw(tout, n_numer.c_ptr(), n_numer.size()); 
                       tout << " n_denom="; display_raw(tout, n_denom.c_ptr(), n_denom.size()); tout << std::endl; );