From b9f64a28174b7be12826ecf1e3f58622e32ba6a1 Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Tue, 3 Dec 2024 17:03:13 -0800
Subject: [PATCH] minor updates

---
 pyproject.toml         | 2 +-
 src/halmos/__main__.py | 8 +++++---
 src/halmos/config.py   | 2 +-
 src/halmos/sevm.py     | 8 ++++----
 4 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/pyproject.toml b/pyproject.toml
index 081de0c1..bc6ce5c5 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -26,7 +26,7 @@ dependencies = [
     "toml>=0.10.2",
     "z3-solver==4.12.6.0",
     "eth_hash[pysha3]>=0.7.0",
-    "rich>=13.8.1"
+    "rich>=13.9.4"
 ]
 dynamic = ["version"]
 
diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
index f1f92cf9..751b6e73 100644
--- a/src/halmos/__main__.py
+++ b/src/halmos/__main__.py
@@ -15,6 +15,7 @@
 from concurrent.futures import ThreadPoolExecutor
 from copy import deepcopy
 from dataclasses import asdict, dataclass
+from datetime import timedelta
 from enum import Enum
 from importlib import metadata
 
@@ -735,8 +736,8 @@ def future_callback(future_model):
         )
 
     # display assertion solving progress
-    if not args.no_pulse or args.early_exit:
-        with Status("solving:") as status:
+    if not args.no_status or args.early_exit:
+        with Status("") as status:
             while True:
                 if args.early_exit and len(counterexamples) > 0:
                     break
@@ -744,7 +745,8 @@ def future_callback(future_model):
                 total = len(future_models)
                 if done == total:
                     break
-                status.update(f"solving: {done} / {total}")
+                elapsed = timedelta(seconds=int(timer.elapsed()))
+                status.update(f"[{elapsed}] solving queries: {done} / {total}")
                 time.sleep(0.1)
 
     if args.early_exit:
diff --git a/src/halmos/config.py b/src/halmos/config.py
index 3e6d366b..c889da3b 100644
--- a/src/halmos/config.py
+++ b/src/halmos/config.py
@@ -296,7 +296,7 @@ class Config:
         short="st",
     )
 
-    no_pulse: bool = arg(
+    no_status: bool = arg(
         help="disable progress display",
         global_default=False,
         group=debugging,
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
index 62fae5b7..f4a2d0aa 100644
--- a/src/halmos/sevm.py
+++ b/src/halmos/sevm.py
@@ -1659,7 +1659,7 @@ class Worklist:
     def __init__(self):
         self.stack = []
 
-        # pulse data
+        # status data
         self.completed_paths = 0
         self.start_time = timer()
 
@@ -2640,7 +2640,7 @@ def gen_nested_ite(curr: int) -> BitVecRef:
         return ZeroExt(248, gen_nested_ite(0))
 
     def run(self, ex0: Exec) -> Iterator[Exec]:
-        with Status("pulse:") as status:
+        with Status("") as status:
             yield from self._run(ex0, status)
 
     def _run(self, ex0: Exec, status: Status) -> Iterator[Exec]:
@@ -2667,12 +2667,12 @@ def finalize(ex: Exec):
                 step_id += 1
 
                 # display progress
-                if not self.options.no_pulse and step_id % PULSE_INTERVAL == 0:
+                if not self.options.no_status and step_id % PULSE_INTERVAL == 0:
                     elapsed = timer() - stack.start_time
                     speed = step_id / elapsed
 
                     # hh:mm:ss
-                    elapsed_fmt = str(timedelta(seconds=int(elapsed)))
+                    elapsed_fmt = timedelta(seconds=int(elapsed))
 
                     status.update(
                         f"[{elapsed_fmt}] {speed:.0f} ops/s"