From d91bb5b5fad8124de15fbdc6ff7e0a2f5628dfe3 Mon Sep 17 00:00:00 2001 From: Daniel Tang Date: Wed, 22 Jul 2026 21:00:06 -0400 Subject: [PATCH] Fix some lost Solver.solutions(t) (#10195) z3-rs correctly used Or. I accidentally forgot that enclosing function call, and had what resulted in And. Test case: ```python s = Solver() x, y, z = Ints("x y z") s.add(x >= 0, x <= 2, y >= 0, y <= 2, z >= 0, z <= 2, x + y + z == 2) # I didn't test multivariable constraints last time fearing nondeterminism # Sorting avoids that print(sorted(map(lambda x: list(map(lambda x: x.as_long(), x)), s.solutions([x, y, z])))) ``` **Before**: `[[0, 1, 1], [2, 0, 0]]` **After**: `[[0, 0, 2], [0, 1, 1], [0, 2, 0], [1, 0, 1], [1, 1, 0], [2, 0, 0]]` Fixes: #8633 --------- Co-authored-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index c3d9ee34d6..2634ca4d3b 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -8098,7 +8098,7 @@ class Solver(Z3PPObject): while s.check() == sat: result = [s.model().eval(t_, model_completion=True) for t_ in t] yield result - s.add(*(t_ != result_ for t_, result_ in zip(t, result))) + s.add(Or(t_ != result_ for t_, result_ in zip(t, result))) else: while s.check() == sat: result = s.model().eval(t, model_completion=True)