16 files changed, 152 insertions, 147 deletions
diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt
index 0da960513..04bb8a818 100644
--- a/examples/api/python/CMakeLists.txt
+++ b/examples/api/python/CMakeLists.txt
@@ -1,3 +1,13 @@
+#####################
+## CMakeLists.txt
+## Top contributors (to current version):
+##   Andres Noetzli
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
 set(EXAMPLES_API_PYTHON
   bitvectors_and_arrays
   bitvectors
diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py
index f12e79541..c370e50be 100755..100644
--- a/examples/api/python/bitvectors.py
+++ b/examples/api/python/bitvectors.py
@@ -1,19 +1,19 @@
 #!/usr/bin/env python
-
 #####################
-#! \file bitvectors.py
- ## \verbatim
- ## Top contributors (to current version):
- ##   Makai Mann, Aina Niemetz
- ## This file is part of the CVC4 project.
- ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ## in the top-level source directory) and their institutional affiliations.
- ## All rights reserved.  See the file COPYING in the top-level source
- ## directory for licensing information.\endverbatim
- ##
- ## \brief A simple demonstration of the solving capabilities of the CVC4
- ## bit-vector solver through the Python API. This is a direct translation
- ## of bitvectors-new.cpp.
+## bitvectors.py
+## Top contributors (to current version):
+##   Makai Mann, Aina Niemetz
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
+## A simple demonstration of the solving capabilities of the CVC4
+## bit-vector solver through the Python API. This is a direct translation
+## of bitvectors-new.cpp.
+##
+
 import pycvc4
 from pycvc4 import kinds
 
diff --git a/examples/api/python/bitvectors_and_arrays.py b/examples/api/python/bitvectors_and_arrays.py
index 7e3d8f478..be88f690e 100755..100644
--- a/examples/api/python/bitvectors_and_arrays.py
+++ b/examples/api/python/bitvectors_and_arrays.py
@@ -1,19 +1,19 @@
 #!/usr/bin/env python
-
 #####################
-#! \file bitvectors_and_arrays.py
- ## \verbatim
- ## Top contributors (to current version):
- ##   Makai Mann
- ## This file is part of the CVC4 project.
- ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ## in the top-level source directory) and their institutional affiliations.
- ## All rights reserved.  See the file COPYING in the top-level source
- ## directory for licensing information.\endverbatim
- ##
- ## \brief A simple demonstration of the solving capabilities of the CVC4
- ## bit-vector and array solvers through the Python API. This is a direct
- ## translation of bitvectors_and_arrays-new.cpp.
+## bitvectors_and_arrays.py
+## Top contributors (to current version):
+##   Makai Mann
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
+## A simple demonstration of the solving capabilities of the CVC4
+## bit-vector and array solvers through the Python API. This is a direct
+## translation of bitvectors_and_arrays-new.cpp.
+##
+
 import pycvc4
 from pycvc4 import kinds
 
diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py
index bae2b6ef9..253365c9d 100755..100644
--- a/examples/api/python/combination.py
+++ b/examples/api/python/combination.py
@@ -1,19 +1,19 @@
 #!/usr/bin/env python
-
 #####################
-#! \file combination.py
- ## \verbatim
- ## Top contributors (to current version):
- ##   Makai Mann, Aina Niemetz
- ## This file is part of the CVC4 project.
- ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ## in the top-level source directory) and their institutional affiliations.
- ## All rights reserved.  See the file COPYING in the top-level source
- ## directory for licensing information.\endverbatim
- ##
- ## \brief A simple demonstration of the solving capabilities of the CVC4
- ## combination solver through the Python API. This is a direct translation
- ## of combination-new.cpp.
+## combination.py
+## Top contributors (to current version):
+##   Makai Mann, Aina Niemetz, Andrew Reynolds
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
+## A simple demonstration of the solving capabilities of the CVC4
+## combination solver through the Python API. This is a direct translation
+## of combination-new.cpp.
+##
+
 import pycvc4
 from pycvc4 import kinds
 
diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
index 1a67f5661..8ae2c29fd 100755..100644
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -1,19 +1,18 @@
 #!/usr/bin/env python
-
 #####################
-#! \file datatypes.py
- ## \verbatim
- ## Top contributors (to current version):
- ##   Makai Mann
- ## This file is part of the CVC4 project.
- ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ## in the top-level source directory) and their institutional affiliations.
- ## All rights reserved.  See the file COPYING in the top-level source
- ## directory for licensing information.\endverbatim
- ##
- ## \brief A simple demonstration of the solving capabilities of the CVC4
- ## datatypes solver through the Python API. This is a direct translation
- ## of datatypes-new.cpp.
+## datatypes.py
+## Top contributors (to current version):
+##   Makai Mann, Andrew Reynolds, Aina Niemetz
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
+## \brief A simple demonstration of the solving capabilities of the CVC4
+## datatypes solver through the Python API. This is a direct translation
+## of datatypes-new.cpp.
+##
 
 import pycvc4
 from pycvc4 import kinds
diff --git a/examples/api/python/exceptions.py b/examples/api/python/exceptions.py
index 27f068011..97b186b26 100644
--- a/examples/api/python/exceptions.py
+++ b/examples/api/python/exceptions.py
@@ -1,20 +1,19 @@
 #!/usr/bin/env python
-
 #####################
-## \file exceptions.py
-## \verbatim
+## exceptions.py
 ## Top contributors (to current version):
 ##   Andres Noetzli
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
-## in the top-level source directory) and their institutional affiliations.
+## in the top-level source directory and their institutional affiliations.
 ## All rights reserved.  See the file COPYING in the top-level source
-## directory for licensing information.\endverbatim
+## directory for licensing information.
 ##
-## \brief Catching CVC4 exceptions with the legacy Python API.
+## Catching CVC4 exceptions with the legacy Python API.
 ##
 ## A simple demonstration of catching CVC4 execptions with the legacy Python
 ## API.
+##
 
 import pycvc4
 from pycvc4 import kinds
diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py
index 2b8714739..dfe339003 100755..100644
--- a/examples/api/python/extract.py
+++ b/examples/api/python/extract.py
@@ -1,19 +1,18 @@
 #!/usr/bin/env python
-
 #####################
-#! \file extract.py
- ## \verbatim
- ## Top contributors (to current version):
- ##   Makai Mann, Aina Niemetz
- ## This file is part of the CVC4 project.
- ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ## in the top-level source directory) and their institutional affiliations.
- ## All rights reserved.  See the file COPYING in the top-level source
- ## directory for licensing information.\endverbatim
- ##
- ## \brief A simple demonstration of the solving capabilities of the CVC4
- ## bit-vector solver through the Python API. This is a direct translation
- ## of extract-new.cpp.
+## extract.py
+## Top contributors (to current version):
+##   Makai Mann, Aina Niemetz
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
+## A simple demonstration of the solving capabilities of the CVC4
+## bit-vector solver through the Python API. This is a direct translation
+## of extract-new.cpp.
+##
 
 from pycvc4 import Solver
 from pycvc4.kinds import BVExtract, Equal
diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py
index 6fb595e34..bee23b2c7 100755..100644
--- a/examples/api/python/floating_point.py
+++ b/examples/api/python/floating_point.py
@@ -1,19 +1,18 @@
 #!/usr/bin/env python
-
 #####################
-#! \file floating_point.py
- ## \verbatim
- ## Top contributors (to current version):
- ##   Eva Darulova, Makai Mann
- ## This file is part of the CVC4 project.
- ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ## in the top-level source directory) and their institutional affiliations.
- ## All rights reserved.  See the file COPYING in the top-level source
- ## directory for licensing information.\endverbatim
- ##
- ## \brief A simple demonstration of the solving capabilities of the CVC4
- ## floating point solver through the Python API contributed by Eva
- ## Darulova. This requires building CVC4 with symfpu.
+## floating_point.py
+## Top contributors (to current version):
+##   Makai Mann, Andres Noetzli
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
+## A simple demonstration of the solving capabilities of the CVC4
+## floating point solver through the Python API contributed by Eva
+## Darulova. This requires building CVC4 with symfpu.
+##
 
 import pycvc4
 from pycvc4 import kinds
diff --git a/examples/api/python/helloworld.py b/examples/api/python/helloworld.py
index 5607d7f83..2d05822e5 100755..100644
--- a/examples/api/python/helloworld.py
+++ b/examples/api/python/helloworld.py
@@ -1,17 +1,17 @@
 #!/usr/bin/env python
-
 #####################
-#! \file helloworld.py
-## \verbatim
+## helloworld.py
 ## Top contributors (to current version):
 ##   Makai Mann, Aina Niemetz
 ## This file is part of the CVC4 project.
-## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
-## in the top-level source directory) and their institutional affiliations.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
 ## All rights reserved.  See the file COPYING in the top-level source
-## directory for licensing information.\endverbatim
+## directory for licensing information.
+##
+## A very simple CVC4 tutorial example, adapted from helloworld-new.cpp
 ##
-## \brief A very simple CVC4 tutorial example, adapted from helloworld-new.cpp
+
 import pycvc4
 from pycvc4 import kinds
 
diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py
index bab9680b3..f85171150 100755..100644
--- a/examples/api/python/linear_arith.py
+++ b/examples/api/python/linear_arith.py
@@ -1,19 +1,19 @@
 #!/usr/bin/env python
-
 #####################
-#! \file linear_arith.py
-## \verbatim
+## linear_arith.py
 ## Top contributors (to current version):
 ##   Makai Mann, Aina Niemetz
 ## This file is part of the CVC4 project.
-## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
-## in the top-level source directory) and their institutional affiliations.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
 ## All rights reserved.  See the file COPYING in the top-level source
-## directory for licensing information.\endverbatim
+## directory for licensing information.
 ##
-## \brief A simple demonstration of the solving capabilities of the CVC4
+## A simple demonstration of the solving capabilities of the CVC4
 ## linear arithmetic solver through the Python API. This is a direct
 ## translation of linear_arith-new.cpp.
+##
+
 import pycvc4
 from pycvc4 import kinds
 
diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py
index 4498e5153..1b0c34f44 100644
--- a/examples/api/python/sequences.py
+++ b/examples/api/python/sequences.py
@@ -1,19 +1,19 @@
 #!/usr/bin/env python
-
 #####################
-#! \file sequences.py
-## \verbatim
+## sequences.py
 ## Top contributors (to current version):
-##   Andres Noetzli
+##   Andres Noetzli, Makai Mann
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
-## in the top-level source directory) and their institutional affiliations.
+## in the top-level source directory and their institutional affiliations.
 ## All rights reserved.  See the file COPYING in the top-level source
-## directory for licensing information.\endverbatim
+## directory for licensing information.
 ##
-## \brief A simple demonstration of the solving capabilities of the CVC4
+## A simple demonstration of the solving capabilities of the CVC4
 ## strings solver through the Python API. This is a direct translation
 ## of sequences.cpp.
+##
+
 import pycvc4
 from pycvc4 import kinds
 
diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py
index b69c56b56..99a8d4c40 100755..100644
--- a/examples/api/python/sets.py
+++ b/examples/api/python/sets.py
@@ -1,19 +1,19 @@
 #!/usr/bin/env python
-
 #####################
-#! \file sets.py
-## \verbatim
+## sets.py
 ## Top contributors (to current version):
 ##   Makai Mann, Aina Niemetz
 ## This file is part of the CVC4 project.
-## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
-## in the top-level source directory) and their institutional affiliations.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
 ## All rights reserved.  See the file COPYING in the top-level source
-## directory for licensing information.\endverbatim
+## directory for licensing information.
 ##
 ## \brief A simple demonstration of the solving capabilities of the CVC4
 ## sets solver through the Python API. This is a direct translation
 ## of sets-new.cpp.
+##
+
 import pycvc4
 from pycvc4 import kinds
 
diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py
index 58a6f6508..c007b4bb5 100755..100644
--- a/examples/api/python/strings.py
+++ b/examples/api/python/strings.py
@@ -1,19 +1,19 @@
 #!/usr/bin/env python
-
 #####################
-#! \file strings.py
-## \verbatim
+## strings.py
 ## Top contributors (to current version):
-##   Makai Mann
+##   Makai Mann, Andres Noetzli
 ## This file is part of the CVC4 project.
-## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
-## in the top-level source directory) and their institutional affiliations.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
 ## All rights reserved.  See the file COPYING in the top-level source
-## directory for licensing information.\endverbatim
+## directory for licensing information.
 ##
-## \brief A simple demonstration of the solving capabilities of the CVC4
+## A simple demonstration of the solving capabilities of the CVC4
 ## strings solver through the Python API. This is a direct translation
 ## of strings-new.cpp.
+##
+
 import pycvc4
 from pycvc4 import kinds
 
diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py
index 25090bd8f..d331c9f9e 100644
--- a/examples/api/python/sygus-fun.py
+++ b/examples/api/python/sygus-fun.py
@@ -1,19 +1,19 @@
 #!/usr/bin/env python
 #####################
-#! \file sygus-fun.py
-## \verbatim
+## sygus-fun.py
 ## Top contributors (to current version):
-##   Yoni Zohar
-## This file is part of the CVC4 project.
+##   Yoni Zohar, Andres Noetzli
 ## Copyright (c) 2009-2018 by the authors listed in the file AUTHkinds.OrS
-## in the top-level source directory) and their institutional affiliations.
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
 ## All rights reserved.  See the file COPYING in the top-level source
-## directory for licensing information.\endverbatim
+## directory for licensing information.
 ##
-## \brief A simple demonstration of the solving capabilities of the CVC4
+## A simple demonstration of the solving capabilities of the CVC4
 ## sygus solver through the Python API. This is a direct
 ## translation of sygus-fun.cpp.
-#####################
+##
 
 import copy
 import pycvc4
diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py
index efba88286..7a8f89c68 100644
--- a/examples/api/python/sygus-grammar.py
+++ b/examples/api/python/sygus-grammar.py
@@ -1,18 +1,19 @@
 #!/usr/bin/env python
 #####################
-#! \file sygus-grammar.py
-## \verbatim
+## sygus-grammar.py
 ## Top contributors (to current version):
 ##   Yoni Zohar
 ## This file is part of the CVC4 project.
-## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
-## in the top-level source directory) and their institutional affiliations.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
 ## All rights reserved.  See the file COPYING in the top-level source
-## directory for licensing information.\endverbatim
+## directory for licensing information.
 ##
-## \brief A simple demonstration of the solving capabilities of the CVC4
+## A simple demonstration of the solving capabilities of the CVC4
 ## sygus solver through the Python API. This is a direct
 ## translation of sygus-grammar.cpp.
+##
+
 import copy
 import pycvc4
 from pycvc4 import kinds
diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py
index cb21e1849..f71091371 100644
--- a/examples/api/python/sygus-inv.py
+++ b/examples/api/python/sygus-inv.py
@@ -1,20 +1,18 @@
 #!/usr/bin/env python
-
 #####################
-#! \file sygus-inv.py
-## \verbatim
+## sygus-inv.py
 ## Top contributors (to current version):
 ##   Yoni Zohar
 ## This file is part of the CVC4 project.
-## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
-## in the top-level source directory) and their institutional affiliations.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
 ## All rights reserved.  See the file COPYING in the top-level source
-## directory for licensing information.\endverbatim
+## directory for licensing information.
 ##
-## \brief A simple demonstration of the solving capabilities of the CVC4
+## A simple demonstration of the solving capabilities of the CVC4
 ## sygus solver through the Python API. This is a direct
 ## translation of sygus-inv.cpp .
-#####################
+##
 
 import pycvc4
 from pycvc4 import kinds