mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-26 17:02:38 +00:00
Code Activity

Fix some lost Solver.solutions(t) (#10195)

Browse source 
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 <nbjorner@microsoft.com>
This commit is contained in:
Daniel Tang 2026-07-22 21:00:06 -04:00 • committed by GitHub
parent 0f2bc0c36b
commit d91bb5b5fa
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/python/z3/z3.py
View file

@ -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)