Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
daejunpark committed Jan 7, 2025
1 parent f1e1d2b commit 33cc8bf
Showing 1 changed file with 0 additions and 17 deletions.
17 changes: 0 additions & 17 deletions src/halmos/sevm.py
Original file line number Diff line number Diff line change
Expand Up @@ -2608,20 +2608,6 @@ def jumpi(
potential_true: bool = ex.check(cond_true) != unsat
potential_false: bool = ex.check(cond_false) != unsat

# if not potential_true and not potential_false:
# print("####")
# print("####")
# print("infeasible", cond_true, cond_false)
# print("####")
# print("####")
# print(ex.path.solver.check())
# print(ex)
# print()
# print(ex.path.solver.unsat_core())
# for xxx in ex.path.solver.assertions():
# print(hexify(str(xxx)))
# print()

# note: both may be false if the previous path condition was considered unknown but turns out to be unsat later

follow_true = False
Expand Down Expand Up @@ -2784,9 +2770,6 @@ def run(self, ex0: Exec) -> Iterator[Exec]:
stack.push(ex0, 0)

def finalize(ex: Exec):
# print("fanalize", ex)
# print()

# if it's at the top-level, there is no callback; yield the current execution state
if ex.callback is None:
stack.completed_paths += 1
Expand Down

0 comments on commit 33cc8bf

Please sign in to comment.