diff --git a/src/math/polysat/conflict2.cpp b/src/math/polysat/conflict2.cpp
index 694c253b3..bc1e95978 100644
--- a/src/math/polysat/conflict2.cpp
+++ b/src/math/polysat/conflict2.cpp
@@ -68,16 +68,21 @@ namespace polysat {
         SASSERT(!empty());
     }
 
-    void conflict2::init(pvar v) {
+    void conflict2::init(pvar v, bool by_viable_fallback) {
         // NOTE: do forbidden interval projection in this method (rather than keeping a separate state like we did before)
         // Option 1: forbidden interval projection
         // Option 2: add all constraints from m_viable + dependent variables
 
-        // TODO: we need to know whether the conflict is from m_viable for m_viable_fallback
-        // - m_viable: standard forbidden interval lemma
-        // - m_viable_fallback: initial conflict is the unsat core of the univariate solver
-        // (a flag on this method might be good enough)
+        if (by_viable_fallback) {
+            // Conflict detected by viable fallback:
+            // initial conflict is the unsat core of the univariate solver
+            signed_constraints unsat_core = s.m_viable_fallback.unsat_core(v);
+            for (auto c : unsat_core)
+                insert(c);
+            return;
+        }
 
+        // TODO:
         // VERIFY(s.m_viable.resolve(v, *this));
         // log_inference(inf_fi_lemma(v));
     }
diff --git a/src/math/polysat/conflict2.h b/src/math/polysat/conflict2.h
index 6d8811994..084db3cd6 100644
--- a/src/math/polysat/conflict2.h
+++ b/src/math/polysat/conflict2.h
@@ -114,7 +114,7 @@ namespace polysat {
         /** conflict because the constraint c is false under current variable assignment */
         void init(signed_constraint c);
         /** conflict because there is no viable value for the variable v */
-        void init(pvar v);
+        void init(pvar v, bool by_viable_fallback = false);
 
         bool contains(signed_constraint c) const { SASSERT(c); return contains(c.blit()); }
         bool contains(sat::literal lit) const;