From d5a692fc59fad1b24ee021f4daa3561068cae0c5 Mon Sep 17 00:00:00 2001 From: Mark Mossberg Date: Mon, 9 Apr 2018 10:01:12 -0600 Subject: [PATCH] Rm the slow solver code (#859) --- manticore/core/smtlib/solver.py | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index b1e7bf2..50b35cd 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -358,16 +358,7 @@ class Z3Solver(Solver): value = self._getvalue(var) result.append(value) - # Reset the solver to avoid the incremental mode - # Triggered with two consecutive calls to check-sat - # Yet, if the number of solution is large, sending back - # the whole formula is more expensive - if len(result) < 50: - self._reset(temp_cs.related_to(var)) - for value in result: - self._assert(var != value) - else: - self._assert(var != value) + self._assert(var != value) if len(result) >= maxcnt: if silent: