mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +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 • committed by Nikolaj Bjorner
parent 380a8ee20f
commit 5b349f8f9a
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

@ -7097,7 +7097,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):