diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 509492067..c4b35bf3d 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -7662,17 +7662,6 @@ class Solver(Z3PPObject): def sexpr(self): """Return a formatted string (in Lisp-like format) with all added constraints. - We say the string is in s-expression format. - - >>> x = Int('x') - >>> s = Solver() - >>> s.add(x > 0) - >>> s.add(x < 2) - >>> print(s.sexpr()) - (declare-fun x () Int) - (assert (> x 0)) - (assert (< x 2)) - """ return Z3_solver_to_string(self.ctx.ref(), self.solver)