16 files changed, 233 insertions, 204 deletions
diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt
index f460c8841..0eed825eb 100644
--- a/examples/api/python/CMakeLists.txt
+++ b/examples/api/python/CMakeLists.txt
@@ -1,13 +1,18 @@
-#####################
-## CMakeLists.txt
-## Top contributors (to current version):
-##   Andres Noetzli
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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.
+###############################################################################
+# Top contributors (to current version):
+#   Andres Noetzli
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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.
+# #############################################################################
+#
+# The build system configuration.
 ##
+
 set(EXAMPLES_API_PYTHON
   bitvectors_and_arrays
   bitvectors
diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py
index 0bd6dc38a..15973472c 100644
--- a/examples/api/python/bitvectors.py
+++ b/examples/api/python/bitvectors.py
@@ -1,17 +1,19 @@
 #!/usr/bin/env python
-#####################
-## bitvectors.py
-## Top contributors (to current version):
-##   Makai Mann, Aina Niemetz
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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.
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann, Aina Niemetz
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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 cvc5 bit-vector
+# solver through the Python API. This is a direct translation of
+# bitvectors-new.cpp.
 ##
 
 import pycvc4
diff --git a/examples/api/python/bitvectors_and_arrays.py b/examples/api/python/bitvectors_and_arrays.py
index 69acf3de7..8f76ac709 100644
--- a/examples/api/python/bitvectors_and_arrays.py
+++ b/examples/api/python/bitvectors_and_arrays.py
@@ -1,17 +1,19 @@
 #!/usr/bin/env python
-#####################
-## bitvectors_and_arrays.py
-## Top contributors (to current version):
-##   Makai Mann
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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.
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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 cvc5
+# bit-vector and array solvers through the Python API. This is a direct
+# translation of bitvectors_and_arrays-new.cpp.
 ##
 
 import pycvc4
diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py
index 0289f07d3..eb40f6ba3 100644
--- a/examples/api/python/combination.py
+++ b/examples/api/python/combination.py
@@ -1,17 +1,19 @@
 #!/usr/bin/env python
-#####################
-## combination.py
-## Top contributors (to current version):
-##   Makai Mann, Mudathir Mohamed, Aina Niemetz
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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.
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann, Mudathir Mohamed, Aina Niemetz
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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 cvc5 combination
+# solver through the Python API. This is a direct translation of
+# combination-new.cpp.
 ##
 
 import pycvc4
diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
index 1c972da13..e15fe709c 100644
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -1,17 +1,19 @@
 #!/usr/bin/env python
-#####################
-## datatypes.py
-## Top contributors (to current version):
-##   Makai Mann, Andrew Reynolds, Aina Niemetz
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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.
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann, Andrew Reynolds, Aina Niemetz
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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 cvc5 datatypes
+# solver through the Python API. This is a direct translation of
+# datatypes-new.cpp.
 ##
 
 import pycvc4
diff --git a/examples/api/python/exceptions.py b/examples/api/python/exceptions.py
index 017aa82be..c779390d9 100644
--- a/examples/api/python/exceptions.py
+++ b/examples/api/python/exceptions.py
@@ -1,18 +1,19 @@
 #!/usr/bin/env python
-#####################
-## exceptions.py
-## Top contributors (to current version):
-##   Andres Noetzli
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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.
-##
-## Catching CVC4 exceptions with the legacy Python API.
-##
-## A simple demonstration of catching CVC4 execptions with the legacy Python
-## API.
+###############################################################################
+# Top contributors (to current version):
+#   Andres Noetzli
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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.
+# #############################################################################
+#
+# Catching cvc5 exceptions with the legacy Python API.
+#
+# A simple demonstration of catching cvc5 exceptions with the legacy Python API.
 ##
 
 import pycvc4
diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py
index e4378674c..d708a7045 100644
--- a/examples/api/python/extract.py
+++ b/examples/api/python/extract.py
@@ -1,17 +1,19 @@
 #!/usr/bin/env python
-#####################
-## extract.py
-## Top contributors (to current version):
-##   Makai Mann, Aina Niemetz
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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.
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann, Aina Niemetz
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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 cvc5 bit-vector
+# solver through the Python API. This is a direct translation of
+# extract-new.cpp.
 ##
 
 from pycvc4 import Solver
diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py
index d22e2be5f..5444a7df3 100644
--- a/examples/api/python/floating_point.py
+++ b/examples/api/python/floating_point.py
@@ -1,17 +1,19 @@
 #!/usr/bin/env python
-#####################
-## floating_point.py
-## Top contributors (to current version):
-##   Makai Mann, Andres Noetzli
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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.
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann, Andres Noetzli
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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 cvc5
+# floating point solver through the Python API contributed by Eva
+# Darulova. This requires building cvc5 with symfpu.
 ##
 
 import pycvc4
diff --git a/examples/api/python/helloworld.py b/examples/api/python/helloworld.py
index e4ca5ec93..8e585073c 100644
--- a/examples/api/python/helloworld.py
+++ b/examples/api/python/helloworld.py
@@ -1,15 +1,17 @@
 #!/usr/bin/env python
-#####################
-## helloworld.py
-## Top contributors (to current version):
-##   Makai Mann, Aina Niemetz
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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 very simple CVC4 tutorial example, adapted from helloworld-new.cpp
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann, Aina Niemetz
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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 very simple example, adapted from helloworld-new.cpp
 ##
 
 import pycvc4
diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py
index 9b236777a..bc48b452e 100644
--- a/examples/api/python/linear_arith.py
+++ b/examples/api/python/linear_arith.py
@@ -1,17 +1,19 @@
 #!/usr/bin/env python
-#####################
-## linear_arith.py
-## Top contributors (to current version):
-##   Makai Mann, Mudathir Mohamed, Aina Niemetz
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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
-## linear arithmetic solver through the Python API. This is a direct
-## translation of linear_arith-new.cpp.
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann, Mudathir Mohamed, Aina Niemetz
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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 cvc5 linear
+# arithmetic solver through the Python API. This is a direct translation of
+# linear_arith-new.cpp.
 ##
 
 import pycvc4
diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py
index d2cff87bf..fa8c1bc4f 100644
--- a/examples/api/python/sequences.py
+++ b/examples/api/python/sequences.py
@@ -1,17 +1,18 @@
 #!/usr/bin/env python
-#####################
-## sequences.py
-## Top contributors (to current version):
-##   Andres Noetzli, Makai Mann, Mudathir Mohamed
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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
-## strings solver through the Python API. This is a direct translation
-## of sequences.cpp.
+###############################################################################
+# Top contributors (to current version):
+#   Andres Noetzli, Makai Mann, Mudathir Mohamed
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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 cvc5 strings solver
+# through the Python API. This is a direct translation of sequences.cpp.
 ##
 
 import pycvc4
diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py
index 0c5b37ad8..01c14cb87 100644
--- a/examples/api/python/sets.py
+++ b/examples/api/python/sets.py
@@ -1,17 +1,18 @@
 #!/usr/bin/env python
-#####################
-## sets.py
-## Top contributors (to current version):
-##   Makai Mann, Mudathir Mohamed, Aina Niemetz
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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
-## sets solver through the Python API. This is a direct translation
-## of sets-new.cpp.
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann, Mudathir Mohamed, Aina Niemetz
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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 cvc5 sets solver
+# through the Python API. This is a direct translation of sets-new.cpp.
 ##
 
 import pycvc4
diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py
index 22ee24ae1..aa540f89c 100644
--- a/examples/api/python/strings.py
+++ b/examples/api/python/strings.py
@@ -1,17 +1,18 @@
 #!/usr/bin/env python
-#####################
-## strings.py
-## Top contributors (to current version):
-##   Makai Mann, Mudathir Mohamed, Andres Noetzli
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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
-## strings solver through the Python API. This is a direct translation
-## of strings-new.cpp.
+###############################################################################
+# Top contributors (to current version):
+#   Makai Mann, Mudathir Mohamed, Andres Noetzli
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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 cvc5 strings solver
+# through the Python API. This is a direct translation of strings-new.cpp.
 ##
 
 import pycvc4
diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py
index c3ae06140..8c490f47e 100644
--- a/examples/api/python/sygus-fun.py
+++ b/examples/api/python/sygus-fun.py
@@ -1,18 +1,18 @@
 #!/usr/bin/env python
-#####################
-## sygus-fun.py
-## Top contributors (to current version):
-##   Yoni Zohar, Andres Noetzli, Mudathir Mohamed
-## Copyright (c) 2009-2018 by the authors listed in the file AUTHkinds.OrS
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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
-## sygus solver through the Python API. This is a direct
-## translation of sygus-fun.cpp.
+###############################################################################
+# Top contributors (to current version):
+#   Yoni Zohar, Andres Noetzli, Mudathir Mohamed
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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 cvc5 sygus solver
+# through the Python API. This is a direct translation of sygus-fun.cpp.
 ##
 
 import copy
diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py
index 881e488a7..0bcc0815d 100644
--- a/examples/api/python/sygus-grammar.py
+++ b/examples/api/python/sygus-grammar.py
@@ -1,17 +1,19 @@
 #!/usr/bin/env python
-#####################
-## sygus-grammar.py
-## Top contributors (to current version):
-##   Yoni Zohar, Mudathir Mohamed
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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
-## sygus solver through the Python API. This is a direct
-## translation of sygus-grammar.cpp.
+###############################################################################
+# Top contributors (to current version):
+#   Yoni Zohar, Mudathir Mohamed
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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 cvc5
+# sygus solver through the Python API. This is a direct
+# translation of sygus-grammar.cpp.
 ##
 
 import copy
diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py
index 9d2216bef..08a50ce63 100644
--- a/examples/api/python/sygus-inv.py
+++ b/examples/api/python/sygus-inv.py
@@ -1,17 +1,19 @@
 #!/usr/bin/env python
-#####################
-## sygus-inv.py
-## Top contributors (to current version):
-##   Yoni Zohar, Mudathir Mohamed
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 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
-## sygus solver through the Python API. This is a direct
-## translation of sygus-inv.cpp .
+###############################################################################
+# Top contributors (to current version):
+#   Yoni Zohar, Mudathir Mohamed
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 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 cvc5
+# sygus solver through the Python API. This is a direct
+# translation of sygus-inv.cpp .
 ##
 
 import pycvc4