mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +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:42:46 -07:00
parent 78afa2527c
commit 4be6927460
3 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/seq_axioms.cpp
View file

@ -327,7 +327,7 @@ void seq_axioms::add_indexof_axiom(expr* i) {
if (!offset || (a.is_numeral(offset, r) && r.is_zero())) { if (!offset || (a.is_numeral(offset, r) && r.is_zero())) {
// |s| = 0 => indexof(t,s,0) = 0 // |s| = 0 => indexof(t,s,0) = 0
add_axiom(~s_eq_empty, i_eq_0); add_axiom(~s_eq_empty, i_eq_0);
#if 0 #if 1
expr_ref x = m_sk.mk_indexof_left(t, s); expr_ref x = m_sk.mk_indexof_left(t, s);
expr_ref y = m_sk.mk_indexof_right(t, s); expr_ref y = m_sk.mk_indexof_right(t, s);
xsy = mk_concat(x, s, y); xsy = mk_concat(x, s, y);

1
src/smt/smt_induction.cpp
View file

@ -95,7 +95,6 @@ collect_induction_literals::collect_induction_literals(context& ctx, ast_manager
vs(vs), vs(vs),
m_literal_index(0) m_literal_index(0)
{ {
// (void)vs;
} }
literal_vector collect_induction_literals::operator()() { literal_vector collect_induction_literals::operator()() {

1
src/smt/theory_seq.cpp
View file

@ -3565,7 +3565,6 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) {
if (k_min < UINT_MAX) { if (k_min < UINT_MAX) {
m_max_unfolding_depth++; m_max_unfolding_depth++;
k_min *= 2; k_min *= 2;
rational lo;
if (m_util.is_seq(s_min)) if (m_util.is_seq(s_min))
k_min = std::max(m_util.str.min_length(s_min), k_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"); IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-length " << mk_pp(s_min, m) << " " << k_min << ")\n");