diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 4e8806d62..56a354ee8 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -395,7 +395,7 @@ class set_option_cmd : public set_get_option_cmd { env_params::updt_params(); ctx.global_params_updated(); } - catch (gparams::exception ex) { + catch (const gparams::exception & ex) { throw cmd_exception(ex.msg()); } } @@ -620,7 +620,7 @@ public: try { ctx.regular_stream() << gparams::get_value(opt) << std::endl; } - catch (gparams::exception ex) { + catch (const gparams::exception & ex) { ctx.print_unsupported(opt, m_line, m_pos); } } diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index 8c2016149..9efb1a383 100644 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -912,7 +912,7 @@ public: if(!add_local_antes(arg, hyps, dk == PR_UNIT_RESOLUTION && i == 0)) return false; } - catch (non_lit_local_ante) { + catch (const non_lit_local_ante &) { std::cout << "\n"; show_step(proof); show(conc(proof)); @@ -1138,7 +1138,7 @@ public: try { res = iproof->make_resolution(pnode,neg,pos); } - catch (const iz3proof::proof_error){ + catch (const iz3proof::proof_error &){ std::cout << "\nresolution error in theory lemma\n"; std::cout << "lits:\n"; for(unsigned j = 0; j < lits.size(); j++) @@ -1212,7 +1212,7 @@ public: try { res = iproof->make_resolution(pnode,neg,pos); } - catch (const iz3proof::proof_error){ + catch (const iz3proof::proof_error &){ std::cout << "\nresolution error in theory lemma\n"; std::cout << "lits:\n"; for(unsigned j = 0; j < lits.size(); j++) @@ -1418,7 +1418,7 @@ public: try { return iproof->make_resolution(pnode,neg,pos); } - catch (const iz3proof::proof_error){ + catch (const iz3proof::proof_error &){ std::cout << "resolution error in unit_resolution, position" << position << "\n"; show_step(proof); throw invalid_lemma(); diff --git a/src/math/subpaving/subpaving.cpp b/src/math/subpaving/subpaving.cpp index 16a9a9a9e..c43b74f0d 100644 --- a/src/math/subpaving/subpaving.cpp +++ b/src/math/subpaving/subpaving.cpp @@ -121,7 +121,7 @@ namespace subpaving { int2mpf(c, m_c); return m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs); } - catch (f2n::exception) { + catch (const f2n::exception &) { throw subpaving::exception(); } } @@ -135,7 +135,7 @@ namespace subpaving { m.set(m_c, k); return reinterpret_cast(m_ctx.mk_ineq(x, m_c, lower, open)); } - catch (f2n::exception) { + catch (const f2n::exception &) { throw subpaving::exception(); } } @@ -178,7 +178,7 @@ namespace subpaving { int2hwf(c, m_c); return m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs); } - catch (f2n::exception) { + catch (const f2n::exception &) { throw subpaving::exception(); } } @@ -192,7 +192,7 @@ namespace subpaving { m.set(m_c, k); return reinterpret_cast(m_ctx.mk_ineq(x, m_c, lower, open)); } - catch (f2n::exception) { + catch (const f2n::exception &) { throw subpaving::exception(); } } @@ -236,7 +236,7 @@ namespace subpaving { int2fpoint(c, m_c); return this->m_ctx.mk_sum(m_c, sz, m_as.c_ptr(), xs); } - catch (typename context_fpoint::numeral_manager::exception) { + catch (const typename context_fpoint::numeral_manager::exception &) { throw subpaving::exception(); } } @@ -251,7 +251,7 @@ namespace subpaving { m.set(m_c, m_qm, k); return reinterpret_cast(this->m_ctx.mk_ineq(x, m_c, lower, open)); } - catch (typename context_fpoint::numeral_manager::exception) { + catch (const typename context_fpoint::numeral_manager::exception &) { throw subpaving::exception(); } } diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h index bb129fee7..cf93fbfad 100644 --- a/src/math/subpaving/subpaving_t_def.h +++ b/src/math/subpaving/subpaving_t_def.h @@ -1310,7 +1310,7 @@ bool context_t::relevant_new_bound(var x, numeral const & k, bool lower, bool TRACE("subpaving_relevant_bound", tout << "new bound is relevant\n";); return true; } - catch (typename C::exception) { + catch (const typename C::exception &) { // arithmetic module failed. set_arith_failed(); return false; @@ -1722,7 +1722,7 @@ void context_t::propagate(node * n, bound * b) { } } } - catch (typename C::exception) { + catch (const typename C::exception &) { // arithmetic module failed, ignore constraint set_arith_failed(); } diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index 9cc13b897..6596cc3b7 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -246,7 +246,7 @@ unsigned read_datalog(char const * file) { false); } - catch (out_of_memory_error) { + catch (const out_of_memory_error &) { std::cout << "\n\nOUT OF MEMORY!\n\n"; display_statistics( std::cout, diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index 6afac32b8..f6e12275f 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -1522,7 +1522,7 @@ public: } SASSERT(ref_count(r) >= 1); } - catch (aig_exception ex) { + catch (const aig_exception & ex) { dec_ref(r); throw ex; } diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp index dd934831c..c78489f21 100644 --- a/src/test/mpff.cpp +++ b/src/test/mpff.cpp @@ -35,7 +35,7 @@ static void tst1() { std::cout << i << ": " << a << "\n"; } } - catch (z3_exception & ex) { + catch (const z3_exception & ex) { std::cout << ex.msg() << "\n"; } } @@ -432,7 +432,7 @@ static void tst_limits(unsigned prec) { m.round_to_plus_inf(); bool overflow = false; try { m.inc(a); } - catch (mpff_manager::overflow_exception) { overflow = true; } + catch (const mpff_manager::overflow_exception &) { overflow = true; } VERIFY(overflow); m.set_max(a); m.dec(a); @@ -446,7 +446,7 @@ static void tst_limits(unsigned prec) { ENSURE(m.eq(a, b)); overflow = true; try { m.dec(a); } - catch (mpff_manager::overflow_exception) { overflow = true; } + catch (const mpff_manager::overflow_exception &) { overflow = true; } ENSURE(overflow); m.round_to_plus_inf(); m.set_min(a);