mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00
Code Activity

Remove unused private fields and local vars.

Browse source
This commit is contained in:
David Detlefs 2026-06-15 13:46:51 -07:00
parent b96f61654e
commit 639530f42a
4 changed files with 2 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/simplifiers/dependent_expr_state.h
View file

@ -45,7 +45,7 @@ Author:
class dependent_expr_state {
unsigned m_qhead = 0;
bool m_suffix_frozen = false;
unsigned m_num_recfun = 0, m_num_lambdas = 0;
unsigned m_num_recfun = 0;
lbool m_has_quantifiers = l_undef;
ast_mark m_frozen;
func_decl_ref_vector m_frozen_trail;

1
src/smt/smt_context.cpp
View file

@ -4672,7 +4672,6 @@ namespace smt {
theory_id th_id = l->get_id();
for (enode * parent : enode::parents(n)) {
auto p = parent->get_expr();
family_id fid = parent->get_family_id();
if (fid != th_id && fid != m.get_basic_family_id()) {
if (is_beta_redex(parent, n))

1
src/smt/theory_sls.h
View file

@ -66,7 +66,6 @@ namespace smt {
unsigned m_final_check_ls_steps = 30000;
unsigned m_final_check_ls_steps_delta = 10000;
unsigned m_final_check_ls_steps_min = 10000;
unsigned m_final_check_ls_steps_max = 30000;
bool m_has_unassigned_clause_after_resolve = false;
unsigned m_after_resolve_decide_gap = 4;
unsigned m_after_resolve_decide_count = 0;

3
src/solver/parallel_tactical2.cpp
View file

@ -460,7 +460,6 @@ class parallel_solver {
};
unsigned id;
parallel_solver& p;
batch_manager& b;
ast_manager m; /* worker-local manager */
ref<solver> s; /* translated solver copy */
@ -579,7 +578,7 @@ class parallel_solver {
worker(unsigned id, parallel_solver& p,
solver& src, params_ref const& params,
expr_ref_vector const& src_asms)
: id(id), p(p), b(p.m_batch_manager),
: id(id), b(p.m_batch_manager),
asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager())
{
/* create translated solver copy */