Merge branch 'master' into includesincludes

56 files changed, 322 insertions, 120 deletions

diff --git a/.github/workflows/docs_cleanup.yml b/.github/workflows/docs_cleanup.yml
index 67b5f6b4a..f56a0f595 100644
--- a/.github/workflows/docs_cleanup.yml
+++ b/.github/workflows/docs_cleanup.yml
@@ -4,8 +4,9 @@ on:
     - cron: '0 1 * * SUN'
 
 jobs:
-  build:
+  docs-cleanup:
     runs-on: ubuntu-latest
+    if: github.repository == 'cvc5/cvc5'
     steps:
       - name: Install Packages
         run: |
@@ -58,6 +59,11 @@ jobs:
 
           python3 genindex.py
           git add README.md
-          git commit -m "Update README.md"
+          if git diff --cached --exit-code
+          then
+            echo "Nothing changed"
+          else
+            git commit -m "Update README.md"
+          fi
 
           git push -f
diff --git a/.github/workflows/docs_upload.yml b/.github/workflows/docs_upload.yml
index 356337de6..7346371e3 100644
--- a/.github/workflows/docs_upload.yml
+++ b/.github/workflows/docs_upload.yml
@@ -75,15 +75,21 @@ jobs:
           if [ -n "$NAME" ]; then
             mv docs-new target/docs-$NAME-$HASH
             cd target/
-            rm -f docs-$NAME
-            ln -s docs-$NAME-$HASH docs-$NAME
-            git add docs-$NAME docs-$NAME-$HASH
 
-            python3 genindex.py
-            git add README.md
-            git commit -m "Update docs for $NAME"
+            if diff -r target/docs-master/ target/docs-$NAME-$HASH
+            then
+              echo "Ignored run, documentation is the same as for current master"
+            else
+              rm -f docs-$NAME
+              ln -s docs-$NAME-$HASH docs-$NAME
+              git add docs-$NAME docs-$NAME-$HASH
 
-            git push
+              python3 genindex.py
+              git add README.md
+              git commit -m "Update docs for $NAME"
+
+              git push
+            fi
           else
             echo "Ignored run"
           fi
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 1c6ad1604..d7512e874 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -503,7 +503,6 @@ endif()
 # Add subdirectories
 
 add_subdirectory(src)
-add_subdirectory(test)
 
 if(BUILD_BINDINGS_PYTHON)
   set(BUILD_BINDINGS_PYTHON_VERSION ${PYTHON_VERSION_MAJOR})
@@ -519,6 +518,8 @@ if(BUILD_DOCS)
   add_subdirectory(docs)
 endif()
 
+add_subdirectory(test)
+
 #-----------------------------------------------------------------------------#
 # Package configuration
 #
diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt
index 99c4f3ab3..11c4b8dfd 100644
--- a/docs/CMakeLists.txt
+++ b/docs/CMakeLists.txt
@@ -25,34 +25,38 @@ set(SPHINX_OUTPUT_DIR ${CMAKE_CURRENT_BINARY_DIR}/sphinx)
 
 configure_file(conf.py.in ${CMAKE_CURRENT_BINARY_DIR}/conf.py)
 
-add_custom_target(docs ALL
-                  DEPENDS docs-cpp docs-python gen-options
-                  COMMAND
-                    ${SPHINX_EXECUTABLE} -b html
-                    -c ${CMAKE_CURRENT_BINARY_DIR}
-                    # Tell Breathe where to find the Doxygen output
-                    -Dbreathe_projects.cvc5=${CPP_DOXYGEN_XML_FOLDER}
-                    -Dbreathe_projects.std=${CPP_DOXYGEN_XML_FOLDER}
-                    ${SPHINX_INPUT_DIR} ${SPHINX_OUTPUT_DIR}
-                  WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}
-                  COMMENT "Generating Sphinx Api docs")
+add_custom_target(
+  docs ALL
+  DEPENDS docs-cpp docs-python gen-options
+  COMMAND
+    ${SPHINX_EXECUTABLE} -b html -c ${CMAKE_CURRENT_BINARY_DIR}
+    # Tell Breathe where to find the Doxygen output
+    -Dbreathe_projects.cvc5=${CPP_DOXYGEN_XML_FOLDER}
+    -Dbreathe_projects.std=${CPP_DOXYGEN_XML_FOLDER} ${SPHINX_INPUT_DIR}
+    ${SPHINX_OUTPUT_DIR}
+  WORKING_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}
+  COMMENT "Generating Sphinx Api docs"
+)
 
 set(SPHINX_GH_OUTPUT_DIR ${CMAKE_CURRENT_BINARY_DIR}/sphinx-gh)
