From 1ada488cb67fef3a4b0e7dbdfa20cf32707dce53 Mon Sep 17 00:00:00 2001
From: Daniel Tang <danielzgtg.opensource@gmail.com>
Date: Sat, 14 Feb 2026 18:13:30 -0500
Subject: [PATCH] Suggest eval in ModelRef.__getitem__ error

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.
---
 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 132edecde..c9156dcd3 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -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):