Skip to content

Commit

Permalink
fix: missing status.stop()
Browse files Browse the repository at this point in the history
  • Loading branch information
daejunpark committed Nov 19, 2024
1 parent e634add commit 1202202
Show file tree
Hide file tree
Showing 2 changed files with 12 additions and 16 deletions.
22 changes: 10 additions & 12 deletions src/halmos/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -734,18 +734,16 @@ def future_callback(future_model):
f"# of potential paths involving assertion violations: {len(future_models)} / {len(result_exs)} (--solver-threads {args.solver_threads})"
)

status = Status("solving:")
status.start()
while True:
if args.early_exit and len(counterexamples) > 0:
break
done = sum(fm.done() for fm in future_models)
total = len(future_models)
if done == total:
break
status.update(f"solving: {done} / {total}")
time.sleep(1)
status.stop()
with Status("solving:") as status:
while True:
if args.early_exit and len(counterexamples) > 0:
break
done = sum(fm.done() for fm in future_models)
total = len(future_models)
if done == total:
break
status.update(f"solving: {done} / {total}")
time.sleep(1)

if args.early_exit:
thread_pool.shutdown(wait=False, cancel_futures=True)
Expand Down
6 changes: 2 additions & 4 deletions src/halmos/sevm.py
Original file line number Diff line number Diff line change
Expand Up @@ -2638,10 +2638,8 @@ def gen_nested_ite(curr: int) -> BitVecRef:
return ZeroExt(248, gen_nested_ite(0))

def run(self, ex0: Exec) -> Iterator[Exec]:
status = Status("pulse:")
status.start()
yield from self._run(ex0, status)
status.stop()
with Status("pulse:") as status:
yield from self._run(ex0, status)

def _run(self, ex0: Exec, status: Status) -> Iterator[Exec]:
step_id: int = 0
Expand Down

0 comments on commit 1202202

Please sign in to comment.