-add_custom_target(docs-gh ALL
-                  DEPENDS docs
-                  COMMAND ${CMAKE_COMMAND} -E remove_directory
-                    ${SPHINX_GH_OUTPUT_DIR}
-                  COMMAND ${CMAKE_COMMAND} -E copy_directory
-                    ${SPHINX_OUTPUT_DIR} ${SPHINX_GH_OUTPUT_DIR}
-                  COMMAND ${CMAKE_COMMAND} -E remove_directory
-                    ${SPHINX_GH_OUTPUT_DIR}/_sources
-                  COMMAND ${CMAKE_COMMAND} -E remove
-                    ${SPHINX_GH_OUTPUT_DIR}/objects.inv
-                  COMMAND ${CMAKE_COMMAND} -E rename
-                    ${SPHINX_GH_OUTPUT_DIR}/_static
-                    ${SPHINX_GH_OUTPUT_DIR}/static
-                  COMMAND find ${SPHINX_GH_OUTPUT_DIR} -type f |
-                    xargs sed -i'orig' 's/_static/static/'
-                  COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete
-                  COMMENT "Generating GitHub Api docs")
-
+add_custom_target(
+  docs-gh ALL
+  DEPENDS docs
+  # remove existing sphinx-gh/ directory
+  COMMAND ${CMAKE_COMMAND} -E remove_directory ${SPHINX_GH_OUTPUT_DIR}
+  # copy sphinx/ to sphinx-gh/
+  COMMAND ${CMAKE_COMMAND} -E copy_directory ${SPHINX_OUTPUT_DIR}
+          ${SPHINX_GH_OUTPUT_DIR}
+  # remove leftovers from the build
+  COMMAND ${CMAKE_COMMAND} -E remove_directory ${SPHINX_GH_OUTPUT_DIR}/.doctrees
+          ${SPHINX_GH_OUTPUT_DIR}/_sources ${SPHINX_GH_OUTPUT_DIR}/_static/fonts
+  COMMAND ${CMAKE_COMMAND} -E remove ${SPHINX_GH_OUTPUT_DIR}/objects.inv
+  # rename _static/ to static/ (as jekyll ignores _*/ dirs)
+  COMMAND ${CMAKE_COMMAND} -E rename ${SPHINX_GH_OUTPUT_DIR}/_static
+          ${SPHINX_GH_OUTPUT_DIR}/static
+  COMMAND find ${SPHINX_GH_OUTPUT_DIR} -type f | xargs sed -i'orig'
+          's/_static/static/'
+  COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete
+  # done
+  COMMENT "Generating GitHub Api docs"
+)
diff --git a/docs/_static/custom.css b/docs/_static/custom.css
index 81ecdc936..032efba56 100644
--- a/docs/_static/custom.css
+++ b/docs/_static/custom.css
@@ -32,7 +32,19 @@ a:hover, a:focus {
 }
 
 .wy-side-nav-search > a {
-  color: #fcfffa;
+  color: #ace600;
+}
+
+.wy-side-nav-search > a:hover, > a:focus, > a:visited {
+  color: #ace600;
+}
+
+.wy-breadcrumbs a {
+  color: #739900;
+}
+
+.wy-breadcrumbs a:hover, a:focus {
+  color: #0099e6;
 }
 
 .wy-side-nav-search input[type="text"] {
@@ -56,10 +68,10 @@ a:hover, a:focus {
 }
 
 .wy-nav-top {
-  color: #fcfffa;
+  color: #ace600;
   background-color: #0099e6;
 }
 
 .wy-nav-top a {
-  color: #fcfffa;
+  color: #ace600;
 }
diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst
new file mode 100644
index 000000000..d28beab14
--- /dev/null
+++ b/docs/binary/binary.rst
@@ -0,0 +1,7 @@
+Binary Documentation
+====================
+
+.. toctree::
+    :maxdepth: 2
+
+    options
diff --git a/docs/options.rst b/docs/binary/options.rst
index 6f9c613e7..6f9c613e7 100644
--- a/docs/options.rst
+++ b/docs/binary/options.rst
diff --git a/docs/conf.py.in b/docs/conf.py.in
index 9dc5255bd..6a23ff759 100644
--- a/docs/conf.py.in
+++ b/docs/conf.py.in
@@ -70,6 +70,7 @@ html_css_files = ['custom.css']
 # -- Breathe configuration ---------------------------------------------------
 breathe_default_project = "cvc5"
 breathe_domain_by_extension = {"h" : "cpp"}
+cpp_index_common_prefix = ["cvc5::api::"]
 
 # where to look for include-build-file
 ibf_folders = ['${CMAKE_CURRENT_BINARY_DIR}']
diff --git a/docs/cpp/cpp.rst b/docs/cpp/cpp.rst
index a2e928927..8d302d60c 100644
--- a/docs/cpp/cpp.rst
+++ b/docs/cpp/cpp.rst
@@ -1,3 +1,5 @@
+.. _cpp-api:
+
 C++ API Documentation
 =====================
 
diff --git a/docs/examples/bitvectors.rst b/docs/examples/bitvectors.rst
new file mode 100644
index 000000000..354c86751
--- /dev/null
+++ b/docs/examples/bitvectors.rst
@@ -0,0 +1,8 @@
+Theory of Bit-Vectors
+=====================
+
+
+.. api-examples::
+    ../../examples/api/cpp/bitvectors.cpp
+    ../../examples/api/java/BitVectors.java
+    ../../examples/api/python/bitvectors.py
diff --git a/docs/examples/bitvectors_and_arrays.rst b/docs/examples/bitvectors_and_arrays.rst
new file mode 100644
index 000000000..9d63f36bd
--- /dev/null
+++ b/docs/examples/bitvectors_and_arrays.rst
@@ -0,0 +1,8 @@
+Theory of Bit-Vectors and Arrays
+================================
+
+
+.. api-examples::
+    ../../examples/api/cpp/bitvectors_and_arrays.cpp
+    ../../examples/api/java/BitVectorsAndArrays.java
+    ../../examples/api/python/bitvectors_and_arrays.py
diff --git a/docs/examples/combination.rst b/docs/examples/combination.rst
new file mode 100644
index 000000000..5f301a14f
--- /dev/null
+++ b/docs/examples/combination.rst
@@ -0,0 +1,8 @@
+Theory Combination
+==================
+
+
+.. api-examples::
+    ../../examples/api/cpp/combination.cpp
+    ../../examples/api/java/Combination.java
+    ../../examples/api/python/combination.py
diff --git a/docs/examples/datatypes.rst b/docs/examples/datatypes.rst
index 8200ebb14..abbb16964 100644
--- a/docs/examples/datatypes.rst
+++ b/docs/examples/datatypes.rst
@@ -1,8 +1,8 @@
-Datatypes
-===========
+Theory of Datatypes
+===================
 
 
 .. api-examples::
-    ../../examples/api/datatypes.cpp
+    ../../examples/api/cpp/datatypes.cpp
     ../../examples/api/java/Datatypes.java
     ../../examples/api/python/datatypes.py
diff --git a/docs/examples/examples.rst b/docs/examples/examples.rst
index ff3651857..528566a3e 100644
--- a/docs/examples/examples.rst
+++ b/docs/examples/examples.rst
@@ -1,9 +1,25 @@
 Examples
 ===========
 
+The following examples show how the APIs (:ref:`cpp-api`, :ref:`python-api`) and input languages can be used.
+For every example, the same problem is constructed and solved using different input mechanisms.
+
+
 .. toctree::
     :maxdepth: 2
  
     helloworld
+    exceptions
+    bitvectors
+    bitvectors_and_arrays
+    extract
     datatypes
-    lineararith
\ No newline at end of file
+    floatingpoint
+    lineararith
+    sequences
+    sets
+    strings
+    combination
+    sygus-fun
+    sygus-grammar
+    sygus-inv
\ No newline at end of file
diff --git a/docs/examples/exceptions.rst b/docs/examples/exceptions.rst
new file mode 100644
index 000000000..6598e8fb0
--- /dev/null
+++ b/docs/examples/exceptions.rst
@@ -0,0 +1,7 @@
+Exception Handling
+======================================
+
+
+.. api-examples::
+    ../../examples/api/java/Exceptions.java
+    ../../examples/api/python/exceptions.py
diff --git a/docs/examples/extract.rst b/docs/examples/extract.rst
new file mode 100644
index 000000000..0108de948
--- /dev/null
+++ b/docs/examples/extract.rst
@@ -0,0 +1,7 @@
+Theory of Bit-Vectors: :code:`extract`
+======================================
+
+
+.. api-examples::
+    ../../examples/api/cpp/extract.cpp
+    ../../examples/api/python/extract.py
diff --git a/docs/examples/floatingpoint.rst b/docs/examples/floatingpoint.rst
new file mode 100644
index 000000000..1b09102b2
--- /dev/null
+++ b/docs/examples/floatingpoint.rst
@@ -0,0 +1,7 @@
+Theory of Floating-Points
+======================================
+
+
+.. api-examples::
+    ../../examples/api/java/FloatingPointArith.java
+    ../../examples/api/python/floating_point.py
diff --git a/docs/examples/helloworld.rst b/docs/examples/helloworld.rst
index 202952bb6..cdc424dfa 100644
--- a/docs/examples/helloworld.rst
+++ b/docs/examples/helloworld.rst
@@ -5,6 +5,7 @@ This example shows the very basic usage of the API.
 We create a solver, declare a Boolean variable and check whether it is entailed (by ``true``, as nothing has been asserted to the solver).
 
 .. api-examples::
-    ../../examples/api/helloworld.cpp
+    ../../examples/api/cpp/helloworld.cpp
     ../../examples/api/java/HelloWorld.java
     ../../examples/api/python/helloworld.py
+    ../../examples/api/smtlib/helloworld.smt2
diff --git a/docs/examples/lineararith.rst b/docs/examples/lineararith.rst
index d772edbb3..29d84cae5 100644
--- a/docs/examples/lineararith.rst
+++ b/docs/examples/lineararith.rst
@@ -1,8 +1,13 @@
-Linear Arithmetic
-=================
+Theory of Linear Arithmetic
+===========================
 
+This example asserts three constraints over an integer variable :code:`x` and a real variable :code:`y`.
+Firstly, it checks that these constraints entail an upper bound on the difference :code:`y - x <= 2/3`.
+Secondly, it checks that this bound is tight by asserting :code:`y - x = 2/3` and checking for satisfiability.
+The two checks are separated by using :code:`push` and :code:`pop`.
 
 .. api-examples::
-    ../../examples/api/linear_arith.cpp
+    ../../examples/api/cpp/linear_arith.cpp
     ../../examples/api/java/LinearArith.java
     ../../examples/api/python/linear_arith.py
+    ../../examples/api/smtlib/linear_arith.smt2
diff --git a/docs/examples/sequences.rst b/docs/examples/sequences.rst
new file mode 100644
index 000000000..a6f9e2238
--- /dev/null
+++ b/docs/examples/sequences.rst
@@ -0,0 +1,7 @@
+Theory of Sequences
+===================
+
+
+.. api-examples::
+    ../../examples/api/cpp/sequences.cpp
+    ../../examples/api/python/sequences.py
diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst
new file mode 100644
index 000000000..71a6843c3
--- /dev/null
+++ b/docs/examples/sets.rst
@@ -0,0 +1,7 @@
+Theory of Sets
+=================
+
+
+.. api-examples::
+    ../../examples/api/cpp/sets.cpp
+    ../../examples/api/python/sets.py
diff --git a/docs/examples/strings.rst b/docs/examples/strings.rst
new file mode 100644
index 000000000..87f566363
--- /dev/null
+++ b/docs/examples/strings.rst
@@ -0,0 +1,8 @@
+Theory of Strings
+=================
+
+
+.. api-examples::
+    ../../examples/api/cpp/strings.cpp
+    ../../examples/api/java/Strings.java
+    ../../examples/api/python/strings.py
diff --git a/docs/examples/sygus-fun.rst b/docs/examples/sygus-fun.rst
new file mode 100644
index 000000000..3d5bddff1
--- /dev/null
+++ b/docs/examples/sygus-fun.rst
@@ -0,0 +1,7 @@
+SyGuS: Functions
+===================
+
+
+.. api-examples::
+    ../../examples/api/cpp/sygus-fun.cpp
+    ../../examples/api/python/sygus-fun.py
diff --git a/docs/examples/sygus-grammar.rst b/docs/examples/sygus-grammar.rst
new file mode 100644
index 000000000..3733fe2c3
--- /dev/null
+++ b/docs/examples/sygus-grammar.rst
@@ -0,0 +1,7 @@
+SyGuS: Grammars
+===================
+
+
+.. api-examples::
+    ../../examples/api/cpp/sygus-grammar.cpp
+    ../../examples/api/python/sygus-grammar.py
diff --git a/docs/examples/sygus-inv.rst b/docs/examples/sygus-inv.rst
new file mode 100644
index 000000000..f9698a720
--- /dev/null
+++ b/docs/examples/sygus-inv.rst
@@ -0,0 +1,7 @@
+SyGuS: Invariants
+===================
+
+
+.. api-examples::
+    ../../examples/api/cpp/sygus-inv.cpp
+    ../../examples/api/python/sygus-inv.py
diff --git a/docs/ext/examples.py b/docs/ext/examples.py
index befb6c175..003726de4 100644
--- a/docs/ext/examples.py
+++ b/docs/ext/examples.py
@@ -22,6 +22,7 @@ class APIExamples(Directive):
         '.cpp': {'title': 'C++', 'lang': 'c++'},
         '.java': {'title': 'Java', 'lang': 'java'},
         '.py': {'title': 'Python', 'lang': 'python'},
+        '.smt2': {'title': 'SMT-LIBv2', 'lang': 'lisp'},
     }
 
     # The "arguments" are actually the content of the directive
