diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index bcd264743..257cf3b53 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -983,11 +983,7 @@ 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));
+    SASSERT(!m_var2expr.get(v, nullptr));
     m_var2expr.reserve(v + 1);
     m_var2expr.set(v, atom);
     if (aux) {
diff --git a/src/util/resource_limit.h b/src/util/resource_limit.h
index 969953aaf..3f5c4d520 100644
--- a/src/util/resource_limit.h
+++ b/src/util/resource_limit.h
@@ -1,7 +1,7 @@
 /*++
 Copyright (c) 2006 Microsoft Corporation
 
-Modulre Name:
+Module Name:
 
     resource_limit.h