mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 05:30:51 +00:00
Code Activity

As of GCC8, the throw by value, catch by reference idiom is enforced via -Wcatch-value

Browse source
This commit is contained in:
Daniel Schemmel 2018-05-19 03:47:11 +02:00
parent 5134c16833
commit f02d031d11
No known key found for this signature in database
GPG key ID: A176732062461ECC
7 changed files with 19 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/interp/iz3translate_direct.cpp
View file

@ -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();