diff --git a/docs/genindex.rst b/docs/genindex.rst
new file mode 100644
index 000000000..9e530fa2f
--- /dev/null
+++ b/docs/genindex.rst
@@ -0,0 +1,2 @@
+Index
+=====
diff --git a/docs/index.rst b/docs/index.rst
index 8d77790fb..fc82111e2 100644
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -6,17 +6,13 @@
 cvc5 API Documentation
 ======================
 
-
-* :ref:`genindex`
-
-
----------------
-
 .. toctree::
    :maxdepth: 1
 
+   installation/installation
+   binary/binary
    cpp/cpp
    python/python
-   references
    examples/examples
-   options
+   references
+   genindex
diff --git a/docs/installation/installation.rst b/docs/installation/installation.rst
new file mode 100644
index 000000000..e50cd8d4b
--- /dev/null
+++ b/docs/installation/installation.rst
@@ -0,0 +1,2 @@
+Installation
+============
\ No newline at end of file
diff --git a/docs/python/python.rst b/docs/python/python.rst
index 50d9077df..c3e425a7f 100644
--- a/docs/python/python.rst
+++ b/docs/python/python.rst
@@ -1,3 +1,5 @@
+.. _python-api:
+
 Python API Documentation
 ========================
 
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index a7ca31a7a..076715f2e 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -78,7 +78,7 @@ cvc5_add_example(simple_vc_quant_cxx "" "")
 #     # argument to binary (for testing)
 #     ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2)
 
