in some cases, such as no constraints in the state, this code was cal…

…ling z3 twice for a single eval. This fixes it
angr · May 30, 2024 · 7501885 · 7501885
1 parent bcb8804
commit 7501885
Showing 1 changed file with 8 additions and 8 deletions.
diff --git a/claripy/frontends/full_frontend.py b/claripy/frontends/full_frontend.py
@@ -141,11 +141,8 @@ def eval(
     ) -> Tuple[float, ...]: ...
 
     def eval(self, e, n, extra_constraints=(), exact=None) -> Tuple[Any, ...]:
-        if not self.satisfiable(extra_constraints=extra_constraints):
-            raise UnsatError("unsat")
-
         try:
-            return tuple(
+            results = tuple(
                 self._solver_backend.eval(
                     e,
                     n,
@@ -154,6 +151,9 @@ def eval(self, e, n, extra_constraints=(), exact=None) -> Tuple[Any, ...]:
                     model_callback=self._model_hook,
                 )
             )
+            if len(results) == 0:
+                raise UnsatError("unsat")
+            return results
         except BackendError as exc:
             raise ClaripyFrontendError("Backend error during eval") from exc
 
@@ -175,17 +175,17 @@ def batch_eval(
     ) -> List[Tuple[float, ...]]: ...
 
     def batch_eval(self, exprs, n, extra_constraints=(), exact=None):
-        if not self.satisfiable(extra_constraints=extra_constraints):
-            raise UnsatError("unsat")
-
         try:
-            return self._solver_backend.batch_eval(
+            results = self._solver_backend.batch_eval(
                 exprs,
                 n,
                 extra_constraints=extra_constraints,
                 solver=self._get_solver(),
                 model_callback=self._model_hook,
             )
+            if len(results) == 0:
+                raise UnsatError("unsat")
+            return results
         except BackendError as e:
             raise ClaripyFrontendError("Backend error during batch_eval") from e