diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 44450175e..908286f00 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -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):