-add_subdirectory(api)
+add_subdirectory(api/cpp)
 # TODO(project issue $206): Port example to new API
 # add_subdirectory(nra-translate)
 # add_subdirectory(sets-translate)
diff --git a/examples/api/CMakeLists.txt b/examples/api/cpp/CMakeLists.txt
index bff7caa4d..bff7caa4d 100644
--- a/examples/api/CMakeLists.txt
+++ b/examples/api/cpp/CMakeLists.txt
diff --git a/examples/api/bitvectors.cpp b/examples/api/cpp/bitvectors.cpp
index 8768bd996..8768bd996 100644
--- a/examples/api/bitvectors.cpp
+++ b/examples/api/cpp/bitvectors.cpp
diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/cpp/bitvectors_and_arrays.cpp
index 547b294a0..547b294a0 100644
--- a/examples/api/bitvectors_and_arrays.cpp
+++ b/examples/api/cpp/bitvectors_and_arrays.cpp
diff --git a/examples/api/combination.cpp b/examples/api/cpp/combination.cpp
index d47897a7c..d47897a7c 100644
--- a/examples/api/combination.cpp
+++ b/examples/api/cpp/combination.cpp
diff --git a/examples/api/datatypes.cpp b/examples/api/cpp/datatypes.cpp
index 76c6da0f0..76c6da0f0 100644
--- a/examples/api/datatypes.cpp
+++ b/examples/api/cpp/datatypes.cpp
diff --git a/examples/api/extract.cpp b/examples/api/cpp/extract.cpp
index d21c59d59..d21c59d59 100644
--- a/examples/api/extract.cpp
+++ b/examples/api/cpp/extract.cpp
diff --git a/examples/api/helloworld.cpp b/examples/api/cpp/helloworld.cpp
index 21eb8e8fc..21eb8e8fc 100644
--- a/examples/api/helloworld.cpp
+++ b/examples/api/cpp/helloworld.cpp
diff --git a/examples/api/linear_arith.cpp b/examples/api/cpp/linear_arith.cpp
index 02ddd956c..02ddd956c 100644
--- a/examples/api/linear_arith.cpp
+++ b/examples/api/cpp/linear_arith.cpp
diff --git a/examples/api/sequences.cpp b/examples/api/cpp/sequences.cpp
index 5ee66048f..5ee66048f 100644
--- a/examples/api/sequences.cpp
+++ b/examples/api/cpp/sequences.cpp
diff --git a/examples/api/sets.cpp b/examples/api/cpp/sets.cpp
index 5c9652707..5c9652707 100644
--- a/examples/api/sets.cpp
+++ b/examples/api/cpp/sets.cpp
diff --git a/examples/api/strings.cpp b/examples/api/cpp/strings.cpp
index a952b31d1..a952b31d1 100644
--- a/examples/api/strings.cpp
+++ b/examples/api/cpp/strings.cpp
diff --git a/examples/api/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp
index 0f96e72a7..0f96e72a7 100644
--- a/examples/api/sygus-fun.cpp
+++ b/examples/api/cpp/sygus-fun.cpp
diff --git a/examples/api/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp
index ce5a1bc8b..ce5a1bc8b 100644
--- a/examples/api/sygus-grammar.cpp
+++ b/examples/api/cpp/sygus-grammar.cpp
diff --git a/examples/api/sygus-inv.cpp b/examples/api/cpp/sygus-inv.cpp
index f658fa33a..f658fa33a 100644
--- a/examples/api/sygus-inv.cpp
+++ b/examples/api/cpp/sygus-inv.cpp
diff --git a/examples/api/utils.cpp b/examples/api/cpp/utils.cpp
index 69676819a..69676819a 100644
--- a/examples/api/utils.cpp
+++ b/examples/api/cpp/utils.cpp
diff --git a/examples/api/utils.h b/examples/api/cpp/utils.h
index 69cddee26..69cddee26 100644
--- a/examples/api/utils.h
+++ b/examples/api/cpp/utils.h
diff --git a/examples/api/smtlib/helloworld.smt2 b/examples/api/smtlib/helloworld.smt2
new file mode 100644
index 000000000..b33689bb7
--- /dev/null
+++ b/examples/api/smtlib/helloworld.smt2
@@ -0,0 +1,4 @@
+(set-logic QF_UF)
+(declare-const |Hello World!| Bool)
+(assert (not |Hello World!|))
+(check-sat)
diff --git a/examples/api/smtlib/linear_arith.smt2 b/examples/api/smtlib/linear_arith.smt2
new file mode 100644
index 000000000..ede655b0e
--- /dev/null
+++ b/examples/api/smtlib/linear_arith.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_LIRA)
+(declare-const x Int)
+(declare-const y Real)
+(assert
+    (and
+        (>= x (* 3 y))
+        (<= x y)
+        (< (- 2) x)
+    )
+)
+(push 1)
+(echo "Checking entailement by asserting the negation")
+(echo "Unsat == ENTAILED")
+(assert (not (<= (- y x) (/ 2 3))))
+(check-sat)
+(pop 1)
+(push 1)
+(echo "Checking that the assertions are consistent")
+(assert (= (- y x) (/ 2 3)))
+(check-sat)
+(pop 1)
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index d56f594ce..53ea46f46 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -112,5 +112,3 @@ add_jar(cvc5jar
 )
 
 add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5)
