diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt
index 341e3eaa7..e89a362ec 100644
--- a/src/math/polysat/CMakeLists.txt
+++ b/src/math/polysat/CMakeLists.txt
@@ -5,8 +5,8 @@ z3_add_component(polysat
     clause_builder.cpp
     conflict.cpp
     constraint.cpp
-    # eq_explain.cpp
-    # explain.cpp
+    eq_explain.cpp
+    explain.cpp
     forbidden_intervals.cpp
     inference_logger.cpp
     justification.cpp
@@ -14,7 +14,7 @@ z3_add_component(polysat
     log.cpp
     op_constraint.cpp
     restart.cpp
-    # saturation.cpp
+    saturation.cpp
     search_state.cpp
     simplify.cpp
     simplify_clause.cpp
@@ -22,7 +22,7 @@ z3_add_component(polysat
     solver.cpp
     ule_constraint.cpp
     umul_ovfl_constraint.cpp
-    # variable_elimination.cpp
+    variable_elimination.cpp
     viable.cpp
   COMPONENT_DEPENDENCIES
     util
diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index bdecde349..3b091c3d2 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -145,9 +145,32 @@ namespace polysat {
 
     void conflict::init(signed_constraint c) {
         SASSERT(empty());
+        set_impl(c);
+        logger().begin_conflict();
+    }
+
+    void conflict::set(signed_constraint c) {
+        reset();
+        set_impl(c);
+    }
+
+    void conflict::set_impl(signed_constraint c) {
         if (c.bvalue(s) == l_false) {
             // boolean conflict
-            NOT_IMPLEMENTED_YET();
+            SASSERT(false);  // fail here to force check when we encounter this case
+            // TODO: if we set() and then log() it will be confusing if this branch is hit.
+            //       ideally the boolean resolution would be done separately afterwards
+            auto* cl = s.m_bvars.reason(c.blit());
+#if 0
+            if (cl)
+                set(*cl);  // why the whole clause? or do we want the boolean resolution?
+            else
+                insert(c);
+#else
+            insert(c);
+            if (cl)
+                resolve_bool(c.blit(), *cl);
+#endif
         } else {
             // conflict due to assignment
             SASSERT(c.bvalue(s) == l_true);
@@ -156,7 +179,6 @@ namespace polysat {
             insert_vars(c);
         }
         SASSERT(!empty());
-        logger().begin_conflict();  // TODO: we often call reset/set so doing this here doesn't really work... make subsequent begins a no-op? or separate init and set? (set could then do reset() internally ... and we only need set() for signed_constraint, not all three variations)
     }
 
     void conflict::init(clause const& cl) {
@@ -239,6 +261,19 @@ namespace polysat {
             m_var_occurrences[v]--;
     }
 
+    void conflict::insert(signed_constraint c, clause_ref lemma) {
+        unsigned const idx = c.blit().to_uint();
+        SASSERT(!contains(c));  // not required, but this case should be checked
+        SASSERT(!m_lemmas.contains(idx));  // not required, but this case should be checked
+        insert(c);
+        m_lemmas.insert(idx, lemma);
+    }
+
+    clause* conflict::side_lemma(sat::literal lit) const {
+        unsigned const idx = lit.to_uint();
+        return m_lemmas.get(idx, {}).get();
+    }
+
     void conflict::resolve_bool(sat::literal lit, clause const& cl) {
         // Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
         //       clause: x \/ u \/ v
@@ -337,8 +372,8 @@ namespace polysat {
         clause_builder lemma(s);
 
         // TODO: is this sound, doing it for each constraint separately?
-        // for (auto c : *this)
-        //     minimize_vars(c);
+        for (auto c : *this)
+            minimize_vars(c);
 
         for (auto c : *this)
             lemma.push(~c);
@@ -354,6 +389,8 @@ namespace polysat {
         logger().log_lemma(lemma);
         logger().end_conflict();
 
+        // TODO: additional lemmas
+
         return lemma.build();
     }
 
diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h
index 7d5a35fa2..142ea4e26 100644
--- a/src/math/polysat/conflict.h
+++ b/src/math/polysat/conflict.h
@@ -76,6 +76,7 @@ TODO:
     - may force backjumping without further conflict resolution (e.g., if applicable lemma was found by global analysis of search state)
     - bailout lemma if no method applies (log these cases in particular because it indicates where we are missing something)
     - force a restart if we get a bailout lemma or non-asserting conflict?
+- store the side lemmas as well (but only those that justify a constraint in the final lemma, recursively)
 - consider case if v is both in vars and bail_vars (do we need to keep it in bail_vars even if we can eliminate it from vars?)
 - Find a way to use resolve_value with forbidden interval lemmas.
   Then get rid of conflict_kind_t::backtrack and m_relevant_vars.
@@ -88,9 +89,9 @@ TODO:
     - or try to find an L(x,y) such that C1 -> L, ..., Cn -> L, and L -> y != b  (under x := a); worst case y != b can work as L
 - minimize_vars... is it sound to do for each constraint separately, like we are doing now?
 
-
 --*/
 #pragma once
+#include "math/polysat/types.h"
 #include "math/polysat/constraint.h"
 #include "math/polysat/inference_logger.h"
 #include <optional>
@@ -128,12 +129,12 @@ namespace polysat {
 
         unsigned_vector m_var_occurrences;  // for each variable, the number of constraints in m_literals that contain it
 
-        // additional lemmas generated during conflict resolution
-        // TODO: we might not need all of these in the end. add only the side lemmas which justify a constraint in the final lemma (recursively)?
-        vector<clause_ref> m_lemmas;
+        // Additional lemmas that justify new constraints generated during conflict resolution
+        u_map<clause_ref> m_lemmas;
 
         conflict_kind_t m_kind = conflict_kind_t::ok;
 
+        void set_impl(signed_constraint c);
         bool minimize_vars(signed_constraint c);
 
     public:
@@ -169,11 +170,17 @@ namespace polysat {
         /** conflict because there is no viable value for the variable v */
         void init(pvar v, bool by_viable_fallback);
 
+        /** replace the current conflict by a single constraint */
+        void set(signed_constraint c);
+
         bool contains(signed_constraint c) const { SASSERT(c); return contains(c.blit()); }
         bool contains(sat::literal lit) const;
         bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); }
         bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; }
 
+        clause* side_lemma(signed_constraint c) const { SASSERT(c); return side_lemma(c.blit()); }
+        clause* side_lemma(sat::literal lit) const;
+
         /**
          * Insert constraint c into conflict state.
          *
@@ -182,6 +189,11 @@ namespace polysat {
          */
         void insert(signed_constraint c);
 
+        /**
+         * Insert constraint c that is justified by the given lemma.
+         */
+        void insert(signed_constraint c, clause_ref lemma);
+
         /** Insert assigned variables of c */
         void insert_vars(signed_constraint c);
 
diff --git a/src/math/polysat/conflict_old.cpp b/src/math/polysat/conflict_old.cpp
index 07ef61247..57f5305b1 100644
--- a/src/math/polysat/conflict_old.cpp
+++ b/src/math/polysat/conflict_old.cpp
@@ -1,3 +1,4 @@
+#if 0
 /*++
 Copyright (c) 2021 Microsoft Corporation
 
@@ -601,3 +602,4 @@ namespace polysat {
         return m_bvar2mark.get(b, false);
     }
 }
+#endif
diff --git a/src/math/polysat/conflict_old.h b/src/math/polysat/conflict_old.h
index ce54f97c5..92fbe5ccf 100644
--- a/src/math/polysat/conflict_old.h
+++ b/src/math/polysat/conflict_old.h
@@ -1,3 +1,4 @@
+#if 0
 /*++
 Copyright (c) 2021 Microsoft Corporation
 
@@ -249,3 +250,4 @@ namespace polysat {
     inline conflict::const_iterator conflict::begin() const { return conflict_iterator::begin(cm(), m_literals); }
     inline conflict::const_iterator conflict::end() const { return conflict_iterator::end(cm(), m_literals); }
 }
+#endif
diff --git a/src/math/polysat/eq_explain.cpp b/src/math/polysat/eq_explain.cpp
index 02274e4e0..8dc20c8e7 100644
--- a/src/math/polysat/eq_explain.cpp
+++ b/src/math/polysat/eq_explain.cpp
@@ -1,3 +1,4 @@
+#if 0
 /*++
 Copyright (c) 2021 Microsoft Corporation
 
@@ -69,3 +70,4 @@ namespace polysat {
     }
 
 }
+#endif
diff --git a/src/math/polysat/eq_explain.h b/src/math/polysat/eq_explain.h
index 30da45da8..bc6a037f3 100644
--- a/src/math/polysat/eq_explain.h
+++ b/src/math/polysat/eq_explain.h
@@ -1,3 +1,4 @@
+#if 0
 /*++
 Copyright (c) 2021 Microsoft Corporation
 
@@ -28,3 +29,4 @@ namespace polysat {
     };
 
 }
+#endif
diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index b7e0ab118..e7f421b2c 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -1,3 +1,4 @@
+#if 0
 /*++
 Copyright (c) 2021 Microsoft Corporation
 
@@ -101,6 +102,14 @@ namespace polysat {
                 core.log_inference(inference_sup("1", v, c2, c1));
                 return l_true;
             case l_undef:
+#if 0
+                core.reset();
+                core.insert(c1);
+                core.insert(c2);
+                core.insert(~c);
+                core.log_inference(inference_sup("1b", v, c2, c1));
+                return l_true;
+#else
                 SASSERT(premises.empty());
                 // Ensure that c is assigned and justified                    
                 premises.push_back(c1);
@@ -115,6 +124,7 @@ namespace polysat {
                 SASSERT_EQ(l_true, c.bvalue(s));
                 SASSERT(c.is_currently_false(s));
                 break;
+#endif
             default:
                 break;
             }
@@ -235,3 +245,4 @@ namespace polysat {
     }
 
 }
+#endif
diff --git a/src/math/polysat/explain.h b/src/math/polysat/explain.h
index 588e80a33..1e830c39c 100644
--- a/src/math/polysat/explain.h
+++ b/src/math/polysat/explain.h
@@ -1,3 +1,4 @@
+#if 0
 /*++
 Copyright (c) 2021 Microsoft Corporation
 
@@ -44,3 +45,4 @@ namespace polysat {
     };
 
 }
+#endif
diff --git a/src/math/polysat/inference_logger.cpp b/src/math/polysat/inference_logger.cpp
index b0af8a8f2..d3bfba069 100644
--- a/src/math/polysat/inference_logger.cpp
+++ b/src/math/polysat/inference_logger.cpp
@@ -60,8 +60,9 @@ namespace polysat {
         for (auto const& c : core) {
             sat::literal const lit = c.blit();
             out_indent() << lit << ": " << c << '\n';
-            // TODO: if justified by a side lemma, print it here
-            // out_indent() << "    justified by: " << lemma << '\n';
+            clause* lemma = core.side_lemma(lit);
+            if (lemma)
+                out_indent() << "    justified by: " << lemma << '\n';
             m_used_constraints.insert(lit.index());
             for (pvar v : c->vars())
                 m_used_vars.insert(v);
diff --git a/src/math/polysat/interval.h b/src/math/polysat/interval.h
index deb03bd41..fac4bdd81 100644
--- a/src/math/polysat/interval.h
+++ b/src/math/polysat/interval.h
@@ -109,7 +109,7 @@ namespace polysat {
             // hi < lo <= lo' <= hi'
             if (lo_val() <= other.lo_val() && other.lo_val() <= other.hi_val())
                 return true;
-            // lo' <= hi' <= hi < lo 
+            // lo' <= hi' <= hi < lo
             if (other.lo_val() <= other.hi_val() && other.hi_val() <= hi_val())
                 return true;
             // hi' <= hi < lo <= lo'
diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index 5f5cb8caa..5b8b9fa62 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -1,3 +1,4 @@
+#if 0
 /*++
 Copyright (c) 2021 Microsoft Corporation
 
@@ -486,3 +487,4 @@ namespace polysat {
     }
 
 }
+#endif
diff --git a/src/math/polysat/saturation.h b/src/math/polysat/saturation.h
index 362656f5d..9cabe6a71 100644
--- a/src/math/polysat/saturation.h
+++ b/src/math/polysat/saturation.h
@@ -1,3 +1,4 @@
+#if 0
 /*++
 Copyright (c) 2021 Microsoft Corporation
 
@@ -110,3 +111,4 @@ namespace polysat {
      */
 
 }
+#endif
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 45869b0d5..2172eeb21 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -17,9 +17,7 @@ Author:
 --*/
 
 #include "math/polysat/solver.h"
-#include "math/polysat/explain.h"
 #include "math/polysat/log.h"
-#include "math/polysat/variable_elimination.h"
 #include "math/polysat/polysat_params.hpp"
 
 // For development; to be removed once the linear solver works well enough
diff --git a/src/math/polysat/variable_elimination.cpp b/src/math/polysat/variable_elimination.cpp
index 74e59d41e..47f759f38 100644
--- a/src/math/polysat/variable_elimination.cpp
+++ b/src/math/polysat/variable_elimination.cpp
@@ -22,9 +22,8 @@ namespace polysat {
         // and kick out all other constraints.
         for (signed_constraint c : core) {
             if (!c->contains_var(v) && c.is_currently_false(s)) {
-                core.reset();
                 core.set(c);
-                core.log_inference("ve_reduction");
+                core.logger().log("ve_reduction");
                 return true;
             }                
         }
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 90e5ff4a1..c1e75ba04 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -635,7 +635,6 @@ namespace polysat {
         auto* e = m_units[v];
         entry* first = e;
         SASSERT(e);
-        core.reset();
         do {
             // Build constraint: upper bound of each interval is not contained in the next interval,
             // using the equivalence:  t \in [l;h[  <=>  t-l < h-l
@@ -670,16 +669,13 @@ namespace polysat {
         core.logger().log(inf_fi(*this, v));
 
         // TODO: should not be here, too general
-        /*
         for (auto c : core) {
             if (c.bvalue(s) == l_false) {
-                core.reset();
                 core.set(~c);
                 core.logger().log("");
                 break;
             }
         }
-        */
 
         return true;
     }