diff --git a/src/ast/ast_translation.cpp b/src/ast/ast_translation.cpp
index b7ed86da5..532795c5c 100644
--- a/src/ast/ast_translation.cpp
+++ b/src/ast/ast_translation.cpp
@@ -77,8 +77,8 @@ void ast_translation::push_frame(ast * n) {
 }
 
 bool ast_translation::visit(ast * n) {        
-    ast * r;
     if (n->get_ref_count() > 1) {
+        ast * r;
         if (m_cache.find(n, r)) {
             m_result_stack.push_back(r);
             ++m_hit_count;
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index 582194bc2..270ae9d04 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -181,7 +181,7 @@ namespace sat {
         for (bool_var v : to_elim) {
             literal  l(v, false);
             literal r  = roots[v];
-            SASSERT(v != r.var());            
+            SASSERT(v != r.var());
             bool root_ok = !m_solver.is_external(v) || m_solver.set_root(l, r);
             if (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok)) {
                 // cannot really eliminate v, since we have to notify extension of future assignments
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 29eaccb8e..3339bc4e6 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -1477,7 +1477,7 @@ namespace sat {
                 }
             }
             if (m_search_mode == lookahead_mode::lookahead1) {
-                SASSERT(nonfixed >= 2);
+                //SASSERT(nonfixed >= 2);
                 switch (m_config.m_reward_type) {
                 case heule_schur_reward: {
                     double to_add = 0;
@@ -1493,7 +1493,7 @@ namespace sat {
                     m_lookahead_reward += pow(0.5, nonfixed);
                     break;
                 case march_cu_reward:
-                    m_lookahead_reward += 3.3 * pow(0.5, nonfixed - 2);
+                    m_lookahead_reward += nonfixed >= 2 ? 3.3 * pow(0.5, nonfixed - 2) : 0.0;
                     break;
                 case ternary_reward:
                     UNREACHABLE();
@@ -1703,7 +1703,8 @@ namespace sat {
                     num_units += do_double(lit, dl_lvl);
                     if (dl_lvl > level) {
                         base = dl_lvl;
-                        SASSERT(get_level(m_trail.back()) == base + m_lookahead[i].m_offset);
+                        //SASSERT(get_level(m_trail.back()) == base + m_lookahead[i].m_offset);
+                        SASSERT(get_level(m_trail.back()) == base);
                     }
                     unsat = inconsistent();
                     pop_lookahead1(lit, num_units);
@@ -1822,11 +1823,11 @@ namespace sat {
     unsigned lookahead::double_look(literal l, unsigned& base) {
         SASSERT(!inconsistent());
         SASSERT(dl_no_overflow(base));
+        SASSERT(is_fixed_at(l, base));
         base += m_lookahead.size();
         unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations;
         scoped_level _sl(*this, dl_truth);
-        SASSERT(get_level(m_trail.back()) == dl_truth);
-        SASSERT(is_fixed(l));
+        //SASSERT(get_level(m_trail.back()) == dl_truth);
         IF_VERBOSE(2, verbose_stream() << "(sat-lookahead :double " << l << " :depth " << m_trail_lim.size() << ")\n";);
         lookahead_backtrack();
         assign(l);
@@ -2078,7 +2079,8 @@ namespace sat {
             inc_istamp();
             if (inconsistent()) {
                 TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
-                m_cube_state.m_freevars_threshold = m_freevars.size();               
+                m_cube_state.m_freevars_threshold = m_freevars.size();     
+                m_cube_state.m_psat_threshold = m_config.m_cube_cutoff == adaptive_psat_cutoff ? psat_heur() : DBL_MAX;  // MN. only compute PSAT if enabled
                 m_cube_state.inc_conflict();
                 if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;                
                 continue;
@@ -2100,7 +2102,7 @@ namespace sat {
                 (m_config.m_cube_cutoff == adaptive_psat_cutoff && psat_heur() >= m_cube_state.m_psat_threshold)) {
                 double dec = (1.0 - pow(m_config.m_cube_fraction, depth));
                 m_cube_state.m_freevars_threshold *= dec;
-                m_cube_state.m_psat_threshold *= dec;
+                m_cube_state.m_psat_threshold *= 2.0 - dec;
                 set_conflict();
                 m_cube_state.inc_cutoff();
 #if 0
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 8c7c4d421..b9d4b0132 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -60,6 +60,7 @@ namespace sat {
         m_next_simplify           = 0;
         m_num_checkpoints         = 0;
         m_simplifications         = 0;
+        m_ext                     = 0;
         m_cuber                   = nullptr;
         m_mc.set_solver(this);
     }