Skip to content

Commit

Permalink
SMT2 back-end: report error when invoking solver fails
Browse files Browse the repository at this point in the history
Our previous attempt at reporting errors was dead code for `run` never
returns a negative value. When the executable isn't found the return
code was 1, else failures will depend on the solver's return code. Also,
propagate the messages produced by `run` on stderr to the error-logging
output.

Fixes: #8362
  • Loading branch information
tautschnig committed Jul 12, 2024
1 parent 629dbcd commit 2409536
Showing 1 changed file with 4 additions and 2 deletions.
6 changes: 4 additions & 2 deletions src/solvers/smt2/smt2_dec.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -138,10 +138,12 @@ decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption)
int res =
run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr());

if(res<0)
if(res != 0)
{
messaget log{message_handler};
log.error() << "error running SMT2 solver" << messaget::eom;
std::ifstream stderr_stream(temp_file_stderr());
log.error() << "error running SMT2 solver: " << stderr_stream.rdbuf()
<< messaget::eom;
return decision_proceduret::resultt::D_ERROR;
}

Expand Down

0 comments on commit 2409536

Please sign in to comment.