From 950bd2a9a8c1b42bbe4a3543ddc43a4b581ec925 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Mon, 6 Jan 2025 09:47:29 -0800 Subject: [PATCH] fix: progress display race condition can result in LiveError --- src/halmos/__main__.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index c9b03769..1d4cde8e 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -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, @@ -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: