Skip to content

Commit

Permalink
unused variable warning
Browse files Browse the repository at this point in the history
Signed-off-by: Nikolaj Bjorner <[email protected]>
  • Loading branch information
NikolajBjorner committed Jul 26, 2020
1 parent 4d586c2 commit 78afa25
Show file tree
Hide file tree
Showing 4 changed files with 6 additions and 7 deletions.
2 changes: 1 addition & 1 deletion src/smt/seq_axioms.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -327,7 +327,7 @@ void seq_axioms::add_indexof_axiom(expr* i) {
if (!offset || (a.is_numeral(offset, r) && r.is_zero())) {
// |s| = 0 => indexof(t,s,0) = 0
add_axiom(~s_eq_empty, i_eq_0);
#if 1
#if 0
expr_ref x = m_sk.mk_indexof_left(t, s);
expr_ref y = m_sk.mk_indexof_right(t, s);
xsy = mk_concat(x, s, y);
Expand Down
7 changes: 3 additions & 4 deletions src/smt/smt_induction.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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()() {
Expand Down Expand Up @@ -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),
Expand All @@ -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
Expand Down
3 changes: 1 addition & 2 deletions src/smt/smt_induction.h
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,6 @@ namespace smt {

context& ctx;
ast_manager& m;
value_sweep& vs;
datatype::util m_dt;
arith_util m_a;
recfun::util m_rec;
Expand Down Expand Up @@ -123,7 +122,7 @@ namespace smt {
void apply_induction(literal lit, induction_positions_t const & positions);

public:
induction_lemmas(context& ctx, ast_manager& m, value_sweep& vs);
induction_lemmas(context& ctx, ast_manager& m);

bool operator()(literal lit);
};
Expand Down
1 change: 1 addition & 0 deletions src/smt/theory_seq.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -3565,6 +3565,7 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) {
if (k_min < UINT_MAX) {
m_max_unfolding_depth++;
k_min *= 2;
rational lo;
if (m_util.is_seq(s_min))
k_min = std::max(m_util.str.min_length(s_min), k_min);
IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-length " << mk_pp(s_min, m) << " " << k_min << ")\n");
Expand Down

0 comments on commit 78afa25

Please sign in to comment.