diff --git a/src/sat/smt/polysat_core.cpp b/src/sat/smt/polysat_core.cpp
index f3950adf2..73e9c5a6b 100644
--- a/src/sat/smt/polysat_core.cpp
+++ b/src/sat/smt/polysat_core.cpp
@@ -290,6 +290,16 @@ namespace polysat {
         s.ctx.push(push_back_vector(m_prop_queue));
     }
 
+    dependency_vector core::explain_eval(signed_constraint const& sc) { 
+        dependency_vector deps;
+        for (auto v : sc.vars()) 
+            if (is_assigned(v))
+                deps.push_back(m_justification[v]);
+        return deps;
+    }
 
+    lbool core::eval(signed_constraint const& sc) { 
+        throw default_exception("nyi"); 
+    }
 
 }
diff --git a/src/sat/smt/polysat_core.h b/src/sat/smt/polysat_core.h
index 802108ffc..6944c39d8 100644
--- a/src/sat/smt/polysat_core.h
+++ b/src/sat/smt/polysat_core.h
@@ -83,8 +83,8 @@ namespace polysat {
 
         signed_constraint get_constraint(unsigned idx, bool sign);
 
-        lbool eval(signed_constraint sc) { throw default_exception("nyi"); }
-        dependency_vector explain_eval(signed_constraint const& dc) { throw default_exception("nyi"); }
+        lbool eval(signed_constraint const& sc);
+        dependency_vector explain_eval(signed_constraint const& sc);
 
     public:
         core(solver& s);