From 06e195fb01a904fa92b3aaf6b74a66cac3b725dd Mon Sep 17 00:00:00 2001
From: Ilana Shapiro <ishapiro00@gmail.com>
Date: Sun, 2 Nov 2025 09:41:36 -0800
Subject: [PATCH] merge

---
 src/smt/smt_context.h        | 4 ----
 src/smt/smt_internalizer.cpp | 7 -------
 2 files changed, 11 deletions(-)

diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index ecd35c785..0e4cdde44 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -137,11 +137,7 @@ namespace smt {
         scoped_ptr<base_dependent_expr_state> m_fmls;
 
         svector<double> m_lit_scores[2];
-<<<<<<< HEAD
-        vector<expr_ref_vector> m_recorded_cubes;
-=======
         vector<expr_ref_vector>* m_recorded_cubes = nullptr;
->>>>>>> e3c715ce37c4064587a55077d89f90ed5c89007c
 
 
         // -----------------------------------
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index cd9690919..b86af05ac 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -967,11 +967,8 @@ namespace smt {
 
     // following the pattern of solver::persist_clause in src/sat/smt/user_solver.cpp
     void context::record_cube(unsigned num_lits, literal const *lits) {
-<<<<<<< HEAD
-=======
         if (!m_recorded_cubes)
             return;
->>>>>>> e3c715ce37c4064587a55077d89f90ed5c89007c
         expr_ref_vector cube(m);
         for (unsigned i = 0; i < num_lits; ++i) {
             literal lit = lits[i];
@@ -981,11 +978,7 @@ namespace smt {
                 e = m.mk_not(e);  // only negate positive literal
             cube.push_back(e);
         }
-<<<<<<< HEAD
-        m_recorded_cubes.push_back(cube);
-=======
         m_recorded_cubes->push_back(cube);
->>>>>>> e3c715ce37c4064587a55077d89f90ed5c89007c
     }
 
     void context::add_scores(unsigned n, literal const *lits) {