fix: resolving address alias for infeasible paths

a16z · Sep 19, 2023 · af0f19e · af0f19e
1 parent 59ebac8
commit af0f19e
Showing 1 changed file with 2 additions and 6 deletions.
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
@@ -1524,17 +1524,13 @@ def resolve_address_alias(self, ex: Exec, target: Address) -> Address:
 
         if target not in ex.alias:
             for addr in ex.code:
-                if (
-                    # must equal
-                    ex.check(target != addr) == unsat
-                    # ensure existing path condition is feasible
-                    and ex.check(target == addr) != unsat
-                ):
+                if ex.check(target != addr) == unsat:  # target == addr
                     if self.options.get("debug"):
                         print(
                             f"[DEBUG] Address alias: {hexify(addr)} for {hexify(target)}"
                         )
                     ex.alias[target] = addr
+                    ex.solver.add(target == addr)
                     break
 
         return ex.alias.get(target)