mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 18:36:16 +00:00
Code Activity

unused variable warning

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-25 15:41:42 -07:00
parent 4d586c2c13
commit 78afa2527c
4 changed files with 6 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/smt_induction.cpp
View file

@ -95,7 +95,7 @@ collect_induction_literals::collect_induction_literals(context& ctx, ast_manager
vs(vs),
m_literal_index(0)
{
(void)vs;
// (void)vs;
}
literal_vector collect_induction_literals::operator()() {
@ -538,10 +538,9 @@ void induction_lemmas::apply_induction(literal lit, induction_positions_t const
}
}
induction_lemmas::induction_lemmas(context& ctx, ast_manager& m, value_sweep& vs):
induction_lemmas::induction_lemmas(context& ctx, ast_manager& m):
ctx(ctx),
m(m),
vs(vs),
m_dt(m),
m_a(m),
m_rec(m),
@ -554,7 +553,7 @@ induction::induction(context& ctx, ast_manager& m):
m(m),
vs(m),
m_collect_literals(ctx, m, vs),
m_create_lemmas(ctx, m, vs)
m_create_lemmas(ctx, m)
{}
// TBD: use smt_arith_value to also include state from arithmetic solver