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

unused variable warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-26 23:21:48 -07:00
parent 5434f3e31d
commit d818233063
4 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/seq_offset_eq.cpp
View file

@ -32,8 +32,9 @@ update m_offset_equalities to contain.
r1 |-> [r2 |-> val]
*/
seq_offset_eq::seq_offset_eq(theory& th, ast_manager& m):
th(th), m(m), seq(m), a(m), m_propagation_level(-1) {
seq_offset_eq::seq_offset_eq(theory& th, ast_manager& _m):
th(th), m(_m), seq(m), a(m), m_propagation_level(-1) {
(void)m;
}
bool seq_offset_eq::match_x_minus_y(expr* e, expr*& x, expr*& y) const {

4
src/smt/theory_seq.cpp
View file

@ -745,6 +745,7 @@ bool theory_seq::is_solved() {
*/
void theory_seq::linearize(dependency* dep, enode_pair_vector& eqs, literal_vector& lits) const {
context & ctx = get_context();
(void)ctx;
DEBUG_CODE(for (literal lit : lits) SASSERT(ctx.get_assignment(lit) == l_true); );
svector<assumption> assumptions;
const_cast<dependency_manager&>(m_dm).linearize(dep, assumptions);
@ -1885,6 +1886,7 @@ class theory_seq::seq_value_proc : public model_value_proc {
svector<source_t> m_source;
public:
seq_value_proc(theory_seq& th, enode* n, sort* s): th(th), m_node(n), m_sort(s) {
(void)m_node;
}
~seq_value_proc() override {}
void add_unit(enode* n) {
@ -3458,7 +3460,7 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) {
void theory_seq::propagate_length_limit(expr* e) {
unsigned k = 0;
expr* s = nullptr, *i = nullptr;
expr* s = nullptr;
VERIFY(m_sk.is_length_limit(e, k, s));
if (m_util.str.is_stoi(s)) {
m_ax.add_stoi_axiom(s, k);

2
src/smt/theory_seq.h
View file

@ -446,7 +446,7 @@ namespace smt {
theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager(), new_ctx->get_fparams()); }
char const * get_name() const override { return "seq"; }
bool include_func_interp(func_decl* f) override { return m_util.str.is_nth_u(f); }
bool is_safe_to_copy(bool_var v) const;
bool is_safe_to_copy(bool_var v) const override;
theory_var mk_var(enode* n) override;
void apply_sort_cnstr(enode* n, sort* s) override;
void display(std::ostream & out) const override;

1
src/tactic/ufbv/ufbv_rewriter.cpp
View file

@ -371,7 +371,6 @@ expr * ufbv_rewriter::rewrite(expr * n) {
if (rewrite_visit_children(a)) {
func_decl * f = a->get_decl();
m_new_args.reset();
unsigned num_args = a->get_num_args();
bool all_untouched = true;
for (expr* o_child : *a) {
expr * n_child;