diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index ce92182e5..f81c556ed 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -518,7 +518,7 @@ namespace polysat {
                 break;
             case dd::find_t::empty:
                 m_free_pvars.unassign_var_eh(v);
-                // TODO: get unsat core from univariate solver
+                auto core = m_viable_fallback.unsat_core(v);  // TODO: add constraints from unsat_core to conflict
                 set_conflict(v);
                 return;
             }
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 4b7469136..4175aa6c3 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -791,5 +791,14 @@ namespace polysat {
             return dd::find_t::empty;
         }
     }
+
+    signed_constraints viable_fallback::unsat_core(pvar v) {
+        signed_constraints cs;
+        for (unsigned dep : m_usolver[v]->unsat_core()) {
+            cs.push_back(m_constraints[v][dep]);
+        }
+        return cs;
+    }
+
 }
 
diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h
index 043c764b2..f64fe19ff 100644
--- a/src/math/polysat/viable.h
+++ b/src/math/polysat/viable.h
@@ -211,7 +211,7 @@ namespace polysat {
         // bool check_value(pvar v, rational const& val);
 
         dd::find_t find_viable(pvar v, rational& out_val);
-        // TODO: get unsat core
+        signed_constraints unsat_core(pvar v);
     };
 
 }