mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-17 14:21:45 +00:00
Code Activity

Suggest eval in ModelRef.__getitem__ error

Browse source 
This improves the previously cryptic error message. I searched multiple
websites before Google AI suggested using model.eval(arr[0]) for getting
solutions out of arrays.
This commit is contained in:
Daniel Tang 2026-02-14 18:13:30 -05:00
parent e2486eff77
commit 1ada488cb6
No known key found for this signature in database
GPG key ID: E1523803636E3951
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

@ -6849,7 +6849,7 @@ class ModelRef(Z3PPObject):
if isinstance(idx, SortRef):
return self.get_universe(idx)
if z3_debug():
_z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected")
_z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected. Use model.eval instead for complicated expressions")
return None
def decls(self):