3 files changed, 16 insertions, 1 deletions
diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst
index 91e2493e7..44a177afb 100644
--- a/docs/binary/binary.rst
+++ b/docs/binary/binary.rst
@@ -1,11 +1,18 @@
 Binary Documentation
 ====================
 
+The easiest way to use cvc5 is usually to invoke the cvc5 binary via the command line.
+The :doc:`quickstart guide <quickstart>` gives a short introduction on how to use cvc5 via the SMT-LIBv2
+interface, but cvc5 also supports other :doc:`input languages <languages>`.
+The behavior of cvc5 can be changed with a number of :doc:`options <options>`, and :doc:`output tags <output-tags>` allow to extract structured information about the solving process.
+
+Alternatively, cvc5 features :doc:`several APIs <../api/api>` for different programming languages.
 
 
 .. toctree::
     :maxdepth: 2
 
     quickstart
+    languages
     options
     output-tags
diff --git a/docs/binary/languages.rst b/docs/binary/languages.rst
new file mode 100644
index 000000000..34c536017
--- /dev/null
+++ b/docs/binary/languages.rst
@@ -0,0 +1,8 @@
+Input Languages
+===============
+
+cvc5 supports the following input languages:
+
+* `SMT-LIB v2 <http://smtlib.cs.uiowa.edu/language.shtml>`_
+* `SyGuS-IF <https://sygus.org/language/>`_
+* `TPTP <http://www.tptp.org/>`_
diff --git a/docs/binary/quickstart.rst b/docs/binary/quickstart.rst
index 67280ca45..f3c9c4ad8 100644
--- a/docs/binary/quickstart.rst
+++ b/docs/binary/quickstart.rst
@@ -119,7 +119,7 @@ Example
 | 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
     ../../examples/api/python/quickstart.py
-    ../../examples/api/smtlib/quickstart.smt2