From 7fd93be97b4c0492f6d8dd495447dce57fed13bc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 12 Jul 2024 10:03:03 +0000 Subject: [PATCH] SMT2 back-end: report error when invoking solver fails 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, which is also a legitimate return code when `z3` runs successfully. Thus, use emptiness of `stderr` output as the success criterion, and propagate the messages produced by `run` on stderr to the error-logging output. Fixes: #8362 --- src/solvers/smt2/smt2_dec.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index 19f57ab9a55..af0db57cee7 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "smt2irep.h" +#include + std::string smt2_dect::decision_procedure_text() const { // clang-format off @@ -135,13 +137,14 @@ decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption) UNREACHABLE; } - int res = - run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr()); + run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr()); - if(res<0) + if(!std::filesystem::is_empty(temp_file_stderr())) { 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; }