diff --git a/src/ast/ast_translation.cpp b/src/ast/ast_translation.cpp
index 532795c5c..d4709c077 100644
--- a/src/ast/ast_translation.cpp
+++ b/src/ast/ast_translation.cpp
@@ -196,7 +196,7 @@ ast * ast_translation::process(ast const * _n) {
     SASSERT(m_extra_children_stack.empty());
     
     ++m_num_process;
-    if (m_num_process > (1 << 16)) {
+    if (m_num_process > (1 << 14)) {
         reset_cache();
         m_num_process = 0;
     }
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index bcfb06356..bcd264743 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -915,7 +915,7 @@ void sat2goal::mc::flush_gmc() {
 }
  
 model_converter* sat2goal::mc::translate(ast_translation& translator) {
-    mc* result = alloc(mc, m);
+    mc* result = alloc(mc, translator.to());
     result->m_smc.copy(m_smc);
     result->m_gmc = m_gmc ? dynamic_cast<generic_model_converter*>(m_gmc->translate(translator)) : nullptr;
     for (app* e : m_var2expr) {
@@ -983,6 +983,10 @@ void sat2goal::mc::operator()(expr_ref& fml) {
 }
 
 void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) {
+    if (m_var2expr.get(v, nullptr)) {
+        std::cout << mk_pp(atom, m) << "\n";
+        std::cout << mk_pp(m_var2expr.get(v, nullptr), m) << "\n";
+    }
     VERIFY(!m_var2expr.get(v, nullptr));
     m_var2expr.reserve(v + 1);
     m_var2expr.set(v, atom);
@@ -1038,7 +1042,7 @@ struct sat2goal::imp {
             for (sat::bool_var v = 0; v < num_vars; v++) {
                 checkpoint();                
                 sat::literal l(v, false);
-                if (m_lit2expr.get(l.index())) {
+                if (m_lit2expr.get(l.index()) && !mc->var2expr(v)) {
                     mc->insert(v, to_app(m_lit2expr.get(l.index())), false);
                     SASSERT(m_lit2expr.get((~l).index()));
                 }
diff --git a/src/util/resource_limit.h b/src/util/resource_limit.h
index 3f5c4d520..969953aaf 100644
--- a/src/util/resource_limit.h
+++ b/src/util/resource_limit.h
@@ -1,7 +1,7 @@
 /*++
 Copyright (c) 2006 Microsoft Corporation
 
-Module Name:
+Modulre Name:
 
     resource_limit.h