Skip to content

Commit

Permalink
fix: progress display race condition can result in LiveError
Browse files Browse the repository at this point in the history
  • Loading branch information
karmacoma-eth committed Jan 6, 2025
1 parent 0ef9341 commit 950bd2a
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions src/halmos/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@
from enum import Enum
from importlib import metadata

import rich
from rich.status import Status
from z3 import (
Z3_OP_CONCAT,
Expand Down Expand Up @@ -753,6 +754,9 @@ def future_callback(future_model):

# display assertion solving progress
if not args.no_status or args.early_exit:
# creating a new live display would fail if the previous one was still active
rich.get_console().clear_live()

with Status("") as status:
while True:
if args.early_exit and len(counterexamples) > 0:
Expand Down

0 comments on commit 950bd2a

Please sign in to comment.