diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index 5da2f7735..cb74d7c66 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -4027,8 +4027,3 @@ namespace smt {
     }
 }
 
-#ifdef Z3DEBUG
-void pp(code_tree * c) {
-    c->display(std::cout);
-}
-#endif
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index e551f584a..b3273e699 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3370,8 +3370,10 @@ namespace smt {
             if (u.get_rec_funs().empty()) {
                 model_ref mdl;
                 get_model(mdl);
-                for (theory* t : m_theory_set) {
-                    t->validate_model(*mdl);
+                if (mdl.get()) {
+                    for (theory* t : m_theory_set) {
+                        t->validate_model(*mdl);
+                    }
                 }
             }
 #if 0