diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index ac332d362..f7b9e7749 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Extension for cardinality and xor reasoning.
+    Extension for cardinality and xr reasoning.
 
 Author:
 
@@ -47,14 +47,14 @@ namespace sat {
         return static_cast<pb const&>(*this);
     }
 
-    ba_solver::xor& ba_solver::constraint::to_xor() {
-        SASSERT(is_xor());
-        return static_cast<xor&>(*this);
+    ba_solver::xr& ba_solver::constraint::to_xr() {
+        SASSERT(is_xr());
+        return static_cast<xr&>(*this);
     }
 
-    ba_solver::xor const& ba_solver::constraint::to_xor() const{
-        SASSERT(is_xor());
-        return static_cast<xor const&>(*this);
+    ba_solver::xr const& ba_solver::constraint::to_xr() const{
+        SASSERT(is_xr());
+        return static_cast<xr const&>(*this);
     }
 
     std::ostream& operator<<(std::ostream& out, ba_solver::constraint const& cnstr) {
@@ -77,8 +77,8 @@ namespace sat {
             out << " >= " << p.k();
             break;
         }
-        case ba_solver::xor_t: {
-            ba_solver::xor const& x = cnstr.to_xor();
+        case ba_solver::xr_t: {
+            ba_solver::xr const& x = cnstr.to_xr();
             for (unsigned i = 0; i < x.size(); ++i) {
                 out << x[i] << " ";
                 if (i + 1 < x.size()) out << "x ";
@@ -187,22 +187,22 @@ namespace sat {
 
 
     // -----------------------------------
-    // xor
+    // xr
     
-    ba_solver::xor::xor(unsigned id, literal_vector const& lits):
-    constraint(xor_t, id, null_literal, lits.size(), get_obj_size(lits.size())) {
+    ba_solver::xr::xr(unsigned id, literal_vector const& lits):
+    constraint(xr_t, id, null_literal, lits.size(), get_obj_size(lits.size())) {
         for (unsigned i = 0; i < size(); ++i) {
             m_lits[i] = lits[i];
         }
     }
 
-    bool ba_solver::xor::is_watching(literal l) const {
+    bool ba_solver::xr::is_watching(literal l) const {
         return 
             l == (*this)[0] || l == (*this)[1] ||
             ~l == (*this)[0] || ~l == (*this)[1];            
     }
 
-    bool ba_solver::xor::well_formed() const {
+    bool ba_solver::xr::well_formed() const {
         uint_set vars;        
         if (lit() != null_literal) vars.insert(lit().var());
         for (literal l : *this) {
@@ -305,7 +305,7 @@ namespace sat {
             UNREACHABLE();
         }
         SASSERT(validate_conflict(c));
-        if (c.is_xor() && value(lit) == l_true) lit.neg();
+        if (c.is_xr() && value(lit) == l_true) lit.neg();
         SASSERT(value(lit) == l_false);
         set_conflict(justification::mk_ext_justification(c.index()), ~lit);
         SASSERT(inconsistent());
@@ -892,16 +892,16 @@ namespace sat {
 
 
     // --------------------
-    // xor:
+    // xr:
 
-    void ba_solver::clear_watch(xor& x) {
+    void ba_solver::clear_watch(xr& x) {
         unwatch_literal(x[0], x);
         unwatch_literal(x[1], x);         
         unwatch_literal(~x[0], x);
         unwatch_literal(~x[1], x);         
     }
 
-    bool ba_solver::parity(xor const& x, unsigned offset) const {
+    bool ba_solver::parity(xr const& x, unsigned offset) const {
         bool odd = false;
         unsigned sz = x.size();
         for (unsigned i = offset; i < sz; ++i) {
@@ -913,7 +913,7 @@ namespace sat {
         return odd;
     }
 
-    bool ba_solver::init_watch(xor& x) {
+    bool ba_solver::init_watch(xr& x) {
         clear_watch(x);
         if (x.lit() != null_literal && value(x.lit()) == l_false) {
             x.negate();
@@ -957,7 +957,7 @@ namespace sat {
     }
 
 
-    lbool ba_solver::add_assign(xor& x, literal alit) {
+    lbool ba_solver::add_assign(xr& x, literal alit) {
         // literal is assigned     
         unsigned sz = x.size();
         TRACE("ba", tout << "assign: "  << ~alit << "@" << lvl(~alit) << " " << x << "\n"; display(tout, x, true); );
@@ -1223,12 +1223,12 @@ namespace sat {
                     for (literal l : m_lemma) process_antecedent(~l, offset);
                     break;
                 }
-                case xor_t: {
+                case xr_t: {
                     // jus.push_back(js);
                     m_lemma.reset();
                     inc_bound(offset);
                     inc_coeff(consequent, offset);
-                    get_xor_antecedents(consequent, idx, js, m_lemma);
+                    get_xr_antecedents(consequent, idx, js, m_lemma);
                     for (literal l : m_lemma) process_antecedent(~l, offset);
                     break;
                 }
@@ -1593,7 +1593,7 @@ namespace sat {
         switch (c.tag()) {
         case card_t: return init_watch(c.to_card()); 
         case pb_t: return init_watch(c.to_pb());
-        case xor_t: return init_watch(c.to_xor()); 
+        case xr_t: return init_watch(c.to_xr()); 
         }
         UNREACHABLE();
         return false;
@@ -1603,7 +1603,7 @@ namespace sat {
         switch (c.tag()) {
         case card_t: return add_assign(c.to_card(), l); 
         case pb_t: return add_assign(c.to_pb(), l); 
-        case xor_t: return add_assign(c.to_xor(), l); 
+        case xr_t: return add_assign(c.to_xr(), l); 
         }
         UNREACHABLE();
         return l_undef;
@@ -1632,13 +1632,13 @@ namespace sat {
         add_pb_ge(lit, wlits, k, false);
     }
 
-    void ba_solver::add_xor(literal_vector const& lits) {
-        add_xor(lits, false);
+    void ba_solver::add_xr(literal_vector const& lits) {
+        add_xr(lits, false);
     }
 
-    ba_solver::constraint* ba_solver::add_xor(literal_vector const& lits, bool learned) {
-        void * mem = m_allocator.allocate(xor::get_obj_size(lits.size()));
-        xor* x = new (mem) xor(next_id(), lits);
+    ba_solver::constraint* ba_solver::add_xr(literal_vector const& lits, bool learned) {
+        void * mem = m_allocator.allocate(xr::get_obj_size(lits.size()));
+        xr* x = new (mem) xr(next_id(), lits);
         x->set_learned(learned);
         add_constraint(x);
         for (literal l : lits) s().set_external(l.var()); // TBD: determine if goal2sat does this.
@@ -1709,7 +1709,7 @@ namespace sat {
         switch (c.tag()) {
         case card_t: return get_reward(c.to_card(), occs);
         case pb_t: return get_reward(c.to_pb(), occs); 
-        case xor_t: return 0;
+        case xr_t: return 0;
         default: UNREACHABLE(); return 0;
         }
     }
@@ -1737,11 +1737,11 @@ namespace sat {
     }
     
     /**
-       \brief perform parity resolution on xor premises.
-       The idea is to collect premises based on xor resolvents. 
+       \brief perform parity resolution on xr premises.
+       The idea is to collect premises based on xr resolvents. 
        Variables that are repeated an even number of times cancel out.
      */
-    void ba_solver::get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r) {
+    void ba_solver::get_xr_antecedents(literal l, unsigned index, justification js, literal_vector& r) {
         unsigned level = lvl(l);
         bool_var v = l.var();
         SASSERT(js.get_kind() == justification::EXT_JUSTIFICATION);
@@ -1758,11 +1758,11 @@ namespace sat {
             if (js.get_kind() == justification::EXT_JUSTIFICATION) {
                 constraint& c = index2constraint(js.get_ext_justification_idx());
                 TRACE("ba", tout << c << "\n";);
-                if (!c.is_xor()) {
+                if (!c.is_xr()) {
                     r.push_back(l);
                 }
                 else {
-                    xor& x = c.to_xor();                    
+                    xr& x = c.to_xr();                    
                     if (x[1].var() == l.var()) {
                         x.swap(0, 1);
                     }
@@ -1959,7 +1959,7 @@ namespace sat {
         }
     }
 
-    void ba_solver::simplify(xor& x) {
+    void ba_solver::simplify(xr& x) {
         // no-op
     }
 
@@ -1979,7 +1979,7 @@ namespace sat {
         }
     }
 
-    void ba_solver::get_antecedents(literal l, xor const& x, literal_vector& r) {
+    void ba_solver::get_antecedents(literal l, xr const& x, literal_vector& r) {
         if (x.lit() != null_literal) r.push_back(x.lit());
         // TRACE("ba", display(tout << l << " ", x, true););
         SASSERT(x.lit() == null_literal || value(x.lit()) == l_true);
@@ -2021,7 +2021,7 @@ namespace sat {
         switch (c.tag()) {
         case card_t: get_antecedents(l, c.to_card(), r); break;
         case pb_t: get_antecedents(l, c.to_pb(), r); break;
-        case xor_t: get_antecedents(l, c.to_xor(), r); break;
+        case xr_t: get_antecedents(l, c.to_xr(), r); break;
         default: UNREACHABLE(); break;
         }
     }
@@ -2042,8 +2042,8 @@ namespace sat {
         case pb_t:
             clear_watch(c.to_pb());
             break;
-        case xor_t:
-            clear_watch(c.to_xor());
+        case xr_t:
+            clear_watch(c.to_xr());
             break;
         default:
             UNREACHABLE();
@@ -2066,7 +2066,7 @@ namespace sat {
         switch (c.tag()) {
         case card_t:  return validate_unit_propagation(c.to_card(), l); 
         case pb_t: return validate_unit_propagation(c.to_pb(), l);
-        case xor_t: return true;
+        case xr_t: return true;
         default: UNREACHABLE(); break;
         }
         return false;
@@ -2081,7 +2081,7 @@ namespace sat {
         switch (c.tag()) {
         case card_t: return eval(v1, eval(c.to_card())); 
         case pb_t:   return eval(v1, eval(c.to_pb()));
-        case xor_t:  return eval(v1, eval(c.to_xor()));
+        case xr_t:  return eval(v1, eval(c.to_xr()));
         default: UNREACHABLE(); break;
         }
         return l_undef;        
@@ -2120,7 +2120,7 @@ namespace sat {
         return l_undef;        
     }
 
-    lbool ba_solver::eval(xor const& x) const {
+    lbool ba_solver::eval(xr const& x) const {
         bool odd = false;
         
         for (auto l : x) {
@@ -2393,9 +2393,9 @@ namespace sat {
             if (!clausify(c.to_pb()))
                 simplify(c.to_pb());
             break;
-        case xor_t:
-            if (!clausify(c.to_xor()))
-                simplify(c.to_xor());
+        case xr_t:
+            if (!clausify(c.to_xr()))
+                simplify(c.to_xr());
             break;
         default:
             UNREACHABLE();
@@ -2551,7 +2551,7 @@ namespace sat {
         case pb_t:
             recompile(c.to_pb());
             break;
-        case xor_t:
+        case xr_t:
             NOT_IMPLEMENTED_YET();
             break;
         default:
@@ -2664,7 +2664,7 @@ namespace sat {
         return false;
     }
 
-    bool ba_solver::clausify(xor& x) {
+    bool ba_solver::clausify(xr& x) {
         return false;
     }
 
@@ -2730,7 +2730,7 @@ namespace sat {
         switch (c.tag()) {
         case card_t: split_root(c.to_card()); break;
         case pb_t: split_root(c.to_pb()); break;
-        case xor_t: NOT_IMPLEMENTED_YET(); break;
+        case xr_t: NOT_IMPLEMENTED_YET(); break;
         }
     }
 
@@ -2843,8 +2843,8 @@ namespace sat {
                 }
                 break;
             }
-            case xor_t: {
-                xor& x = cp->to_xor();
+            case xr_t: {
+                xr& x = cp->to_xr();
                 for (literal l : x) {
                     m_cnstr_use_list[l.index()].push_back(&x);
                     m_cnstr_use_list[(~l).index()].push_back(&x);
@@ -3319,11 +3319,11 @@ namespace sat {
                 result->add_pb_ge(p.lit(), wlits, p.k(), p.learned());
                 break;
             }
-            case xor_t: {
-                xor const& x = cp->to_xor();
+            case xr_t: {
+                xr const& x = cp->to_xr();
                 lits.reset();
                 for (literal l : x) lits.push_back(l);
-                result->add_xor(lits, x.learned());        
+                result->add_xr(lits, x.learned());        
                 break;
             }
             default:
@@ -3355,8 +3355,8 @@ namespace sat {
                 }
                 break;
             }
-            case xor_t: {
-                xor const& x = cp->to_xor();
+            case xr_t: {
+                xr const& x = cp->to_xr();
                 for (literal l : x) {
                     ul.insert(l, idx);
                     ul.insert(~l, idx);
@@ -3450,8 +3450,8 @@ namespace sat {
         out << ">= " << ineq.m_k << "\n";
     }
 
-    void ba_solver::display(std::ostream& out, xor const& x, bool values) const {
-        out << "xor: ";
+    void ba_solver::display(std::ostream& out, xr const& x, bool values) const {
+        out << "xr: ";
         for (literal l : x) {
             out << l;
             if (values) {
@@ -3520,7 +3520,7 @@ namespace sat {
         switch (c.tag()) {
         case card_t: display(out, c.to_card(), values); break;
         case pb_t: display(out, c.to_pb(), values); break;
-        case xor_t: display(out, c.to_xor(), values); break;
+        case xr_t: display(out, c.to_xr(), values); break;
         default: UNREACHABLE(); break;
         }
     }
@@ -3612,7 +3612,7 @@ namespace sat {
         return false;
     }
 
-    bool ba_solver::validate_unit_propagation(xor const& x, literal alit) const {
+    bool ba_solver::validate_unit_propagation(xr const& x, literal alit) const {
         if (value(x.lit()) != l_true) return false;
         for (unsigned i = 1; i < x.size(); ++i) {
             if (value(x[i]) == l_undef) return false;
@@ -3827,14 +3827,14 @@ namespace sat {
                 if (p.lit() != null_literal) ineq.push(~p.lit(), p.k());
                 break;
             }
-            case xor_t: {
-                xor& x = cnstr.to_xor();
+            case xr_t: {
+                xr& x = cnstr.to_xr();
                 literal_vector ls;
                 get_antecedents(lit, x, ls);                
                 ineq.reset(offset);
                 for (literal l : ls) ineq.push(~l, offset);
-                literal lxor = x.lit();                
-                if (lxor != null_literal) ineq.push(~lxor, offset);
+                literal lxr = x.lit();                
+                if (lxr != null_literal) ineq.push(~lxr, offset);
                 break;
             }
             default:
diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h
index d950cb8cc..63e58d4b6 100644
--- a/src/sat/ba_solver.h
+++ b/src/sat/ba_solver.h
@@ -51,12 +51,12 @@ namespace sat {
         enum tag_t {
             card_t,
             pb_t,
-            xor_t
+            xr_t
         };
 
         class card;
         class pb;
-        class xor;
+        class xr;
 
         class constraint {
         protected:
@@ -91,13 +91,13 @@ namespace sat {
             size_t obj_size() const { return m_obj_size; }
             card& to_card();
             pb&  to_pb();
-            xor& to_xor();
+            xr& to_xr();
             card const& to_card() const;
             pb const&  to_pb() const;
-            xor const& to_xor() const;
+            xr const& to_xr() const;
             bool is_card() const { return m_tag == card_t; }
             bool is_pb() const { return m_tag == pb_t; }
-            bool is_xor() const { return m_tag == xor_t; }
+            bool is_xr() const { return m_tag == xr_t; }
             
             virtual bool is_watching(literal l) const { UNREACHABLE(); return false; };
             virtual literal_vector literals() const { UNREACHABLE(); return literal_vector(); }
@@ -174,11 +174,11 @@ namespace sat {
             virtual unsigned get_coeff(unsigned i) const { return m_wlits[i].first; }
         };
 
-        class xor : public constraint {
+        class xr : public constraint {
             literal        m_lits[0];
         public:
-            static size_t get_obj_size(unsigned num_lits) { return sizeof(xor) + num_lits * sizeof(literal); }
-            xor(unsigned id, literal_vector const& lits);
+            static size_t get_obj_size(unsigned num_lits) { return sizeof(xr) + num_lits * sizeof(literal); }
+            xr(unsigned id, literal_vector const& lits);
             literal operator[](unsigned i) const { return m_lits[i]; }
             literal const* begin() const { return m_lits; }
             literal const* end() const { return begin() + m_size; }
@@ -351,17 +351,17 @@ namespace sat {
         double get_reward(card const& c, literal_occs_fun& occs) const;
 
 
-        // xor specific functionality
-        void clear_watch(xor& x);
-        bool init_watch(xor& x);
-        bool parity(xor const& x, unsigned offset) const;
-        lbool add_assign(xor& x, literal alit);
-        void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r);
-        void get_antecedents(literal l, xor const& x, literal_vector & r);
-        void simplify(xor& x);
-        bool clausify(xor& x);
-        void flush_roots(xor& x);
-        lbool eval(xor const& x) const;
+        // xr specific functionality
+        void clear_watch(xr& x);
+        bool init_watch(xr& x);
+        bool parity(xr const& x, unsigned offset) const;
+        lbool add_assign(xr& x, literal alit);
+        void get_xr_antecedents(literal l, unsigned index, justification js, literal_vector& r);
+        void get_antecedents(literal l, xr const& x, literal_vector & r);
+        void simplify(xr& x);
+        bool clausify(xr& x);
+        void flush_roots(xr& x);
+        lbool eval(xr const& x) const;
         
         // pb functionality
         unsigned m_a_max;
@@ -425,14 +425,14 @@ namespace sat {
 
         // validation utilities
         bool validate_conflict(card const& c) const;
-        bool validate_conflict(xor const& x) const;
+        bool validate_conflict(xr const& x) const;
         bool validate_conflict(pb const& p) const;
         bool validate_assign(literal_vector const& lits, literal lit);
         bool validate_lemma();
         bool validate_unit_propagation(card const& c, literal alit) const;
         bool validate_unit_propagation(pb const& p, literal alit) const;
         bool validate_unit_propagation(pb const& p, literal_vector const& r, literal alit) const;
-        bool validate_unit_propagation(xor const& x, literal alit) const;
+        bool validate_unit_propagation(xr const& x, literal alit) const;
         bool validate_conflict(literal_vector const& lits, ineq& p);
         bool validate_watch_literals() const;
         bool validate_watch_literal(literal lit) const;
@@ -456,11 +456,11 @@ namespace sat {
         void display(std::ostream& out, constraint const& c, bool values) const;
         void display(std::ostream& out, card const& c, bool values) const;
         void display(std::ostream& out, pb const& p, bool values) const;
-        void display(std::ostream& out, xor const& c, bool values) const;
+        void display(std::ostream& out, xr const& c, bool values) const;
 
         constraint* add_at_least(literal l, literal_vector const& lits, unsigned k, bool learned);
         constraint* add_pb_ge(literal l, svector<wliteral> const& wlits, unsigned k, bool learned);
-        constraint* add_xor(literal_vector const& lits, bool learned);
+        constraint* add_xr(literal_vector const& lits, bool learned);
 
         void copy_core(ba_solver* result, bool learned);
         void copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints);
@@ -472,7 +472,7 @@ namespace sat {
         virtual void set_unit_walk(unit_walk* u) { m_unit_walk = u; }
         void    add_at_least(bool_var v, literal_vector const& lits, unsigned k);
         void    add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
-        void    add_xor(literal_vector const& lits);
+        void    add_xr(literal_vector const& lits);
 
         virtual bool propagate(literal l, ext_constraint_idx idx);
         virtual lbool resolve_conflict();
diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 376d607ab..da9617151 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -400,7 +400,7 @@ namespace sat {
                     }
                     break;
                 }
-                case ba_solver::xor_t:
+                case ba_solver::xr_t:
                     NOT_IMPLEMENTED_YET();
                     break;
                 }
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 0ba8926cd..c6d6b4cac 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -104,7 +104,7 @@ public:
 
     virtual ~inc_sat_solver() {}
 
-    virtual solver* translate(ast_manager& dst_m, params_ref const& p) {
+    solver* translate(ast_manager& dst_m, params_ref const& p) override {
         if (m_num_scopes > 0) {
             throw default_exception("Cannot translate sat solver at non-base level");
         }
@@ -128,7 +128,7 @@ public:
         return result;
     }
 
-    virtual void set_progress_callback(progress_callback * callback) {}
+    void set_progress_callback(progress_callback * callback) override {}
 
     void display_weighted(std::ostream& out, unsigned sz, expr * const * assumptions, unsigned const* weights) {
         if (weights != 0) {
@@ -160,7 +160,7 @@ public:
             (m.is_not(e, e) && is_uninterp_const(e));
     }
 
-    virtual lbool check_sat(unsigned sz, expr * const * assumptions) {
+    lbool check_sat(unsigned sz, expr * const * assumptions) override {
         m_solver.pop_to_base_level();
         m_core.reset();
         if (m_solver.inconsistent()) return l_false;
@@ -213,7 +213,8 @@ public:
         }
         return r;
     }
-    virtual void push() {
+
+    void push() override {
         internalize_formulas();
         m_solver.user_push();
         ++m_num_scopes;
@@ -223,7 +224,8 @@ public:
         if (m_bb_rewriter) m_bb_rewriter->push();
         m_map.push();
     }
-    virtual void pop(unsigned n) {
+
+    void pop(unsigned n) override {
         if (n > m_num_scopes) {   // allow inc_sat_solver to
             n = m_num_scopes;     // take over for another solver.
         }
@@ -243,9 +245,11 @@ public:
             --n;
         }
     }
+
     unsigned get_scope_level() const override {
         return m_num_scopes;
     }
+
     void assert_expr_core2(expr * t, expr * a) override {
         if (a) {
             m_asmsf.push_back(a);
@@ -256,18 +260,18 @@ public:
         }
     }
 
-    virtual ast_manager& get_manager() const { return m; }
-    virtual void assert_expr_core(expr * t) {
+    ast_manager& get_manager() const override { return m; }
+    void assert_expr_core(expr * t) override {
         TRACE("goal2sat", tout << mk_pp(t, m) << "\n";);
         m_fmls.push_back(t);
     }
-    virtual void set_produce_models(bool f) {}
-    virtual void collect_param_descrs(param_descrs & r) {
+    void set_produce_models(bool f) override {}
+    void collect_param_descrs(param_descrs & r) override {
         solver::collect_param_descrs(r);
         goal2sat::collect_param_descrs(r);
         sat::solver::collect_param_descrs(r);
     }
-    virtual void updt_params(params_ref const & p) {
+    void updt_params(params_ref const & p) override {
         m_params.append(p);
         sat_params p1(p);
         m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver());
@@ -279,20 +283,20 @@ public:
         m_solver.set_incremental(is_incremental() && !override_incremental());
 
     }
-    virtual void collect_statistics(statistics & st) const {
+    void collect_statistics(statistics & st) const override {
         if (m_preprocess) m_preprocess->collect_statistics(st);
         m_solver.collect_statistics(st);
     }
-    virtual void get_unsat_core(ptr_vector<expr> & r) {
+    void get_unsat_core(ptr_vector<expr> & r) override {
         r.reset();
         r.append(m_core.size(), m_core.c_ptr());
     }
-    virtual proof * get_proof() {
+    proof * get_proof() override {
         UNREACHABLE();
         return 0;
     }
 
-    virtual expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) {
+    expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) override {
         if (!is_internalized()) {
             lbool r = internalize_formulas();
             if (r != l_true) return expr_ref_vector(m);
@@ -331,8 +335,8 @@ public:
         }
         return fmls;
     }
-
-    virtual lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {
+    
+    lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) override {
         init_preprocess();
         TRACE("sat", tout << assumptions << "\n" << vars << "\n";);
         sat::literal_vector asms;
@@ -780,7 +784,7 @@ private:
         }
     }
 
-    virtual void get_model_core(model_ref & mdl) {
+    void get_model_core(model_ref & mdl) override {
         TRACE("sat", tout << "retrieve model " << (m_solver.model_is_current()?"present":"absent") << "\n";);
         if (!m_solver.model_is_current()) {
             mdl = nullptr;
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 5bba70659..ac97eb3c3 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -400,7 +400,7 @@ struct goal2sat::imp {
             lits[i].neg();
         }
         ensure_extension();
-        m_ext->add_xor(lits);
+        m_ext->add_xr(lits);
         sat::literal lit(v, sign);
         if (root) {            
             m_result_stack.reset();
@@ -1115,7 +1115,7 @@ struct sat2goal::imp {
         r.assert_expr(fml);
     }
 
-    void assert_xor(ref<mc>& mc, goal & r, sat::ba_solver::xor const& x) {
+    void assert_xor(ref<mc>& mc, goal & r, sat::ba_solver::xr const& x) {
         ptr_buffer<expr> lits;
         for (sat::literal l : x) {
             lits.push_back(lit2expr(mc, l));
@@ -1185,8 +1185,8 @@ struct sat2goal::imp {
                 case sat::ba_solver::pb_t: 
                     assert_pb(mc, r, c->to_pb());
                     break;
-                case sat::ba_solver::xor_t: 
-                    assert_xor(mc, r, c->to_xor());
+                case sat::ba_solver::xr_t: 
+                    assert_xor(mc, r, c->to_xr());
                     break;
                 }
             }