diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp
index 6b8ff8d63..503abac2f 100644
--- a/src/model/model_core.cpp
+++ b/src/model/model_core.cpp
@@ -88,20 +88,20 @@ void model_core::register_decl(func_decl * d, func_interp * fi) {
 }
 
 void model_core::unregister_decl(func_decl * d) {
-	decl2expr::obj_map_entry * ec = m_interp.find_core(d);
-	if (ec && ec->get_data().m_value != 0) {
-		m_manager.dec_ref(ec->get_data().m_key);
-		m_manager.dec_ref(ec->get_data().m_value);
-		m_interp.remove(d);
+    decl2expr::obj_map_entry * ec = m_interp.find_core(d);
+    if (ec && ec->get_data().m_value != 0) {
+        m_manager.dec_ref(ec->get_data().m_key);
+        m_manager.dec_ref(ec->get_data().m_value);
+        m_interp.remove(d);
         m_const_decls.erase(d);
-		return;
-	}
-
-	decl2finterp::obj_map_entry * ef = m_finterp.find_core(d);
-	if (ef && ef->get_data().m_value != 0) {
-		m_manager.dec_ref(ef->get_data().m_key);
-		dealloc(ef->get_data().m_value);
-		m_finterp.remove(d);
+            return;
+    }
+    
+    decl2finterp::obj_map_entry * ef = m_finterp.find_core(d);
+    if (ef && ef->get_data().m_value != 0) {
+        m_manager.dec_ref(ef->get_data().m_key);
+        dealloc(ef->get_data().m_value);
+        m_finterp.remove(d);
         m_func_decls.erase(d);
-	}
-}
\ No newline at end of file
+    }
+}
diff --git a/src/model/model_core.h b/src/model/model_core.h
index 371106b05..c42451c5a 100644
--- a/src/model/model_core.h
+++ b/src/model/model_core.h
@@ -60,7 +60,7 @@ public:
 
     void register_decl(func_decl * d, expr * v);
     void register_decl(func_decl * f, func_interp * fi);
-	void unregister_decl(func_decl * d);
+    void unregister_decl(func_decl * d);
 
     virtual expr * get_some_value(sort * s) = 0;
 
diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index eaedc470b..8aa6f509e 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -294,6 +294,7 @@ public:
 
     void extract_literals(model& model, expr_ref_vector& fmls) {
         expr_ref val(m);
+        TRACE("qe", tout << fmls << "\n";);
         for (unsigned i = 0; i < fmls.size(); ++i) {
             expr* fml = fmls[i].get(), *nfml, *f1, *f2, *f3;
             SASSERT(m.is_bool(fml));
@@ -404,6 +405,7 @@ public:
                 // TBD other Boolean operations.
             }
         }
+        TRACE("qe", tout << fmls << "\n";);
         m_visited.reset();
     }
 
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 1bfd53597..e378c7fdf 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -909,6 +909,7 @@ namespace qe {
                 num_scopes = 2;
             }
             else {
+				if (level.max() + 2 > m_level) return false;
                 SASSERT(level.max() + 2 <= m_level);
                 num_scopes = m_level - level.max();
                 SASSERT(num_scopes >= 2);
diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp
index bc3585d09..044511c33 100644
--- a/src/tactic/smtlogics/quant_tactics.cpp
+++ b/src/tactic/smtlogics/quant_tactics.cpp
@@ -104,21 +104,12 @@ tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p) {
 }
 
 tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
-#if 0
-    tactic * st = and_then(mk_quant_preprocessor(m),
-                           or_else(try_for(mk_smt_tactic(), 100), 
-                                   try_for(qe::mk_sat_tactic(m), 1000), 
-                                   try_for(mk_smt_tactic(), 1000),
-                                   and_then(mk_qe_tactic(m), mk_smt_tactic())
-                                   ));
-#else
     tactic * st = and_then(mk_quant_preprocessor(m),
                            mk_qe_lite_tactic(m, p),
                            cond(mk_has_quantifier_probe(), 
                                 or_else(mk_qsat_tactic(m, p),
                                         and_then(mk_qe_tactic(m), mk_smt_tactic())),
                                 mk_smt_tactic()));
-#endif
     st->updt_params(p);
     return st;
 }