From 3f4895d558bc5f4d59cd50f88167f1575f746e8f Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@stanford.edu>
Date: Tue, 18 Jan 2022 12:32:17 -0800
Subject: [PATCH] Some random documentation issues (#7921)

This PR fixes a few issues in the documentation, mostly about examples that were not included where they should be.
---
 docs/api/cpp/quickstart.rst         | 4 +---
 docs/api/java/quickstart.rst        | 4 +---
 docs/api/python/base/quickstart.rst | 6 ++----
 docs/binary/options.rst             | 2 ++
 docs/binary/quickstart.rst          | 4 +---
 docs/examples/floatingpoint.rst     | 1 +
 6 files changed, 8 insertions(+), 13 deletions(-)

diff --git a/docs/api/cpp/quickstart.rst b/docs/api/cpp/quickstart.rst
index cb3e00fab..88320a508 100644
--- a/docs/api/cpp/quickstart.rst
+++ b/docs/api/cpp/quickstart.rst
@@ -177,11 +177,9 @@ This will print:
 Example
 -------
 
-| The SMT-LIB input for this example can be found at `examples/api/smtlib/quickstart.smt2 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_.
-| The source code for this example can be found at `examples/api/cpp/quickstart.cpp <https://github.com/cvc5/cvc5/blob/master/examples/api/cpp/quickstart.cpp>`_.
-
 .. api-examples::
     <examples>/api/cpp/quickstart.cpp
     <examples>/api/java/QuickStart.java
+    <z3pycompat>/test/pgms/example_quickstart.py
     <examples>/api/python/quickstart.py
     <examples>/api/smtlib/quickstart.smt2
diff --git a/docs/api/java/quickstart.rst b/docs/api/java/quickstart.rst
index 2c986ab55..ccc8a7e13 100644
--- a/docs/api/java/quickstart.rst
+++ b/docs/api/java/quickstart.rst
@@ -181,11 +181,9 @@ This will print:
 Example
 -------
 
-| The SMT-LIB input for this example can be found at `examples/api/smtlib/quickstart.smt2 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_.
-| The source code for this example can be found at `examples/api/java/QuickStart.java <https://github.com/cvc5/cvc5/blob/master/examples/api/java/QuickStart.java>`_.
-
 .. api-examples::
     <examples>/api/java/QuickStart.java
     <examples>/api/cpp/quickstart.cpp
+    <z3pycompat>/test/pgms/example_quickstart.py
     <examples>/api/python/quickstart.py
     <examples>/api/smtlib/quickstart.smt2
diff --git a/docs/api/python/base/quickstart.rst b/docs/api/python/base/quickstart.rst
index ba3360db8..e1c2993b5 100644
--- a/docs/api/python/base/quickstart.rst
+++ b/docs/api/python/base/quickstart.rst
@@ -165,11 +165,9 @@ This will print:
 Example
 -------
 
-| The SMT-LIB input for this example can be found at `examples/api/smtlib/quickstart.smt2 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_.
-| The source code for this example can be found at `examples/api/python/quickstart.py <https://github.com/cvc5/cvc5/blob/master/examples/api/python/quickstart.py>`_.
-
 .. api-examples::
+    <examples>/api/python/quickstart.py
     <examples>/api/cpp/quickstart.cpp
     <examples>/api/java/QuickStart.java
-    <examples>/api/python/quickstart.py
+    <z3pycompat>/test/pgms/example_quickstart.py
     <examples>/api/smtlib/quickstart.smt2
diff --git a/docs/binary/options.rst b/docs/binary/options.rst
index 6f9c613e7..d301c7045 100644
--- a/docs/binary/options.rst
+++ b/docs/binary/options.rst
@@ -1,5 +1,7 @@
 Commandline Options
 ===================
 
+Below is an exhaustive list of commandline options supported by cvc5.
+
 .. include-build-file:: options_generated.rst
 
diff --git a/docs/binary/quickstart.rst b/docs/binary/quickstart.rst
index ddfc7d9f0..b7b35716b 100644
--- a/docs/binary/quickstart.rst
+++ b/docs/binary/quickstart.rst
@@ -115,11 +115,9 @@ This will print:
 Example
 -------
 
-| The SMT-LIB input for this example can be found at `examples/api/smtlib/quickstart.smt2 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_.
-| The source code for this example can be found at `examples/api/smtlib/quickstart.smt2 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_.
-
 .. api-examples::
     <examples>/api/smtlib/quickstart.smt2
     <examples>/api/cpp/quickstart.cpp
     <examples>/api/java/QuickStart.java
+    <z3pycompat>/test/pgms/example_quickstart.py
     <examples>/api/python/quickstart.py
diff --git a/docs/examples/floatingpoint.rst b/docs/examples/floatingpoint.rst
index 5f3dd7855..7cf4e32dd 100644
--- a/docs/examples/floatingpoint.rst
+++ b/docs/examples/floatingpoint.rst
@@ -3,6 +3,7 @@ Theory of Floating-Points
 
 
 .. api-examples::
+    <examples>/api/cpp/floating_point_arith.cpp
     <examples>/api/java/FloatingPointArith.java
     <z3pycompat>/test/pgms/example_floating_point.py
     <examples>/api/python/floating_point.py
-- 
2.30.2