diff options
| -rw-r--r-- | lib/Solver/Z3Solver.cpp | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 85943e4f..87ffbdf3 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -8,9 +8,11 @@ //===----------------------------------------------------------------------===// #include "klee/Config/config.h" -#include "klee/Support/OptionCategories.h" #include "klee/Support/ErrorHandling.h" #include "klee/Support/FileHandling.h" +#include "klee/Support/OptionCategories.h" + +#include <csignal> #ifdef ENABLE_Z3 @@ -322,6 +324,9 @@ bool Z3SolverImpl::internalRunSolver( } return true; // success } + if (runStatusCode == SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED) { + raise(SIGINT); + } return false; // failed } @@ -400,6 +405,9 @@ SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse( if (strcmp(reason, "unknown") == 0) { return SolverImpl::SOLVER_RUN_STATUS_FAILURE; } + if (strcmp(reason, "interrupted from keyboard") == 0) { + return SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED; + } klee_warning("Unexpected solver failure. Reason is \"%s,\"\n", reason); abort(); } |