From b1ef0c8a7bd433b81c057ecad656608a82a3b7dc Mon Sep 17 00:00:00 2001 From: Pavel Yatcheniy Date: Fri, 5 Feb 2021 18:49:15 +0300 Subject: [Z3] Handle the case when interruption caught by Z3 --- lib/Solver/Z3Solver.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'lib/Solver') 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 #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(); } -- cgit 1.4.1