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: