diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index de5f46892..091c854a8 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -178,6 +178,8 @@ void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
 }
 
 void asserted_formulas::push_scope() {
+    reduce();
+    commit();
     SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.canceled());
     TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n";);
     m_scoped_substitution.push();
@@ -278,8 +280,6 @@ void asserted_formulas::reduce() {
     flush_cache();
     CASSERT("well_sorted",check_well_sorted());
 
-//    display(std::cout);
-//    exit(0);
 }
 
 
diff --git a/src/smt/smt_lookahead.cpp b/src/smt/smt_lookahead.cpp
index 801c97653..363687b1b 100644
--- a/src/smt/smt_lookahead.cpp
+++ b/src/smt/smt_lookahead.cpp
@@ -82,7 +82,7 @@ namespace smt {
         unsigned nf = 0, nc = 0, ns = 0, bound = 2000, n = 0;
         for (bool_var v : vars) {
             if (!ctx.bool_var2expr(v)) continue;
-            literal lit(v, false);			
+            literal lit(v, false);	
             ctx.push_scope();
             ctx.assign(lit, b_justification::mk_axiom(), true);
             ctx.propagate();