DEBUG

Author: tautschnig

regression/cbmc/Failing_Assert1/z3-wrapper.sh

@@ -2,7 +2,10 @@
 
 # handle output by older Z3 versions where the output was not compatible with
 # current SAT solvers
-
+set -vx
+echo "Trying to run z3"
+z3 --version
+z3 $1
 z3 $1 2>&1 | \
   perl -n -e '
     print "s ".uc($1)."ISFIABLE\n" if(/^((un)?sat)\s*$/);

src/solvers/sat/external_sat.cpp

@@ -62,10 +62,13 @@ void external_satt::write_cnf_file(std::string cnf_file)
 std::string external_satt::execute_solver(std::string cnf_file)
 {
   log.status() << "Invoking SAT solver" << messaget::eom;
+  temporary_filet stderr_file("external-sat", ".log");
   std::ostringstream response_ostream;
-  auto cmd_result = run(solver_cmd, {"", cnf_file}, "", response_ostream, "");
+  auto cmd_result = run(solver_cmd, {"", cnf_file}, "", response_ostream, stderr_file());
 
   log.status() << "Solver returned code: " << cmd_result << messaget::eom;
+  std::ifstream stderr_stream{stderr_file()};
+  response_ostream << stderr_stream.rdbuf();
   return response_ostream.str();
 }
 
@@ -159,7 +162,7 @@ external_satt::resultt external_satt::parse_result(std::string solver_output)
     return resultt::P_SATISFIABLE;
   }
 
-  log.error() << "external SAT solver has provided an unexpected response"
+  log.error() << "external SAT solver has provided an unexpected response: " << solver_output
               << messaget::eom;
   return resultt::P_ERROR;
 }

src/util/run.cpp

@@ -315,6 +315,7 @@ int run(
     // now re-open the file and write the above error message
     std::ofstream stderr_stream(std_error);
     stderr_stream << windows_error;
+    std::cerr << "RUN failed: " << windows_error << std::endl;
 
     return -1;
   }