search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.3k stars 1.48k forks source link

-Wunused-but-set-variable and -Wunused-variable warnings #579

Closed chadrosier closed 8 years ago

chadrosier commented 8 years ago

It would be nice if z3 built without warnings. As of c414c6b5fd07846a49a1050a1d45c23e6b7b9a9a I see the following warnings for unused variables:

src/util/mpn.cpp:277:35: warning: variable ‘r_hat’ set but not used [-Wunused-but-set-variable] src/util/mpff.cpp:1397:16: warning: unused variable ‘s’ [-Wunused-variable] src/util/mpf.cpp:1093:18: warning: unused variable ‘less_than_tie’ [-Wunused-variable] src/util/mpf.cpp:1716:17: warning: unused variable ‘p_m1’ [-Wunused-variable] src/util/mpf.cpp:1908:10: warning: unused variable ‘last’ [-Wunused-variable] src/math/simplex/model_based_opt.cpp:114:22: warning: unused variable ‘r’ [-Wunused-variable] src/math/simplex/model_based_opt.cpp:108:29: warning: unused variable ‘x_val’ [-Wunused-variable] src/math/simplex/model_based_opt.cpp:109:36: warning: unused variable ‘row_ids’ [-Wunused-variable] src/math/euclid/euclidean_solver.cpp:583:20: warning: unused variable ‘eq’ [-Wunused-variable] src/sat/sat_clause.cpp:54:24: warning: variable ‘curr’ set but not used [-Wunused-but-set-variable] src/sat/sat_clause_set.cpp:65:26: warning: unused variable ‘c’ [-Wunused-variable] src/math/polynomial/upolynomial.cpp:2761:13: warning: unused variable ‘sign_b’ [-Wunused-variable] src/math/polynomial/upolynomial.cpp:2813:13: warning: unused variable ‘sign_b’ [-Wunused-variable] src/math/polynomial/upolynomial.cpp:2930:17: warning: unused variable ‘sign_b’ [-Wunused-variable] src/sat/sat_bceq.cpp:349:20: warning: unused variable ‘b’ [-Wunused-variable] src/sat/sat_integrity_checker.cpp:43:29: warning: variable ‘l’ set but not used [-Wunused-but-set-variable] src/sat/sat_integrity_checker.cpp:160:21: warning: variable ‘l’ set but not used [-Wunused-but-set-variable] src/math/polynomial/upolynomial_factorization.cpp:374:14: warning: unused variable ‘p’ [-Wunused-variable] src/math/polynomial/upolynomial_factorization.cpp:437:14: warning: unused variable ‘d’ [-Wunused-variable] src/sat/sat_sls.cpp:274:18: warning: unused variable ‘is_sat’ [-Wunused-variable] src/sat/sat_sls.cpp:285:26: warning: unused variable ‘idx’ [-Wunused-variable] src/sat/sat_sls.cpp:559:18: warning: unused variable ‘v’ [-Wunused-variable] src/sat/sat_sls.cpp:651:17: warning: unused variable ‘hs’ [-Wunused-variable] src/sat/sat_sls.cpp:658:22: warning: unused variable ‘v’ [-Wunused-variable] src/sat/sat_sls.cpp:659:20: warning: unused variable ‘ss’ [-Wunused-variable] src/sat/sat_solver.cpp:83:26: warning: unused variable ‘new_v’ [-Wunused-variable] src/sat/sat_solver.cpp:410:19: warning: unused variable ‘val’ [-Wunused-variable] src/nlsat/nlsat_interval_set.cpp:109:34: warning: unused variable ‘next’ [-Wunused-variable] src/nlsat/nlsat_interval_set.cpp:106:30: warning: unused variable ‘curr’ [-Wunused-variable] src/nlsat/nlsat_solver.cpp:1735:36: warning: unused variable ‘c’ [-Wunused-variable] src/nlsat/nlsat_solver.cpp:1747:36: warning: unused variable ‘c’ [-Wunused-variable] src/nlsat/nlsat_explain.cpp:1168:27: warning: unused variable ‘val’ [-Wunused-variable] src/ast/ast.cpp:1497:21: warning: unused variable ‘new_fid’ [-Wunused-variable] src/ast/seq_decl_plugin.cpp:280:18: warning: unused variable ‘m’ [-Wunused-variable] src/ast/rewriter/bv_trailing.cpp:70:24: warning: unused variable ‘rm1’ [-Wunused-variable] src/ast/rewriter/bv_trailing.cpp:71:24: warning: unused variable ‘rm2’ [-Wunused-variable] src/ast/rewriter/bv_trailing.cpp:125:28: warning: unused variable ‘crm’ [-Wunused-variable] src/ast/simplifier/simplifier.cpp:65:13: warning: unused variable ‘s_orig’ [-Wunused-variable] src/ast/fpa/fpa2bv_converter.cpp:2183:18: warning: unused variable ‘to_sbits’ [-Wunused-variable] src/ast/fpa/fpa2bv_converter.cpp:2317:18: warning: unused variable ‘sig_sz’ [-Wunused-variable] src/tactic/arith/fm_tactic.cpp:78:18: warning: variable ‘found’ set but not used [-Wunused-but-set-variable] src/ackermannization/lackr.cpp:137:26: warning: unused variable ‘fd’ [-Wunused-variable] src/interp/iz3translate_direct.cpp:358:22: warning: variable ‘found_pivot2’ set but not used [-Wunused-but-set-variable] src/tactic/bv/elim_small_bv_tactic.cpp:150:32: warning: unused variable ‘name’ [-Wunused-variable] src/interp/iz3translate.cpp:338:22: warning: variable ‘found_pivot2’ set but not used [-Wunused-but-set-variable] src/parsers/smt2/smt2parser.cpp:475:22: warning: unused variable ‘stack_pos’ [-Wunused-variable] src/parsers/smt2/smt2parser.cpp:633:22: warning: unused variable ‘stack_pos’ [-Wunused-variable] src/parsers/smt2/smt2parser.cpp:695:22: warning: unused variable ‘stack_pos’ [-Wunused-variable] src/smt/qi_queue.cpp:370:31: warning: unused variable ‘f’ [-Wunused-variable] src/smt/qi_queue.cpp:382:30: warning: unused variable ‘qa’ [-Wunused-variable] src/smt/qi_queue.cpp:400:26: warning: unused variable ‘qa’ [-Wunused-variable] src/smt/smt_conflict_resolution.cpp:102:22: warning: unused variable ‘m’ [-Wunused-variable] src/smt/smt_context.cpp:2261:30: warning: unused variable ‘ilvl’ [-Wunused-variable] src/smt/smt_context.cpp:2858:18: warning: unused variable ‘res’ [-Wunused-variable] src/smt/smt_context.cpp:3113:22: warning: unused variable ‘res’ [-Wunused-variable] src/smt/smt_context.cpp:3200:26: warning: unused variable ‘res’ [-Wunused-variable] src/smt/theory_array.cpp:78:20: warning: unused variable ‘r2’ [-Wunused-variable] src/smt/smt_model_finder.cpp:2907:39: warning: unused variable ‘qi’ [-Wunused-variable] src/smt/smt_model_finder.cpp:3549:18: warning: unused variable ‘flat_num_decls’ [-Wunused-variable] src/smt/smt_model_finder.cpp:3550:18: warning: unused variable ‘num_sks’ [-Wunused-variable] src/smt/theory_datatype.cpp:201:20: warning: unused variable ‘r2’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:609:13: warning: unused variable ‘e_id’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:276:18: warning: unused variable ‘m’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:1197:27: warning: unused variable ‘objective’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:937:17: warning: unused variable ‘edge_id’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:609:13: warning: unused variable ‘e_id’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:276:18: warning: unused variable ‘m’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:1197:27: warning: unused variable ‘objective’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:937:17: warning: unused variable ‘edge_id’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:609:13: warning: unused variable ‘e_id’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:276:18: warning: unused variable ‘m’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:1197:27: warning: unused variable ‘objective’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:937:17: warning: unused variable ‘edge_id’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:609:13: warning: unused variable ‘e_id’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:276:18: warning: unused variable ‘m’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:1197:27: warning: unused variable ‘objective’ [-Wunused-variable] src/smt/theory_diff_logic_def.h:937:17: warning: unused variable ‘edge_id’ [-Wunused-variable] src/math/simplex/sparse_matrix_def.h:515:30: warning: unused variable ‘c’ [-Wunused-variable] src/math/simplex/sparse_matrix_def.h:545:31: warning: unused variable ‘r’ [-Wunused-variable] src/smt/diff_logic.h:706:38: warning: variable ‘max_idx’ set but not used [-Wunused-but-set-variable] src/smt/diff_logic.h:706:38: warning: variable ‘max_idx’ set but not used [-Wunused-but-set-variable] src/smt/diff_logic.h:706:38: warning: variable ‘max_idx’ set but not used [-Wunused-but-set-variable] src/smt/diff_logic.h:706:38: warning: variable ‘max_idx’ set but not used [-Wunused-but-set-variable] src/smt/theory_bv.cpp:460:14: warning: unused variable ‘r’ [-Wunused-variable] src/smt/theory_bv.cpp:557:23: warning: unused variable ‘m’ [-Wunused-variable] src/smt/theory_bv.cpp:1145:19: warning: unused variable ‘ctx’ [-Wunused-variable] src/smt/theory_fpa.cpp:55:22: warning: unused variable ‘ebits’ [-Wunused-variable] src/smt/theory_fpa.cpp:202:18: warning: unused variable ‘r’ [-Wunused-variable] src/smt/theory_fpa.cpp:219:18: warning: variable ‘r’ set but not used [-Wunused-but-set-variable] src/smt/theory_fpa.cpp:179:23: warning: unused variable ‘m’ [-Wunused-variable] src/smt/theory_fpa.cpp:255:23: warning: unused variable ‘m’ [-Wunused-variable] src/smt/theory_fpa.cpp:264:14: warning: unused variable ‘r’ [-Wunused-variable] src/smt/theory_fpa.cpp:360:26: warning: unused variable ‘ebits’ [-Wunused-variable] src/smt/theory_wmaxsat.cpp:263:18: warning: unused variable ‘m’ [-Wunused-variable] src/smt/diff_logic.h:706:38: warning: variable ‘max_idx’ set but not used [-Wunused-but-set-variable] src/smt/diff_logic.h:706:38: warning: variable ‘max_idx’ set but not used [-Wunused-but-set-variable] src/smt/theory_pb.cpp:790:23: warning: unused variable ‘c’ [-Wunused-variable] src/smt/theory_pb.cpp:1837:18: warning: unused variable ‘ctx’ [-Wunused-variable] src/smt/theory_seq.cpp:3184:14: warning: unused variable ‘ctx’ [-Wunused-variable] src/smt/theory_seq.cpp:3205:14: warning: unused variable ‘ctx’ [-Wunused-variable] src/smt/theory_seq.cpp:3683:14: warning: unused variable ‘ctx’ [-Wunused-variable] src/smt/theory_arith_aux.h:1786:15: warning: unused variable ‘e’ [-Wunused-variable] src/smt/theory_arith_aux.h:1324:14: warning: variable ‘empty_column’ set but not used [-Wunused-but-set-variable] src/smt/theory_arith_aux.h:1786:15: warning: unused variable ‘e’ [-Wunused-variable] src/smt/theory_arith_aux.h:1324:14: warning: variable ‘empty_column’ set but not used [-Wunused-but-set-variable] src/smt/theory_arith_aux.h:1786:15: warning: unused variable ‘e’ [-Wunused-variable] src/smt/theory_arith_aux.h:1324:14: warning: variable ‘empty_column’ set but not used [-Wunused-but-set-variable] src/qe/qe_arith_plugin.cpp:1156:26: warning: unused variable ‘m’ [-Wunused-variable] src/qe/qe_arith_plugin.cpp:1157:18: warning: unused variable ‘x’ [-Wunused-variable] src/qe/qe_arith_plugin.cpp:2326:18: warning: unused variable ‘atm’ [-Wunused-variable] src/qe/qe_datatype_plugin.cpp:795:26: warning: unused variable ‘sz’ [-Wunused-variable] src/qe/qe_sat_tactic.cpp:606:19: warning: unused variable ‘is_sat’ [-Wunused-variable] src/qe/qe.cpp:864:26: warning: unused variable ‘m’ [-Wunused-variable] src/qe/qe.cpp:1902:19: warning: unused variable ‘fml’ [-Wunused-variable] src/muz/transforms/dl_mk_bit_blast.cpp:73:26: warning: unused variable ‘arity_p’ [-Wunused-variable] src/muz/transforms/dl_mk_quantifier_abstraction.cpp:74:26: warning: unused variable ‘arity_p’ [-Wunused-variable] src/duality/duality_rpfp.cpp:2368:18: warning: unused variable ‘ok’ [-Wunused-variable] src/muz/rel/dl_external_relation.cpp:341:26: warning: unused variable ‘m’ [-Wunused-variable] src/muz/rel/dl_finite_product_relation.cpp:1569:46: warning: unused variable ‘plugin’ [-Wunused-variable] src/muz/rel/karr_relation.cpp:127:22: warning: variable ‘processed’ set but not used [-Wunused-but-set-variable] src/muz/rel/udoc_relation.cpp:407:26: warning: unused variable ‘m’ [-Wunused-variable] src/muz/pdr/pdr_farkas_learner.cpp:907:16: warning: unused variable ‘p0’ [-Wunused-variable] src/muz/fp/dl_cmds.cpp:241:14: warning: variable ‘query_exn’ set but not used [-Wunused-but-set-variable] src/opt/hitting_sets.cpp:767:32: warning: unused variable ‘S’ [-Wunused-variable] src/opt/hitting_sets.cpp:773:32: warning: unused variable ‘S’ [-Wunused-variable]

I see other warnings, but I've limited the scope of this bug to unused variables.

NikolajBjorner commented 8 years ago

Note that many of these variables are used in debug assertions, so I would rather just consider warnings in debug builds. We do see such warnings in our build machines and fix them as they appear (the new code in model_based_opt has 3 warnings).

chadrosier commented 8 years ago

Ah, I see. One solution I commonly see in other open-source projects is to use a void cast.

(void)unused-var;