From: Gereon Kremer <gkremer@stanford.edu>
Date: Wed, 1 Dec 2021 16:32:16 +0000 (-0800)
Subject: Add the first example for z3pycompat (#7722)
X-Git-Tag: cvc5-1.0.0~743
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8ce83ed35085fccace319ddd75d6fc1bd9a14a07;p=cvc5.git

Add the first example for z3pycompat (#7722)

This PR adds the first example for the z3py compat API.
---

diff --git a/docs/examples/lineararith.rst b/docs/examples/lineararith.rst
index f6914c88e..bcc7b9a99 100644
--- a/docs/examples/lineararith.rst
+++ b/docs/examples/lineararith.rst
@@ -9,5 +9,6 @@ The two checks are separated by using :code:`push` and :code:`pop`.
 .. api-examples::
     <examples>/api/cpp/linear_arith.cpp
     <examples>/api/java/LinearArith.java
+    <z3pycompat>/test/pgms/example_linear_arith.py
     <examples>/api/python/linear_arith.py
     <examples>/api/smtlib/linear_arith.smt2