Update smt-logics.rst

SRI-CSL · Jun 24, 2024 · df2b7da · df2b7da
1 parent e3b0884
commit df2b7da
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/doc/sphinx/source/smt-logics.rst b/doc/sphinx/source/smt-logics.rst
@@ -125,6 +125,9 @@ officially part of SMT-LIB.
    | QF_AUF     | Arrays and Uninterpreted Functions           |
    |            |                                              |
    +------------+----------------------------------------------+
+   | QF_AUFBVLIA| Arrays, Uninterpreted Functions, Bitvectors  |
+   |            | and Linear Integer Arithmetic                |
+   +------------+----------------------------------------------+
    | QF_AUFLRA  | Arrays, Uninterpreted Functions,             |
    |            | Linear Real Arithmetic                       |
    +------------+----------------------------------------------+
@@ -137,6 +140,9 @@ officially part of SMT-LIB.
    | QF_LIRA    | Mixed Linear Arithmetic                      |
    |            |                                              |
    +------------+----------------------------------------------+
+   | QF_UFBVLIA | Uninterpreted Functions, Bitvectors          |
+   |            | Linear Integer Arithmetic                    |
+   +------------+----------------------------------------------+
    | QF_UFLIRA  | Uninterpreted Functions and                  |
    |            | Mixed Linear Arithmetic                      |
    +------------+----------------------------------------------+