From cf58fa027d3af2574d9fad14c4718e7970e765bf Mon Sep 17 00:00:00 2001 From: Julien Stephan Date: Sat, 6 Jun 2026 22:24:19 +0200 Subject: [PATCH] python: make Statistics doctests robust to optional ":time" counter (#9729) The doctests for Statistics.__len__ and Statistics.__getitem__ in src/api/python/z3/z3.py asserted a fixed counter count (len(st) == 7). This is fragile because the ":time" entry is only added to statistics when the elapsed wall-clock time of check() is non-zero (see collect_timer_stats in src/solver/check_sat_result.h). On fast native builds, ":time" rounds to 0 and is omitted; under slow environments (e.g. riscv64 under qemu emulation), it becomes non-zero and is included, changing len(st). Fix this by checking the presence of statistics rather than an exact count. Signed-off-by: Julien Stephan --- src/api/python/z3/z3.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 34eb9f5f8..c8574f560 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -7396,8 +7396,8 @@ class Statistics: >>> s.check() sat >>> st = s.statistics() - >>> len(st) - 7 + >>> len(st) > 0 + True """ return int(Z3_stats_size(self.ctx.ref(), self.stats)) @@ -7410,8 +7410,8 @@ class Statistics: >>> s.check() sat >>> st = s.statistics() - >>> len(st) - 7 + >>> len(st) > 0 + True >>> st[0] ('nlsat propagations', 2) >>> st[1]