mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +00:00
Code Activity

Document example for Solver.sexpr()

Browse source
This commit is contained in:
Daniel Tang 2026-02-14 21:51:21 -05:00 • committed by Nikolaj Bjorner
parent 5202b40309
commit c17e8f990e
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/python/z3/z3.py
View file

@ -7905,7 +7905,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)