diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index ed44eb642..8600a3d3a 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4459,8 +4459,8 @@ namespace smt {
             if (has_case_splits())
                 return false;
             fcs = final_check();
+            TRACE("opt", tout << (refinalize?"refinalize":"no-op") << " " << fcs << "\n";);
         }
-        TRACE("opt", tout << (refinalize?"refinalize":"no-op") << " " << fcs << "\n";);
         if (fcs == FC_DONE) {
             reset_model();
         }
diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp
index cca8a906c..781150a6a 100644
--- a/src/tactic/sine_filter.cpp
+++ b/src/tactic/sine_filter.cpp
@@ -215,6 +215,8 @@ private:
             visiting = to_visit.back();
             to_visit.pop_back();
             visited.insert(visiting);
+            if (!exp2const.contains(visiting))
+                continue;
             for (func_decl* f : exp2const[visiting]) 
                 for (expr* e : const2exp[f]) {
                     if (!visited.contains(e))