diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 9c20c5deb..066185aa3 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -170,11 +170,9 @@ namespace smt {
                 if (sk_term != 0) {
                     sk_value = sk_term;
                 }
-                else {
-                    if (m_manager.is_model_value(sk_value))
-                        return false;
-                }
             }
+            if (m_manager.is_model_value(sk_value))
+                return false;
             bindings.set(num_decls - i - 1, sk_value);
         }
         
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index d8f18a123..fea9f9bce 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -102,6 +102,7 @@ namespace smt {
                     return;
                 m_manager.inc_ref(n);
                 m_elems.insert(n, generation);
+                CTRACE("model_finder", m_manager.is_model_value(n), tout << mk_pp(n, m_manager) << "\n";);
                 SASSERT(!m_manager.is_model_value(n));
             }