mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

remove unused variables

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-10-10 20:29:39 +09:00
parent f3e9712beb
commit 338d7b3283
2 changed files with 0 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/int_solver.h
View file

@ -44,10 +44,6 @@ class int_solver {
int_solver& lia; int_solver& lia;
lar_solver& lra; lar_solver& lra;
lar_core_solver& lrac; lar_core_solver& lrac;
unsigned m_patch_success = 0;
unsigned m_patch_fail = 0;
unsigned m_num_ones = 0;
unsigned m_num_divides = 0;
public: public:
patcher(int_solver& lia); patcher(int_solver& lia);
bool should_apply() const { return true; } bool should_apply() const { return true; }

1
src/smt/smt_clause_proof.cpp
View file

@ -194,7 +194,6 @@ namespace smt {
m_trail.push_back(info(st, v, p)); m_trail.push_back(info(st, v, p));
if (m_on_clause_eh) if (m_on_clause_eh)
m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data()); m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data());
static unsigned s_count = 0;
if (m_has_log) { if (m_has_log) {
init_pp_out(); init_pp_out();