From c13095d558dcb01d795c3aeabb7fbf6a461a0c62 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 18 Sep 2023 18:10:13 -0700 Subject: [PATCH] fix: resolving address alias for infeasible paths (#195) --- src/halmos/sevm.py | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index b9c6418e..6ffa3bfd 100644 --- 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)