-
-get_target_property(CVC5_JAR_PATH cvc5jar JAR_FILE)
\ No newline at end of file
diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 281901c1c..007acc64d 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -95,23 +95,23 @@ private:
    */
   Allocator d_allocator;
 
-protected:
+ protected:
   /**
    * Private copy constructor used only by save().  d_list and
    * d_sizeAlloc are not copied: only the base class information and
    * d_size are needed in restore.
    */
-  CDList(const CDList& l) :
-    ContextObj(l),
-    d_list(NULL),
-    d_size(l.d_size),
-    d_callDestructor(false),
-    d_sizeAlloc(0),
-    d_cleanUp(l.d_cleanUp),
-    d_allocator(l.d_allocator) {
-    Debug("cdlist") << "copy ctor: " << this
-                    << " from " << &l
-                    << " size " << d_size << std::endl;
+  CDList(const CDList& l)
+      : ContextObj(l),
+        d_list(nullptr),
+        d_size(l.d_size),
+        d_callDestructor(false),
+        d_sizeAlloc(0),
+        d_cleanUp(l.d_cleanUp),
+        d_allocator(l.d_allocator)
+  {
+    Debug("cdlist") << "copy ctor: " << this << " from " << &l << " size "
+                    << d_size << std::endl;
   }
   CDList& operator=(const CDList& l) = delete;
 
@@ -132,38 +132,50 @@ protected:
     Debug("cdlist") << "grow " << this << " " << getContext()->getLevel()
                     << ": grow!" << std::endl;
 
-    if(d_list == NULL) {
+    const size_t maxSize =
+        std::allocator_traits<AllocatorT>::max_size(d_allocator);
+    if (d_list == nullptr)
+    {
       // Allocate an initial list if one does not yet exist
       d_sizeAlloc = INITIAL_SIZE;
       Debug("cdlist") << "initial grow of cdlist " << this
                       << " level " << getContext()->getLevel()
                       << " to " << d_sizeAlloc << std::endl;
-      if(d_sizeAlloc > d_allocator.max_size()) {
-        d_sizeAlloc = d_allocator.max_size();
+      if (d_sizeAlloc > maxSize)
+      {
+        d_sizeAlloc = maxSize;
       }
-      d_list = d_allocator.allocate(d_sizeAlloc);
-      if(d_list == NULL) {
+      d_list =
+          std::allocator_traits<AllocatorT>::allocate(d_allocator, d_sizeAlloc);
+      if (d_list == nullptr)
+      {
         throw std::bad_alloc();
       }
-    } else {
+    }
+    else
+    {
       // Allocate a new array with double the size
       size_t newSize = GROWTH_FACTOR * d_sizeAlloc;
-      if(newSize > d_allocator.max_size()) {
-        newSize = d_allocator.max_size();
+      if (newSize > maxSize)
+      {
+        newSize = maxSize;
         Assert(newSize > d_sizeAlloc)
             << "cannot request larger list due to allocator limits";
       }
-      T* newList = d_allocator.allocate(newSize);
+      T* newList =
+          std::allocator_traits<AllocatorT>::allocate(d_allocator, newSize);
       Debug("cdlist") << "2x grow of cdlist " << this
                       << " level " << getContext()->getLevel()
                       << " to " << newSize
                       << " (from " << d_list
                       << " to " << newList << ")" << std::endl;
-      if(newList == NULL) {
+      if (newList == nullptr)
+      {
         throw std::bad_alloc();
       }
       std::memcpy(newList, d_list, sizeof(T) * d_sizeAlloc);
-      d_allocator.deallocate(d_list, d_sizeAlloc);
+      std::allocator_traits<AllocatorT>::deallocate(
+          d_allocator, d_list, d_sizeAlloc);
       d_list = newList;
       d_sizeAlloc = newSize;
     }
@@ -222,7 +234,8 @@ protected:
       while(d_size != size) {
         --d_size;
         d_cleanUp(&d_list[d_size]);
-        d_allocator.destroy(&d_list[d_size]);
+        std::allocator_traits<AllocatorT>::destroy(d_allocator,
+                                                   &d_list[d_size]);
       }
     } else {
       d_size = size;
@@ -231,19 +244,20 @@ protected:
 
  public:
   /**
-   * Main constructor: d_list starts as NULL, size is 0
+   * Main constructor: d_list starts as nullptr, size is 0
    */
   CDList(Context* context,
          bool callDestructor = true,
          const CleanUp& cleanup = CleanUp(),
-         const Allocator& alloc = Allocator()) :
-    ContextObj(context),
-    d_list(NULL),
-    d_size(0),
-    d_callDestructor(callDestructor),
-    d_sizeAlloc(0),
-    d_cleanUp(cleanup),
-    d_allocator(alloc) {
+         const Allocator& alloc = Allocator())
+      : ContextObj(context),
+        d_list(nullptr),
+        d_size(0),
+        d_callDestructor(callDestructor),
+        d_sizeAlloc(0),
+        d_cleanUp(cleanup),
+        d_allocator(alloc)
+  {
   }
 
   /**
@@ -256,7 +270,8 @@ protected:
       truncateList(0);
     }
 
-    this->d_allocator.deallocate(this->d_list, this->d_sizeAlloc);
+    std::allocator_traits<AllocatorT>::deallocate(
+        d_allocator, this->d_list, this->d_sizeAlloc);
   }
 
   /**
@@ -295,7 +310,8 @@ protected:
                     << ": construct! at " << d_list
                     << "[" << d_size << "] == " << &d_list[d_size]
                     << std::endl;
-    d_allocator.construct(&d_list[d_size], data);
+    std::allocator_traits<AllocatorT>::construct(
+        d_allocator, &d_list[d_size], data);
     Debug("cdlist") << "push_back " << this
                     << " " << getContext()->getLevel()
                     << ": done..." << std::endl;
@@ -355,7 +371,7 @@ protected:
    * wrapper around a pointer.  Note that for efficiency, we implement
    * only prefix increment and decrement.  Also note that it's OK to
    * create an iterator from an empty, uninitialized list, as begin()
-   * and end() will have the same value (NULL).
+   * and end() will have the same value (nullptr).
    */
   class const_iterator {
     T const* d_it;
@@ -374,7 +390,7 @@ protected:
     typedef const T* pointer;
     typedef const T& reference;
 
-    const_iterator() : d_it(NULL) {}
+    const_iterator() : d_it(nullptr) {}
 
     inline bool operator==(const const_iterator& i) const {
       return d_it == i.d_it;
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index b17f19acd..ac0e487f9 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -92,7 +92,8 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
   // into fixed length regular expressions are easy to handle.
   // the index of _* in re
   unsigned pivotIndex = 0;
-  size_t numPivotIndex = 0;
+  bool hasPivotIndex = false;
+  bool hasFixedLength = true;
   std::vector<Node> childLengths;
   std::vector<Node> childLengthsPostPivot;
   for (unsigned i = 0, size = children.size(); i < size; i++)
@@ -101,34 +102,34 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
     Node fl = RegExpEntail::getFixedLengthForRegexp(c);
     if (fl.isNull())
     {
-      if (numPivotIndex == 0 && c.getKind() == REGEXP_STAR
+      if (!hasPivotIndex && c.getKind() == REGEXP_STAR
           && c[0].getKind() == REGEXP_SIGMA)
       {
-        numPivotIndex = 1;
+        hasPivotIndex = true;
         pivotIndex = i;
         // zero is used in sum below and is used for concat-fixed-len
         fl = zero;
       }
       else
       {
-        numPivotIndex++;
+        hasFixedLength = false;
       }
     }
     if (!fl.isNull())
     {
       childLengths.push_back(fl);
-      if (numPivotIndex > 0)
+      if (hasPivotIndex)
       {
         childLengthsPostPivot.push_back(fl);
       }
     }
   }
-  Node lenSum = childLengths.size() > 1 ? nm->mkNode(PLUS, childLengths)
-                                        : childLengths[0];
-  // if we have at most one pivot index
-  if (numPivotIndex <= 1)
+  Node lenSum = childLengths.size() > 1
+                    ? nm->mkNode(PLUS, childLengths)
+                    : (childLengths.empty() ? zero : childLengths[0]);
+  // if we have a fixed length
+  if (hasFixedLength)
   {
-    bool hasPivotIndex = (numPivotIndex == 1);
     Assert(re.getNumChildren() == children.size());
     std::vector<Node> conc;
     conc.push_back(nm->mkNode(hasPivotIndex ? GEQ : EQUAL, lenx, lenSum));
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3d8016379..01deeaede 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2089,6 +2089,7 @@ set(regress_1_tests
   regress1/strings/issue6271-rnf.smt2
   regress1/strings/issue6271-2-rnf.smt2
   regress1/strings/issue6567-empty-re-range.smt2
+  regress1/strings/issue6604-2.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
diff --git a/test/regress/regress1/strings/issue6604-2.smt2 b/test/regress/regress1/strings/issue6604-2.smt2
new file mode 100644
index 000000000..e28f5dcb5
--- /dev/null
+++ b/test/regress/regress1/strings/issue6604-2.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-exp --re-elim
+; EXPECT: unsat
+(set-logic ALL)
+(declare-const a String)
+(assert (str.in_re a (re.++ (str.to_re "A") re.allchar (str.to_re "A"))))
+(assert (not (str.in_re a (re.++ (str.to_re "A") (re.* (re.++ (str.to_re "A") re.allchar)) re.allchar (str.to_re "A")))))
+(check-sat)
diff --git a/test/unit/api/java/CMakeLists.txt b/test/unit/api/java/CMakeLists.txt
index 0ef649b87..fe497ef3b 100644
--- a/test/unit/api/java/CMakeLists.txt
+++ b/test/unit/api/java/CMakeLists.txt
@@ -17,6 +17,8 @@ find_package(Java REQUIRED)
 include(UseJava)
 find_package(JUnit REQUIRED)
 
+get_target_property(CVC5_JAR_PATH cvc5jar JAR_FILE)
+
 # specify source files for junit tests
 set(java_test_src_files
   ${CMAKE_CURRENT_SOURCE_DIR}/cvc5/SolverTest.java
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index d7f9a4dc3..617f032ab 100644
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -785,30 +785,30 @@ TEST_F(TestApiBlackTerm, getReal)
   ASSERT_TRUE(real8.isRealValue());
   ASSERT_TRUE(real9.isRealValue());
 
-  ASSERT_EQ(std::make_pair(0, 1u), real1.getReal32Value());
-  ASSERT_EQ(std::make_pair(0l, 1ul), real1.getReal64Value());
+  ASSERT_EQ((std::pair<int32_t, uint32_t>(0, 1)), real1.getReal32Value());
+  ASSERT_EQ((std::pair<int64_t, uint64_t>(0, 1)), real1.getReal64Value());
   ASSERT_EQ("0", real1.getRealValue());
 
-  ASSERT_EQ(std::make_pair(0, 1u), real2.getReal32Value());
-  ASSERT_EQ(std::make_pair(0l, 1ul), real2.getReal64Value());
+  ASSERT_EQ((std::pair<int32_t, uint32_t>(0, 1)), real2.getReal32Value());
+  ASSERT_EQ((std::pair<int64_t, uint64_t>(0, 1)), real2.getReal64Value());
   ASSERT_EQ("0", real2.getRealValue());
 
-  ASSERT_EQ(std::make_pair(-17, 1u), real3.getReal32Value());
-  ASSERT_EQ(std::make_pair(-17l, 1ul), real3.getReal64Value());
+  ASSERT_EQ((std::pair<int32_t, uint32_t>(-17, 1)), real3.getReal32Value());
+  ASSERT_EQ((std::pair<int64_t, uint64_t>(-17, 1)), real3.getReal64Value());
   ASSERT_EQ("-17", real3.getRealValue());
 
-  ASSERT_EQ(std::make_pair(-3, 5u), real4.getReal32Value());
-  ASSERT_EQ(std::make_pair(-3l, 5ul), real4.getReal64Value());
+  ASSERT_EQ((std::pair<int32_t, uint32_t>(-3, 5)), real4.getReal32Value());
+  ASSERT_EQ((std::pair<int64_t, uint64_t>(-3, 5)), real4.getReal64Value());
   ASSERT_EQ("-3/5", real4.getRealValue());
 
-  ASSERT_EQ(std::make_pair(127, 10u), real5.getReal32Value());
-  ASSERT_EQ(std::make_pair(127l, 10ul), real5.getReal64Value());
+  ASSERT_EQ((std::pair<int32_t, uint32_t>(127, 10)), real5.getReal32Value());
+  ASSERT_EQ((std::pair<int64_t, uint64_t>(127, 10)), real5.getReal64Value());
   ASSERT_EQ("127/10", real5.getRealValue());
 
-  ASSERT_EQ(std::make_pair(1l, 4294967297ul), real6.getReal64Value());
+  ASSERT_EQ((std::pair<int64_t, uint64_t>(1, 4294967297)), real6.getReal64Value());
   ASSERT_EQ("1/4294967297", real6.getRealValue());
 
-  ASSERT_EQ(std::make_pair(4294967297l, 1ul), real7.getReal64Value());
+  ASSERT_EQ((std::pair<int64_t, uint64_t>(4294967297, 1)), real7.getReal64Value());
   ASSERT_EQ("4294967297", real7.getRealValue());
 
   ASSERT_EQ("1/18446744073709551617", real8.getRealValue());