From 5870211b1eff13ddb397095e499d2f837feda800 Mon Sep 17 00:00:00 2001 From: Mark Mossberg Date: Mon, 10 Apr 2017 17:10:40 -0400 Subject: [PATCH] More gracefully handle uninstalled z3 (#127) * More gracefully handle uninstalled z3 * Use better error --- manticore/core/smtlib/solver.py | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index e0ff9a9..77e8806 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -26,6 +26,10 @@ from visitors import * from ...utils.helpers import issymbolic logger = logging.getLogger("SMT") + +class Z3NotFoundError(EnvironmentError): + pass + class SolverException(Exception): pass @@ -145,7 +149,10 @@ class SMTSolver(Solver): forked in memory or even sent over the network. ''' super(SMTSolver, self).__init__() - version_cmd_output = check_output(self.version_cmd.split()) + try: + version_cmd_output = check_output(self.version_cmd.split()) + except OSError: + raise Z3NotFoundError self._check_solver_version(version_cmd_output) self._proc = None self._constraints = None @@ -160,7 +167,10 @@ class SMTSolver(Solver): def _start_proc(self): ''' Auxiliary method to spawn the external solver pocess''' assert '_proc' not in dir(self) or self._proc is None - self._proc = Popen(self.command.split(' '), stdin=PIPE, stdout=PIPE ) + try: + self._proc = Popen(self.command.split(' '), stdin=PIPE, stdout=PIPE ) + except OSError: + raise Z3NotFoundError # TODO(mark) don't catch this exception in two places #run solver specific initializations for cfg in self.init: