From 33cc8bfbfdd8b2bce66eb926b2426233682573e8 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 7 Jan 2025 12:58:03 -0800 Subject: [PATCH] wip --- src/halmos/sevm.py | 17 ----------------- 1 file changed, 17 deletions(-) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 3c232808..682683f8 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -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 @@ -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