3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-16 22:01:44 +00:00

Merge pull request #8631 from danielzgtg/doc/solverSexpr

Document example for Solver.sexpr()
This commit is contained in:
Nikolaj Bjorner 2026-02-15 20:51:54 -08:00 committed by GitHub
commit b0ebc78217
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -7668,7 +7668,11 @@ class Solver(Z3PPObject):
>>> s = Solver()
>>> s.add(x > 0)
>>> s.add(x < 2)
>>> r = s.sexpr()
>>> print(s.sexpr())
(declare-fun x () Int)
(assert (> x 0))
(assert (< x 2))
"""
return Z3_solver_to_string(self.ctx.ref(), self.solver)