mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-23 14:11:28 +00:00
Code Activity

merge

Browse source
This commit is contained in:
Ilana Shapiro 2025-11-02 09:41:36 -08:00
parent 8e17288026
commit 06e195fb01
2 changed files with 0 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_context.h
View file

@ -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
// -----------------------------------

7
src/smt/smt_internalizer.cpp
View file

@ -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) {