diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index aec92b466..9c0c2bee8 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6860,7 +6860,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):