mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-29 11:58:51 +00:00
Code Activity

Eliminate unused private fields and local variables. (#9875)

Browse source 
This is another PR towards the goal of getting a clean build with clang,
using the compiler options used in building clang-tidy.

By default, without any new -W flags, clang warns about unused local
variables and private class fields. This PR deletes the handful of these
that clang found.

I'm assuming that the class "enode" in smt_context.cpp is the one in
smt_enode.h, so that
```
parent->get_expr()
```
calls a const method with no side effects.
This commit is contained in:
davedets 2026-06-16 06:55:18 -07:00 • committed by GitHub
parent c67bb140dc
commit 86de0cbd71
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 2 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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;