diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt
index 7251c2c5b..ddc5e7edc 100644
--- a/src/math/polysat/CMakeLists.txt
+++ b/src/math/polysat/CMakeLists.txt
@@ -3,7 +3,7 @@ z3_add_component(polysat
     boolean.cpp
     clause.cpp
     clause_builder.cpp
-    conflict_core.cpp
+    conflict.cpp
     constraint.cpp
     explain.cpp
     forbidden_intervals.cpp
diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict.cpp
similarity index 85%
rename from src/math/polysat/conflict_core.cpp
rename to src/math/polysat/conflict.cpp
index ef8046beb..d6aadc09e 100644
--- a/src/math/polysat/conflict_core.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -21,7 +21,7 @@ TODO: If we have e.g. 4x+y=2 and y=0, then we have a conflict no matter the valu
 
 --*/
 
-#include "math/polysat/conflict_core.h"
+#include "math/polysat/conflict.h"
 #include "math/polysat/solver.h"
 #include "math/polysat/log.h"
 #include "math/polysat/log_helper.h"
@@ -33,7 +33,7 @@ TODO: If we have e.g. 4x+y=2 and y=0, then we have a conflict no matter the valu
 
 namespace polysat {
 
-    conflict_core::conflict_core(solver& s) {
+    conflict::conflict(solver& s) {
         m_solver = &s;
         ex_engines.push_back(alloc(ex_polynomial_superposition));
         for (auto* engine : ex_engines)
@@ -44,11 +44,11 @@ namespace polysat {
             engine->set_solver(s);
     }
 
-    conflict_core::~conflict_core() {}
+    conflict::~conflict() {}
 
-    constraint_manager& conflict_core::cm() const { return s().m_constraints; }
+    constraint_manager& conflict::cm() const { return s().m_constraints; }
 
-    std::ostream& conflict_core::display(std::ostream& out) const {
+    std::ostream& conflict::display(std::ostream& out) const {
         char const* sep = "";
         for (auto c : *this) 
             out << sep << c->bvar2string() << " " << c, sep = " ; ";
@@ -59,7 +59,7 @@ namespace polysat {
         return out;
     }
 
-    void conflict_core::reset() {
+    void conflict::reset() {
         for (auto c : *this)
             unset_mark(c);
         m_constraints.reset();
@@ -75,7 +75,7 @@ namespace polysat {
     * The constraint is false under the current assignment of variables.
     * The core is then the conjuction of this constraint and assigned variables.
     */
-    void conflict_core::set(signed_constraint c) {
+    void conflict::set(signed_constraint c) {
         LOG("Conflict: " << c);
         SASSERT(empty());
         c->set_var_dependent();
@@ -91,7 +91,7 @@ namespace polysat {
     * A consistent approach could be to add these constraints to the core and then also include the
     * variable assignments.
     */
-    void conflict_core::set(pvar v) {
+    void conflict::set(pvar v) {
         LOG("Conflict: v" << v);
         SASSERT(empty());
         m_conflict_var = v;
@@ -102,7 +102,7 @@ namespace polysat {
         SASSERT(!empty());
     }
 
-    void conflict_core::set(clause const& cl) {
+    void conflict::set(clause const& cl) {
         LOG("Conflict: " << cl);
         SASSERT(empty());
         for (auto lit : cl) {
@@ -113,7 +113,7 @@ namespace polysat {
         SASSERT(!empty());
     }
 
-    void conflict_core::insert(signed_constraint c) {
+    void conflict::insert(signed_constraint c) {
         LOG("inserting: " << c);
         // Skip trivial constraints
         // (e.g., constant ones such as "4 > 1"... only true ones should appear, otherwise the lemma would be a tautology)
@@ -128,12 +128,12 @@ namespace polysat {
             m_constraints.push_back(c);
     }
 
-    void conflict_core::insert(signed_constraint c, vector<signed_constraint> premises) {
+    void conflict::insert(signed_constraint c, vector<signed_constraint> premises) {
         insert(c);
         m_saturation_premises.insert(c, std::move(premises));  // TODO: map doesn't have move-insertion, so this still copies the vector.
     }
 
-    void conflict_core::remove(signed_constraint c) {
+    void conflict::remove(signed_constraint c) {
         unset_mark(c);       
         if (c->has_bvar()) {
             SASSERT(std::count(m_constraints.begin(), m_constraints.end(), c) == 0);
@@ -143,18 +143,18 @@ namespace polysat {
             m_constraints.erase(c);
     }
 
-    void conflict_core::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> c_new_premises) {
+    void conflict::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> c_new_premises) {
         remove(c_old);
         insert(c_new, c_new_premises);
     }
 
-    void conflict_core::set_bailout() {
+    void conflict::set_bailout() {
         SASSERT(!is_bailout());
         m_bailout = true;
         s().m_stats.m_num_bailouts++;
     }
 
-    void conflict_core::resolve(constraint_manager const& m, sat::bool_var var, clause const& cl) {
+    void conflict::resolve(constraint_manager const& m, sat::bool_var var, clause const& cl) {
         // Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
         //       clause: x \/ u \/ v
         //       resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v
@@ -185,7 +185,7 @@ namespace polysat {
     }
 
     /** If the constraint c is a temporary constraint derived by core saturation, insert it (and recursively, its premises) into \Gamma */
-    void conflict_core::keep(signed_constraint c) {
+    void conflict::keep(signed_constraint c) {
         if (!c->has_bvar()) {
             remove(c);
             cm().ensure_bvar(c.get());
@@ -215,7 +215,7 @@ namespace polysat {
             s().assign_bool(s().level(*lemma), c.blit(), lemma.get(), nullptr);
     }
 
-    clause_builder conflict_core::build_lemma() {
+    clause_builder conflict::build_lemma() {
         LOG_H3("Build lemma from core");
         LOG("core: " << *this);
         clause_builder lemma(s());
@@ -244,7 +244,7 @@ namespace polysat {
     }
 
 
-    bool conflict_core::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) {
+    bool conflict::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) {
         // NOTE:
         // In the "standard" case where "v = val" is on the stack:
         //      - cjust_v contains true constraints
@@ -281,7 +281,7 @@ namespace polysat {
         return false;
     }
 
-    bool conflict_core::try_eliminate(pvar v) {       
+    bool conflict::try_eliminate(pvar v) {       
         bool has_v = false;
         for (auto c : *this)
             has_v |= c->contains_var(v);
@@ -293,14 +293,14 @@ namespace polysat {
         return false;
     }
 
-    bool conflict_core::try_saturate(pvar v) {
+    bool conflict::try_saturate(pvar v) {
         for (auto* engine : inf_engines)
             if (engine->perform(v, *this))
                 return true;
         return false;
     }
 
-    void conflict_core::set_mark(signed_constraint c) {
+    void conflict::set_mark(signed_constraint c) {
         if (c->is_marked())
             return;
         c->set_mark();
@@ -315,7 +315,7 @@ namespace polysat {
         }
     }
 
-    void conflict_core::unset_mark(signed_constraint c) {
+    void conflict::unset_mark(signed_constraint c) {
         if (!c->is_marked())
             return;
         c->unset_mark();
@@ -328,46 +328,46 @@ namespace polysat {
         }
     }
 
-    void conflict_core::inc_pref(pvar v) {
+    void conflict::inc_pref(pvar v) {
         if (v >= m_pvar2count.size())
             m_pvar2count.resize(v + 1);
         m_pvar2count[v]++;
     }
 
-    void conflict_core::dec_pref(pvar v) {
+    void conflict::dec_pref(pvar v) {
         SASSERT(m_pvar2count[v] > 0);
         m_pvar2count[v]--;
     }
 
-    bool conflict_core::is_pmarked(pvar v) const {
+    bool conflict::is_pmarked(pvar v) const {
         return m_pvar2count.get(v, 0) > 0;
     }
 
-    void conflict_core::set_bmark(sat::bool_var b) {
+    void conflict::set_bmark(sat::bool_var b) {
         if (b >= m_bvar2mark.size())
             m_bvar2mark.resize(b + 1);
         SASSERT(!m_bvar2mark[b]);
         m_bvar2mark[b] = true;
     }
 
-    void conflict_core::unset_bmark(sat::bool_var b) {
+    void conflict::unset_bmark(sat::bool_var b) {
         SASSERT(m_bvar2mark[b]);
         m_bvar2mark[b] = false;
     }
 
-    bool conflict_core::is_bmarked(sat::bool_var b) const {
+    bool conflict::is_bmarked(sat::bool_var b) const {
         return m_bvar2mark.get(b, false);
     }
 
-    bool conflict_core::contains_literal(sat::literal lit) const {
+    bool conflict::contains_literal(sat::literal lit) const {
         return m_literals.contains(lit.to_uint());
     }
 
-    void conflict_core::insert_literal(sat::literal lit) {
+    void conflict::insert_literal(sat::literal lit) {
         m_literals.insert(lit.to_uint());
     }
 
-    void conflict_core::remove_literal(sat::literal lit) {
+    void conflict::remove_literal(sat::literal lit) {
         m_literals.remove(lit.to_uint());
     }
 
diff --git a/src/math/polysat/conflict_core.h b/src/math/polysat/conflict.h
similarity index 80%
rename from src/math/polysat/conflict_core.h
rename to src/math/polysat/conflict.h
index 0e40b1ef5..13bf23a40 100644
--- a/src/math/polysat/conflict_core.h
+++ b/src/math/polysat/conflict.h
@@ -22,10 +22,10 @@ namespace polysat {
     class explainer;
     class inference_engine;
     class variable_elimination_engine;
-    class conflict_core_iterator;
+    class conflict_iterator;
 
     /** Conflict state, represented as core (~negation of clause). */
-    class conflict_core {
+    class conflict {
         signed_constraints m_constraints;   // new constraints used as premises
         indexed_uint_set m_literals;        // set of boolean literals in the conflict
         uint_set m_vars;                    // variable assignments used as premises
@@ -62,8 +62,8 @@ namespace polysat {
         // ptr_addr_map<constraint, vector<signed_constraint>> m_saturation_premises;
         map<signed_constraint, vector<signed_constraint>, obj_hash<signed_constraint>, default_eq<signed_constraint>> m_saturation_premises;
     public:
-        conflict_core(solver& s);
-        ~conflict_core();
+        conflict(solver& s);
+        ~conflict();
 
         pvar conflict_var() const { return m_conflict_var; }
 
@@ -109,18 +109,18 @@ namespace polysat {
         bool try_eliminate(pvar v);
         bool try_saturate(pvar v);
 
-        using const_iterator = conflict_core_iterator;
+        using const_iterator = conflict_iterator;
         const_iterator begin() const;
         const_iterator end() const;
 
         std::ostream& display(std::ostream& out) const;
     };
 
-    inline std::ostream& operator<<(std::ostream& out, conflict_core const& c) { return c.display(out); }
+    inline std::ostream& operator<<(std::ostream& out, conflict const& c) { return c.display(out); }
 
 
-    class conflict_core_iterator {
-        friend class conflict_core;
+    class conflict_iterator {
+        friend class conflict;
 
         using it1_t = signed_constraints::const_iterator;
         using it2_t = indexed_uint_set::iterator;
@@ -130,14 +130,14 @@ namespace polysat {
         it1_t m_end1;
         it2_t m_it2;
 
-        conflict_core_iterator(constraint_manager& cm, it1_t it1, it1_t end1, it2_t it2):
+        conflict_iterator(constraint_manager& cm, it1_t it1, it1_t end1, it2_t it2):
             m_cm(&cm), m_it1(it1), m_end1(end1), m_it2(it2) {}
 
-        static conflict_core_iterator begin(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
+        static conflict_iterator begin(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
             return {cm, cs.begin(), cs.end(), lits.begin()};
         }
 
-        static conflict_core_iterator end(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
+        static conflict_iterator end(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
             return {cm, cs.end(), cs.end(), lits.end()};
         }
 
@@ -148,7 +148,7 @@ namespace polysat {
         using reference = signed_constraint const&;
         using iterator_category = std::input_iterator_tag;
 
-        conflict_core_iterator& operator++() {
+        conflict_iterator& operator++() {
             if (m_it1 != m_end1)
                 ++m_it1;
             else
@@ -163,14 +163,14 @@ namespace polysat {
                 return m_cm->lookup(sat::to_literal(*m_it2));
         }
 
-        bool operator==(conflict_core_iterator const& other) const {
+        bool operator==(conflict_iterator const& other) const {
             return m_it1 == other.m_it1 && m_it2 == other.m_it2;
         }
 
-        bool operator!=(conflict_core_iterator const& other) const { return !operator==(other); }
+        bool operator!=(conflict_iterator const& other) const { return !operator==(other); }
     };
 
 
-    inline conflict_core::const_iterator conflict_core::begin() const { return conflict_core_iterator::begin(cm(), m_constraints, m_literals); }
-    inline conflict_core::const_iterator conflict_core::end() const { return conflict_core_iterator::end(cm(), m_constraints, m_literals); }
+    inline conflict::const_iterator conflict::begin() const { return conflict_iterator::begin(cm(), m_constraints, m_literals); }
+    inline conflict::const_iterator conflict::end() const { return conflict_iterator::end(cm(), m_constraints, m_literals); }
 }
diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index 08a36a31b..2e69f8bd2 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -274,6 +274,7 @@ namespace polysat {
             if (!s.is_assigned(other_v)) {
                 s.add_watch({this, is_positive}, other_v);
                 std::swap(vars()[idx], vars()[i]);
+               // narrow(s, is_positive);
                 return true;
             }
         }
diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index 2cf93e102..55af07c83 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -46,7 +46,7 @@ namespace polysat {
 
     // c2 ... constraint that is currently false
     // Try to replace it with a new false constraint (derived from superposition with a true constraint)
-    signed_constraint ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict_core& core) {
+    signed_constraint ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict& core) {
         for (auto c1 : core) {
             if (!is_positive_equality_over(v, c1))
                 continue;
@@ -67,7 +67,7 @@ namespace polysat {
 
     // TODO(later): check superposition into disequality again (see notes)
     // true = done, false = abort, undef = continue
-    lbool ex_polynomial_superposition::try_explain1(pvar v, conflict_core& core) {
+    lbool ex_polynomial_superposition::try_explain1(pvar v, conflict& core) {
         for (auto c2 : core) {
             if (!is_positive_equality_over(v, c2))
                 continue;
@@ -92,7 +92,7 @@ namespace polysat {
         return l_false;
     }
 
-    void ex_polynomial_superposition::reduce_by(pvar v, conflict_core& core) {
+    void ex_polynomial_superposition::reduce_by(pvar v, conflict& core) {
         //return;
         bool progress = true;
         while (progress) {
@@ -106,7 +106,7 @@ namespace polysat {
         }
     }
 
-    bool ex_polynomial_superposition::reduce_by(pvar v, signed_constraint eq, conflict_core& core) {
+    bool ex_polynomial_superposition::reduce_by(pvar v, signed_constraint eq, conflict& core) {
         pdd p = eq->to_ule().p();
         for (auto c : core) {
             if (c == eq)
@@ -136,7 +136,7 @@ namespace polysat {
         return false;
     }
 
-    bool ex_polynomial_superposition::try_explain(pvar v, conflict_core& core) {
+    bool ex_polynomial_superposition::try_explain(pvar v, conflict& core) {
         LOG_H3("Trying polynomial superposition...");
         reduce_by(v, core);
         lbool result = l_undef;
diff --git a/src/math/polysat/explain.h b/src/math/polysat/explain.h
index 80089d161..fa61b55f4 100644
--- a/src/math/polysat/explain.h
+++ b/src/math/polysat/explain.h
@@ -12,7 +12,7 @@ Author:
 
 --*/
 #pragma once
-#include "math/polysat/conflict_core.h"
+#include "math/polysat/conflict.h"
 #include "math/polysat/constraint.h"
 #include "math/polysat/clause_builder.h"
 #include "math/polysat/interval.h"
@@ -22,26 +22,26 @@ namespace polysat {
     class solver;
 
     class explainer {
-        friend class conflict_core;
+        friend class conflict;
         solver* m_solver = nullptr;
         void set_solver(solver& s) { m_solver = &s; }
     protected:
         solver& s() { return *m_solver; }
     public:
         virtual ~explainer() {}
-        virtual bool try_explain(pvar v, /* vector<signed_constraint> const& cjust_v, */ conflict_core& core) = 0;
+        virtual bool try_explain(pvar v, /* vector<signed_constraint> const& cjust_v, */ conflict& core) = 0;
     };
 
     class ex_polynomial_superposition : public explainer {
     private:
         bool is_positive_equality_over(pvar v, signed_constraint const& c);
         signed_constraint resolve1(pvar v, signed_constraint c1, signed_constraint c2);
-        signed_constraint find_replacement(signed_constraint c2, pvar v, conflict_core& core);
-        void reduce_by(pvar v, conflict_core& core);
-        bool reduce_by(pvar, signed_constraint c, conflict_core& core);
-        lbool try_explain1(pvar v, conflict_core& core);
+        signed_constraint find_replacement(signed_constraint c2, pvar v, conflict& core);
+        void reduce_by(pvar v, conflict& core);
+        bool reduce_by(pvar, signed_constraint c, conflict& core);
+        lbool try_explain1(pvar v, conflict& core);
     public:
-        bool try_explain(pvar v, conflict_core& core) override;
+        bool try_explain(pvar v, conflict& core) override;
     };
 
 
@@ -54,7 +54,7 @@ namespace polysat {
     class conflict_explainer {
         solver& m_solver;
 
-        // conflict_core m_conflict;
+        // conflict m_conflict;
         vector<constraint> m_new_assertions;  // to be inserted into Gamma (conclusions from saturation)
 
         scoped_ptr_vector<inference_engine> inference_engines;
@@ -64,7 +64,7 @@ namespace polysat {
         // Gamma
         // search_state& search() { return m_solver.m_search; }
         // Core
-        // conflict_core& conflict() { return m_solver.m_conflict; }
+        // conflict& conflict() { return m_solver.m_conflict; }
     public:
         /** Create empty conflict */
         conflict_explainer(solver& s);
diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp
index d9062bfb7..b2df96dbc 100644
--- a/src/math/polysat/forbidden_intervals.cpp
+++ b/src/math/polysat/forbidden_intervals.cpp
@@ -72,7 +72,7 @@ namespace polysat {
     * We assume that neg_cond is a consequence of src that  
     * does not mention the variable v to be eliminated.
     */
-    void forbidden_intervals::full_interval_conflict(signed_constraint src, signed_constraint neg_cond, conflict_core& core) {
+    void forbidden_intervals::full_interval_conflict(signed_constraint src, signed_constraint neg_cond, conflict& core) {
         SASSERT(neg_cond);
         core.reset();
         core.insert(~neg_cond);
@@ -80,7 +80,7 @@ namespace polysat {
         core.set_bailout();
     }
 
-    bool forbidden_intervals::perform(solver& s, pvar v, vector<signed_constraint> const& just, conflict_core& core) {
+    bool forbidden_intervals::perform(solver& s, pvar v, vector<signed_constraint> const& just, conflict& core) {
         
         // Extract forbidden intervals from conflicting constraints
         vector<fi_record> records;
diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h
index fd927fb9f..f3e05f580 100644
--- a/src/math/polysat/forbidden_intervals.h
+++ b/src/math/polysat/forbidden_intervals.h
@@ -20,9 +20,9 @@ Author:
 namespace polysat {
 
     class forbidden_intervals {
-        void full_interval_conflict(signed_constraint c, signed_constraint neg_cond, conflict_core& core);
+        void full_interval_conflict(signed_constraint c, signed_constraint neg_cond, conflict& core);
         bool get_interval(solver& s, signed_constraint const& c, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond);
     public:
-        bool perform(solver& s, pvar v, vector<signed_constraint> const& just, conflict_core& core);
+        bool perform(solver& s, pvar v, vector<signed_constraint> const& just, conflict& core);
     };
 }
diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index b890b8258..50153256e 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -29,7 +29,7 @@ TODO: when we check that 'x' is "unary":
 
 namespace polysat {
     
-    bool inf_saturate::perform(pvar v, conflict_core& core) {
+    bool inf_saturate::perform(pvar v, conflict& core) {
         for (auto c1 : core) {
             if (!c1->is_ule())
                 continue;
@@ -57,7 +57,7 @@ namespace polysat {
     * Propagate c. It is added to reason and core all other literals in reason are false in current stack.
     * The lemmas outlined in the rules are valid and therefore c is implied.
     */
-    bool inf_saturate::propagate(conflict_core& core, inequality const& crit1, inequality const& crit2, signed_constraint& c, vector<signed_constraint>& new_constraints) {
+    bool inf_saturate::propagate(conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint& c, vector<signed_constraint>& new_constraints) {
         bool crit1_false = crit1.as_signed_constraint().is_currently_false(s());
         bool crit2_false = crit2.as_signed_constraint().is_currently_false(s());
         if (!crit1_false && !crit2_false)
@@ -83,7 +83,7 @@ namespace polysat {
         return true;
     }
 
-    bool inf_saturate::propagate(conflict_core& core, inequality const& crit1, inequality const& crit2, bool is_strict, pdd const& lhs, pdd const& rhs, vector<signed_constraint>& new_constraints) {
+    bool inf_saturate::propagate(conflict& core, inequality const& crit1, inequality const& crit2, bool is_strict, pdd const& lhs, pdd const& rhs, vector<signed_constraint>& new_constraints) {
         signed_constraint c = ineq(is_strict, lhs, rhs);
         return propagate(core, crit1, crit2, c, new_constraints);
     }
@@ -263,7 +263,7 @@ namespace polysat {
      *  [x] zx > yx  ==>  Ω*(x,y) \/ z > y
      *  [x] yx <= zx  ==>  Ω*(x,y) \/ y <= z \/ x = 0
      */
-    bool inf_saturate::try_ugt_x(pvar v, conflict_core& core, inequality const& c) {
+    bool inf_saturate::try_ugt_x(pvar v, conflict& core, inequality const& c) {
         pdd x = s().var(v);
         pdd y = x;
         pdd z = x;
@@ -283,7 +283,7 @@ namespace polysat {
 
     /// [y] z' <= y /\ zx > yx  ==>  Ω*(x,y) \/ zx > z'x
     /// [y] z' <= y /\ yx <= zx  ==>  Ω*(x,y) \/ z'x <= zx
-    bool inf_saturate::try_ugt_y(pvar v, conflict_core& core, inequality const& le_y, inequality const& yx_l_zx, pdd const& x, pdd const& z) {
+    bool inf_saturate::try_ugt_y(pvar v, conflict& core, inequality const& le_y, inequality const& yx_l_zx, pdd const& x, pdd const& z) {
         pdd const y = s().var(v);
 
         SASSERT(is_l_v(v, le_y));
@@ -301,7 +301,7 @@ namespace polysat {
         return propagate(core, le_y, yx_l_zx, yx_l_zx.is_strict || le_y.is_strict, z_prime * x, z * x, new_constraints);
     }
 
-    bool inf_saturate::try_ugt_y(pvar v, conflict_core& core, inequality const& c) {
+    bool inf_saturate::try_ugt_y(pvar v, conflict& core, inequality const& c) {
         if (!is_l_v(v, c))
             return false;
         pdd x = s().var(v);
@@ -319,7 +319,7 @@ namespace polysat {
 
     /// [x]  y <= ax /\ x <= z  (non-overflow case)
     ///     ==>   Ω*(a, z)  \/  y <= az
-    bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict_core& core, inequality const& c) {
+    bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& c) {
         if (!is_g_v(x, c))
             return false;
         pdd y = s().var(x);
@@ -334,7 +334,7 @@ namespace polysat {
         return false;
     }
 
-    bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict_core& core, inequality const& x_l_z, inequality const& y_l_ax, pdd const& a, pdd const& y) {
+    bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& x_l_z, inequality const& y_l_ax, pdd const& a, pdd const& y) {
 
         SASSERT(is_g_v(x, x_l_z));
         SASSERT(verify_Y_l_Ax(x, y_l_ax, a, y));
@@ -351,7 +351,7 @@ namespace polysat {
 
     /// [z] z <= y' /\ zx > yx  ==>  Ω*(x,y') \/ y'x > yx
     /// [z] z <= y' /\ yx <= zx  ==>  Ω*(x,y') \/ yx <= y'x
-    bool inf_saturate::try_ugt_z(pvar z, conflict_core& core, inequality const& c) {
+    bool inf_saturate::try_ugt_z(pvar z, conflict& core, inequality const& c) {
         if (!is_g_v(z, c))
             return false;
         pdd y = s().var(z);
@@ -366,7 +366,7 @@ namespace polysat {
         return false;
     }
 
-    bool inf_saturate::try_ugt_z(pvar z, conflict_core& core, inequality const& z_l_y, inequality const& yx_l_zx, pdd const& x, pdd const& y) {
+    bool inf_saturate::try_ugt_z(pvar z, conflict& core, inequality const& z_l_y, inequality const& yx_l_zx, pdd const& x, pdd const& y) {
         SASSERT(is_g_v(z, z_l_y));
         SASSERT(verify_YX_l_zX(z, yx_l_zx, x, y));
         pdd const& y_prime = z_l_y.rhs;
diff --git a/src/math/polysat/saturation.h b/src/math/polysat/saturation.h
index 5d19c8c5c..612f7b3a6 100644
--- a/src/math/polysat/saturation.h
+++ b/src/math/polysat/saturation.h
@@ -12,7 +12,7 @@ Author:
 
 --*/
 #pragma once
-#include "math/polysat/conflict_core.h"
+#include "math/polysat/conflict.h"
 
 namespace polysat {
 
@@ -20,7 +20,7 @@ namespace polysat {
     class constraint_manager;
 
     class inference_engine {
-        friend class conflict_core;
+        friend class conflict;
         solver* m_solver = nullptr;
         void set_solver(solver& s) { m_solver = &s; }
     protected:
@@ -31,7 +31,7 @@ namespace polysat {
          *  Derive new constraints from constraints containing the variable v (i.e., at least one premise must contain v).
          *  Returns true if a new constraint was added to the core.
          */
-        virtual bool perform(pvar v, conflict_core& core) = 0;
+        virtual bool perform(pvar v, conflict& core) = 0;
     };
 
     class inf_saturate : public inference_engine {
@@ -40,19 +40,19 @@ namespace polysat {
         void push_omega(vector<signed_constraint>& new_constraints, pdd const& x, pdd const& y);
         void push_omega_bisect(vector<signed_constraint>& new_constraints, pdd const& x, rational x_max, pdd const& y, rational y_max);
         signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs);
-        bool propagate(conflict_core& core, inequality const& crit1, inequality const& crit2, signed_constraint& c, vector<signed_constraint>& new_constraints);
-        bool propagate(conflict_core& core, inequality const& crit1, inequality const& crit2, bool strict, pdd const& lhs, pdd const& rhs, vector<signed_constraint>& new_constraints);
+        bool propagate(conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint& c, vector<signed_constraint>& new_constraints);
+        bool propagate(conflict& core, inequality const& crit1, inequality const& crit2, bool strict, pdd const& lhs, pdd const& rhs, vector<signed_constraint>& new_constraints);
 
-        bool try_ugt_x(pvar v, conflict_core& core, inequality const& c);
+        bool try_ugt_x(pvar v, conflict& core, inequality const& c);
 
-        bool try_ugt_y(pvar v, conflict_core& core, inequality const& c);
-        bool try_ugt_y(pvar v, conflict_core& core, inequality const& l_y, inequality const& yx_l_zx, pdd const& x, pdd const& z);
+        bool try_ugt_y(pvar v, conflict& core, inequality const& c);
+        bool try_ugt_y(pvar v, conflict& core, inequality const& l_y, inequality const& yx_l_zx, pdd const& x, pdd const& z);
 
-        bool try_y_l_ax_and_x_l_z(pvar x, conflict_core& core, inequality const& c);
-        bool try_y_l_ax_and_x_l_z(pvar x, conflict_core& core, inequality const& x_l_z, inequality const& y_l_ax, pdd const& a, pdd const& y);
+        bool try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& c);
+        bool try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& x_l_z, inequality const& y_l_ax, pdd const& a, pdd const& y);
             
-        bool try_ugt_z(pvar z, conflict_core& core, inequality const& c);
-        bool try_ugt_z(pvar z, conflict_core& core, inequality const& x_l_z0, inequality const& yz_l_xz, pdd const& y, pdd const& x);
+        bool try_ugt_z(pvar z, conflict& core, inequality const& c);
+        bool try_ugt_z(pvar z, conflict& core, inequality const& x_l_z0, inequality const& yz_l_xz, pdd const& y, pdd const& x);
 
         // c := lhs ~ v 
         //  where ~ is < or <=         
@@ -90,7 +90,7 @@ namespace polysat {
 
     public:
 
-        bool perform(pvar v, conflict_core& core) override;
+        bool perform(pvar v, conflict& core) override;
     };
 
     /*
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 22becc979..a36e5b9de 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -21,7 +21,7 @@ Author:
 #include "util/statistics.h"
 #include "util/params.h"
 #include "math/polysat/boolean.h"
-#include "math/polysat/conflict_core.h"
+#include "math/polysat/conflict.h"
 #include "math/polysat/constraint.h"
 #include "math/polysat/clause_builder.h"
 #include "math/polysat/explain.h"
@@ -52,7 +52,7 @@ namespace polysat {
         friend class signed_constraint;
         friend class clause;
         friend class clause_builder;
-        friend class conflict_core;
+        friend class conflict;
         friend class conflict_explainer;
         friend class explainer;
         friend class inference_engine;
@@ -73,7 +73,7 @@ namespace polysat {
         small_object_allocator   m_alloc;
         poly_dep_manager         m_dm;
         linear_solver            m_linear_solver;
-        conflict_core            m_conflict;        
+        conflict                 m_conflict;        
         bool_var_manager         m_bvars;       // Map boolean variables to constraints
         var_queue                m_free_pvars;  // free poly vars
         stats                    m_stats;
diff --git a/src/math/polysat/variable_elimination.cpp b/src/math/polysat/variable_elimination.cpp
index 31f9e7047..8d6705fb5 100644
--- a/src/math/polysat/variable_elimination.cpp
+++ b/src/math/polysat/variable_elimination.cpp
@@ -17,7 +17,7 @@ Author:
 
 namespace polysat {
 
-    bool ve_reduction::perform(solver& s, pvar v, conflict_core& core) {
+    bool ve_reduction::perform(solver& s, pvar v, conflict& core) {
         // without any further hints, we just do core reduction with the stronger premise "C contains a c' that evaluates to false",
         // and kick out all other constraints.
         auto pred = [&s, v](signed_constraint c) -> bool {
diff --git a/src/math/polysat/variable_elimination.h b/src/math/polysat/variable_elimination.h
index 391d3b28d..160580a66 100644
--- a/src/math/polysat/variable_elimination.h
+++ b/src/math/polysat/variable_elimination.h
@@ -12,7 +12,7 @@ Author:
 
 --*/
 #pragma once
-#include "math/polysat/conflict_core.h"
+#include "math/polysat/conflict.h"
 
 namespace polysat {
 
@@ -21,12 +21,12 @@ namespace polysat {
     class variable_elimination_engine {
     public:
         virtual ~variable_elimination_engine() {}
-        virtual bool perform(solver& s, pvar v, conflict_core& core) = 0;
+        virtual bool perform(solver& s, pvar v, conflict& core) = 0;
     };
 
     class ve_reduction : public variable_elimination_engine {
     public:
-        bool perform(solver& s, pvar v, conflict_core& core) override;
+        bool perform(solver& s, pvar v, conflict& core) override;
     };
 
 }