Rename occurrences of CVC4 to CVC5. (#6351)

This renames everything but GitHub links and build system related macros. Switching the build system to cvc5 will be the last step in the renaming process.
author: Aina Niemetz <aina.niemetz@gmail.com> 2021-04-15 13:04:55 -0700
committer: GitHub <noreply@github.com> 2021-04-15 20:04:55 +0000
commit: 77bca094a140b35341257f125a55212ff0108250 (patch)
tree: 1d3369b9be5fc4c3e8cb279ae5ea662e59cbcb3e /test
parent: 63647b1d79df6f287ea6599958b16fce44b8271d (diff)
20 files changed, 702 insertions, 702 deletions
diff --git a/test/api/interactive_shell.py b/test/api/interactive_shell.py
index 6660ebe2e..3c8a1d5a8 100644
--- a/test/api/interactive_shell.py
+++ b/test/api/interactive_shell.py
@@ -11,7 +11,7 @@
 # directory for licensing information.
 # #############################################################################
 #
-# A simple test file to interact with CVC4 with line editing
+# A simple test file to interact with cvc5 with line editing
 ##
 
 import sys
@@ -19,15 +19,15 @@ import pexpect
 
 def check_iteractive_shell():
     """
-    Interacts with CVC4's interactive shell and checks that things such a tab
+    Interacts with cvc5's interactive shell and checks that things such a tab
     completion and "pressing up" works.
     """
 
-    # Open CVC4
+    # Open cvc5
     child = pexpect.spawnu("bin/cvc4", timeout=1)
 
-    # We expect to see the CVC4 prompt
-    child.expect("CVC4>")
+    # We expect to see the cvc5 prompt
+    child.expect("cvc5>")
 
     # If we send a line with just 'BOOLE' ...
     child.sendline("BOOLE")
@@ -56,8 +56,8 @@ def check_iteractive_shell():
     # Send enter
     child.sendcontrol("m")
 
-    # We expect to see the CVC4 prompt
-    child.expect("CVC4>")
+    # We expect to see the cvc5 prompt
+    child.expect("cvc5>")
 
     # Now send an up key
     child.send("\033[A")
diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp
index d4aeaf427..3f1fa6733 100644
--- a/test/api/ouroborous.cpp
+++ b/test/api/ouroborous.cpp
@@ -47,7 +47,7 @@ int main()
   {
     return runTest();
   }
-  catch (api::CVC4ApiException& e)
+  catch (api::CVC5ApiException& e)
   {
     std::cerr << e.getMessage() << std::endl;
   }
@@ -97,7 +97,7 @@ std::string parse(std::string instr,
 
   api::Solver solver;
   InputLanguage ilang =
-      input_language == "smt2" ? input::LANG_SMTLIB_V2 : input::LANG_CVC4;
+      input_language == "smt2" ? input::LANG_SMTLIB_V2 : input::LANG_CVC;
 
   solver.setOption("input-language", input_language);
   solver.setOption("output-language", output_language);
@@ -131,10 +131,10 @@ std::string translate(std::string instr,
   std::cout << "==============================================" << std::endl
             << "translating from "
             << (input_language == "smt2" ? input::LANG_SMTLIB_V2
-                                         : input::LANG_CVC4)
+                                         : input::LANG_CVC)
             << " to "
             << (output_language == "smt2" ? output::LANG_SMTLIB_V2
-                                          : output::LANG_CVC4)
+                                          : output::LANG_CVC)
             << " this string:" << std::endl
             << instr << std::endl;
   std::string outstr = parse(instr, input_language, output_language);
@@ -142,7 +142,7 @@ std::string translate(std::string instr,
             << outstr << std::endl
             << "reparsing as "
             << (output_language == "smt2" ? input::LANG_SMTLIB_V2
-                                          : input::LANG_CVC4)
+                                          : input::LANG_CVC)
             << std::endl;
   std::string poutstr = parse(outstr, output_language, output_language);
   assert(outstr == poutstr);
diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp
index 2d37d5c36..c01d16bfc 100644
--- a/test/api/sep_log_api.cpp
+++ b/test/api/sep_log_api.cpp
@@ -85,7 +85,7 @@ int validate_exception(void)
   {
     Term heap_expr = slv.getSeparationHeap();
   }
-  catch (const CVC4ApiException& e)
+  catch (const CVC5ApiException& e)
   {
     caught_on_heap = true;
 
@@ -101,7 +101,7 @@ int validate_exception(void)
   {
     Term nil_expr = slv.getSeparationNilTerm();
   }
-  catch (const CVC4ApiException& e)
+  catch (const CVC5ApiException& e)
   {
     caught_on_nil = true;
 
diff --git a/test/regress/README.md b/test/regress/README.md
index 0dc1d4eb8..f7fb2b6d3 100644
--- a/test/regress/README.md
+++ b/test/regress/README.md
@@ -2,13 +2,13 @@
 
 ## Regression Levels and Running Regression Tests
 
-CVC4's regression tests are divided into 5 levels (level 0 to 4). Higher
+cvc5's regression tests are divided into 5 levels (level 0 to 4). Higher
 regression levels are reserved for longer running regressions. 
 
 For running regressions tests, 
 see the [INSTALL](https://github.com/CVC4/CVC4/blob/master/INSTALL.md#testing-cvc4) file.
 
-By default, each invocation of CVC4 is done with a 10 minute timeout. To use a
+By default, each invocation of cvc5 is done with a 10 minute timeout. To use a
 different timeout, set the `TEST_TIMEOUT` environment variable:
 
 ```
@@ -36,7 +36,7 @@ The following types of regression files are supported:
 
 - `*.smt`: An [SMT1.x](http://smtlib.cs.uiowa.edu/papers/format-v1.2-r06.08.30.pdf) benchmark
 - `*.smt2`: An [SMT 2.x](http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf) benchmark
-- `*.cvc`: A benchmark that uses [CVC4's native input language](https://github.com/CVC4/CVC4/wiki/CVC4-Native-Input-Language)
+- `*.cvc`: A benchmark that uses [cvc5's native input language](https://github.com/CVC4/CVC4/wiki/CVC4-Native-Input-Language)
 - `*.sy`: A [SyGuS](http://sygus.seas.upenn.edu/files/SyGuS-IF.pdf) benchmark
 - `*.p`: A [TPTP](http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html) benchmark
 
@@ -51,7 +51,7 @@ with the following directives:
 % EXIT: 0
 ```
 
-This example expects an exit status of 0 from CVC4, the single line "stderr" on
+This example expects an exit status of 0 from cvc5, the single line "stderr" on
 stderr, and the single line "stdout" on stdout. You can repeat `EXPECT` and
 `EXPECT-ERROR` lines as many times as you like, and at different points of the
 file.  This is useful for multiple queries:
@@ -61,7 +61,7 @@ file.  This is useful for multiple queries:
 QUERY FALSE;
 % EXPECT: VALID
 QUERY TRUE;
-% EXPECT-ERROR: CVC4 Error:
+% EXPECT-ERROR: cvc5 Error:
 % EXPECT-ERROR: Parse Error: regress.cvc:7.13: Unexpected token: 'error'.
 syntax error;
 % EXIT: 1
@@ -71,7 +71,7 @@ Note that the directives are in comments, so if the benchmark file is an smt2
 file for example, the first character would be `;` instead of `%`.
 
 Benchmark files can also specify the command line options to be used when
-executing CVC4, for example:
+executing cvc5, for example:
 
 ```
 % COMMAND-LINE: --incremental
@@ -98,7 +98,7 @@ string `TERM` to make the regression test robust to the actual term printed
 (e.g. there could be multiple non-linear facts and it is ok if any of them is
 printed).
 
-Sometimes, certain benchmarks only apply to certain CVC4
+Sometimes, certain benchmarks only apply to certain cvc5
 configurations. The `REQUIRES` directive can be used to only run
 a given benchmark when a feature is supported. For example:
 
@@ -108,6 +108,6 @@ a given benchmark when a feature is supported. For example:
 
 This benchmark is only run when symfpu has been configured.  Multiple
 `REQUIRES` directives are supported. For a list of features that can be listed
-as a requirement, refer to CVC4's `--show-config` output. Features can also be
+as a requirement, refer to cvc5's `--show-config` output. Features can also be
 excluded by adding the `no-` prefix, e.g. `no-symfpu` means that the test is
 not valid for builds that include symfpu support.
diff --git a/test/regress/regress0/sygus/no-logic.sy b/test/regress/regress0/sygus/no-logic.sy
index 8c9794986..fd63506d2 100644
--- a/test/regress/regress0/sygus/no-logic.sy
+++ b/test/regress/regress0/sygus/no-logic.sy
@@ -1,7 +1,7 @@
 ; REQUIRES: no-competition
 ; COMMAND-LINE: --sygus-out=status --lang=sygus2
 ; EXPECT-ERROR: no-logic.sy:8.10: No set-logic command was given before this point.
-; EXPECT-ERROR: no-logic.sy:8.10: CVC4 will make all theories available.
+; EXPECT-ERROR: no-logic.sy:8.10: cvc5 will make all theories available.
 ; EXPECT-ERROR: no-logic.sy:8.10: Consider setting a stricter logic for (likely) better performance.
 ; EXPECT-ERROR: no-logic.sy:8.10: To suppress this warning in the future use (set-logic ALL).
 ; EXPECT: unsat
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 58e43df36..5ff9628f0 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -103,10 +103,10 @@ def run_process(args, cwd, timeout, s_input=None):
     return out, err, exit_status
 
 
-def get_cvc4_features(cvc4_binary):
-    """Returns a list of features supported by the CVC4 binary `cvc4_binary`."""
+def get_cvc5_features(cvc5_binary):
+    """Returns a list of features supported by the cvc5 binary `cvc5_binary`."""
 
-    output, _, _ = run_process([cvc4_binary, '--show-config'], None, None)
+    output, _, _ = run_process([cvc5_binary, '--show-config'], None, None)
     if isinstance(output, bytes):
         output = output.decode()
 
@@ -124,17 +124,17 @@ def get_cvc4_features(cvc4_binary):
     return features, disabled_features
 
 
-def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc4_binary,
+def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc5_binary,
                   command_line, benchmark_dir, benchmark_filename, timeout):
-    """Runs CVC4 on the file `benchmark_filename` in the directory
-    `benchmark_dir` using the binary `cvc4_binary` with the command line
+    """Runs cvc5 on the file `benchmark_filename` in the directory
+    `benchmark_dir` using the binary `cvc5_binary` with the command line
     options `command_line`. The output is scrubbed using `scrubber` and
     `error_scrubber` for stdout and stderr, respectively. If dump is true, the
-    function first uses CVC4 to read in and dump the benchmark file and then
+    function first uses cvc5 to read in and dump the benchmark file and then
     uses that as input."""
 
     bin_args = wrapper[:]
-    bin_args.append(cvc4_binary)
+    bin_args.append(cvc5_binary)
 
     output = None
     error = None
@@ -173,22 +173,22 @@ def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc4_binary,
 
 
 def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code,
-                   skip_timeout, wrapper, cvc4_binary, benchmark_path,
+                   skip_timeout, wrapper, cvc5_binary, benchmark_path,
                    timeout):
-    """Determines the expected output for a benchmark, runs CVC4 on it and then
+    """Determines the expected output for a benchmark, runs cvc5 on it and then
     checks whether the output corresponds to the expected output. Optionally
     uses a wrapper `wrapper`, tests unsat cores (if check_unsat_cores is true),
     checks proofs (if check_proofs is true), or dumps a benchmark and uses that as
     the input (if dump is true). `use_skip_return_code` enables/disables
     returning 77 when a test is skipped."""
 
-    if not os.access(cvc4_binary, os.X_OK):
+    if not os.access(cvc5_binary, os.X_OK):
         sys.exit(
-            '"{}" does not exist or is not executable'.format(cvc4_binary))
+            '"{}" does not exist or is not executable'.format(cvc5_binary))
     if not os.path.isfile(benchmark_path):
         sys.exit('"{}" does not exist or is not a file'.format(benchmark_path))
 
-    cvc4_features, cvc4_disabled_features = get_cvc4_features(cvc4_binary)
+    cvc5_features, cvc5_disabled_features = get_cvc5_features(cvc5_binary)
 
     basic_command_line_args = []
 
@@ -287,18 +287,18 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code,
         if req_feature.startswith("no-"):
             req_feature = req_feature[len("no-"):]
             is_negative = True
-        if req_feature not in (cvc4_features + cvc4_disabled_features):
+        if req_feature not in (cvc5_features + cvc5_disabled_features):
             print(
                 'Illegal requirement in regression: {}\nAllowed requirements: {}'
                 .format(req_feature,
-                        ' '.join(cvc4_features + cvc4_disabled_features)))
+                        ' '.join(cvc5_features + cvc5_disabled_features)))
             return EXIT_FAILURE
         if is_negative:
-            if req_feature in cvc4_features:
+            if req_feature in cvc5_features:
                 print('1..0 # Skipped regression: not valid with {}'.format(
                     req_feature))
                 return (EXIT_SKIP if use_skip_return_code else EXIT_OK)
-        elif req_feature not in cvc4_features:
+        elif req_feature not in cvc5_features:
             print('1..0 # Skipped regression: {} not supported'.format(
                 req_feature))
             return (EXIT_SKIP if use_skip_return_code else EXIT_OK)
@@ -360,14 +360,14 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code,
         for extra_arg in extra_command_line_args:
             command_line_args_configs.append(all_args + [extra_arg])
 
-    # Run CVC4 on the benchmark with the different option sets and check
+    # Run cvc5 on the benchmark with the different option sets and check
     # whether the exit status, stdout output, stderr output are as expected.
     print('1..{}'.format(len(command_line_args_configs)))
     print('# Starting')
     exit_code = EXIT_OK
     for command_line_args in command_line_args_configs:
         output, error, exit_status = run_benchmark(dump, wrapper, scrubber,
-                                                   error_scrubber, cvc4_binary,
+                                                   error_scrubber, cvc5_binary,
                                                    command_line_args,
                                                    benchmark_dir,
                                                    benchmark_basename, timeout)
@@ -444,7 +444,7 @@ def main():
     parser.add_argument('--no-check-proofs', dest='check_proofs',
                         action='store_false')
     parser.add_argument('wrapper', nargs='*')
-    parser.add_argument('cvc4_binary')
+    parser.add_argument('cvc5_binary')
     parser.add_argument('benchmark')
 
     argv = sys.argv[1:]
@@ -454,7 +454,7 @@ def main():
 
     args = parser.parse_args(argv)
 
-    cvc4_binary = os.path.abspath(args.cvc4_binary)
+    cvc5_binary = os.path.abspath(args.cvc5_binary)
 
     wrapper = args.wrapper
     if os.environ.get('VALGRIND') == '1' and not wrapper:
@@ -464,7 +464,7 @@ def main():
 
     return run_regression(args.check_unsat_cores, args.check_proofs, args.dump,
                           args.use_skip_return_code, args.skip_timeout,
-                          wrapper, cvc4_binary, args.benchmark, timeout)
+                          wrapper, cvc5_binary, args.benchmark, timeout)
 
 
 if __name__ == "__main__":
diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp
index 7c85f84e0..3fbdcc0b5 100644
--- a/test/unit/api/datatype_api_black.cpp
+++ b/test/unit/api/datatype_api_black.cpp
@@ -37,7 +37,7 @@ TEST_F(TestApiBlackDatatype, mkDatatypeSort)
   Datatype d = listSort.getDatatype();
   DatatypeConstructor consConstr = d[0];
   DatatypeConstructor nilConstr = d[1];
-  ASSERT_THROW(d[2], CVC4ApiException);
+  ASSERT_THROW(d[2], CVC5ApiException);
   ASSERT_NO_THROW(consConstr.getConstructorTerm());
   ASSERT_NO_THROW(nilConstr.getConstructorTerm());
 }
@@ -104,7 +104,7 @@ TEST_F(TestApiBlackDatatype, mkDatatypeSorts)
   std::vector<DatatypeDecl> dtdeclsBad;
   DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD");
   dtdeclsBad.push_back(emptyD);
-  ASSERT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackDatatype, datatypeStructs)
@@ -118,7 +118,7 @@ TEST_F(TestApiBlackDatatype, datatypeStructs)
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
   Sort nullSort;
-  ASSERT_THROW(cons.addSelector("null", nullSort), CVC4ApiException);
+  ASSERT_THROW(cons.addSelector("null", nullSort), CVC5ApiException);
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
@@ -200,14 +200,14 @@ TEST_F(TestApiBlackDatatype, datatypeNames)
   ASSERT_EQ(dt.getName(), std::string("list"));
   ASSERT_NO_THROW(dt.getConstructor("nil"));
   ASSERT_NO_THROW(dt["cons"]);
-  ASSERT_THROW(dt.getConstructor("head"), CVC4ApiException);
-  ASSERT_THROW(dt.getConstructor(""), CVC4ApiException);
+  ASSERT_THROW(dt.getConstructor("head"), CVC5ApiException);
+  ASSERT_THROW(dt.getConstructor(""), CVC5ApiException);
 
   DatatypeConstructor dcons = dt[0];
   ASSERT_EQ(dcons.getName(), std::string("cons"));
   ASSERT_NO_THROW(dcons.getSelector("head"));
   ASSERT_NO_THROW(dcons["tail"]);
-  ASSERT_THROW(dcons.getSelector("cons"), CVC4ApiException);
+  ASSERT_THROW(dcons.getSelector("cons"), CVC5ApiException);
 
   // get selector
   DatatypeSelector dselTail = dcons[1];
@@ -215,7 +215,7 @@ TEST_F(TestApiBlackDatatype, datatypeNames)
   ASSERT_EQ(dselTail.getRangeSort(), dtypeSort);
 
   // possible to construct null datatype declarations if not using solver
-  ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException);
+  ASSERT_THROW(DatatypeDecl().getName(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackDatatype, parametricDatatype)
@@ -543,7 +543,7 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons)
   ASSERT_NO_THROW(testConsTerm = nilc.getSpecializedConstructorTerm(listInt));
   ASSERT_NE(testConsTerm, nilc.getConstructorTerm());
   // error to get the specialized constructor term for Int
-  ASSERT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException);
+  ASSERT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC5ApiException);
 }
 }  // namespace test
 }  // namespace cvc5
diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp
index ccab121db..7b7556539 100644
--- a/test/unit/api/grammar_black.cpp
+++ b/test/unit/api/grammar_black.cpp
@@ -39,15 +39,15 @@ TEST_F(TestApiBlackGrammar, addRule)
   ASSERT_NO_THROW(g.addRule(start, d_solver.mkBoolean(false)));
 
   ASSERT_THROW(g.addRule(nullTerm, d_solver.mkBoolean(false)),
-               CVC4ApiException);
-  ASSERT_THROW(g.addRule(start, nullTerm), CVC4ApiException);
-  ASSERT_THROW(g.addRule(nts, d_solver.mkBoolean(false)), CVC4ApiException);
-  ASSERT_THROW(g.addRule(start, d_solver.mkInteger(0)), CVC4ApiException);
-  ASSERT_THROW(g.addRule(start, nts), CVC4ApiException);
+               CVC5ApiException);
+  ASSERT_THROW(g.addRule(start, nullTerm), CVC5ApiException);
+  ASSERT_THROW(g.addRule(nts, d_solver.mkBoolean(false)), CVC5ApiException);
+  ASSERT_THROW(g.addRule(start, d_solver.mkInteger(0)), CVC5ApiException);
+  ASSERT_THROW(g.addRule(start, nts), CVC5ApiException);
 
   d_solver.synthFun("f", {}, boolean, g);
 
-  ASSERT_THROW(g.addRule(start, d_solver.mkBoolean(false)), CVC4ApiException);
+  ASSERT_THROW(g.addRule(start, d_solver.mkBoolean(false)), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackGrammar, addRules)
@@ -64,16 +64,16 @@ TEST_F(TestApiBlackGrammar, addRules)
   ASSERT_NO_THROW(g.addRules(start, {d_solver.mkBoolean(false)}));
 
   ASSERT_THROW(g.addRules(nullTerm, {d_solver.mkBoolean(false)}),
-               CVC4ApiException);
-  ASSERT_THROW(g.addRules(start, {nullTerm}), CVC4ApiException);
-  ASSERT_THROW(g.addRules(nts, {d_solver.mkBoolean(false)}), CVC4ApiException);
-  ASSERT_THROW(g.addRules(start, {d_solver.mkInteger(0)}), CVC4ApiException);
-  ASSERT_THROW(g.addRules(start, {nts}), CVC4ApiException);
+               CVC5ApiException);
+  ASSERT_THROW(g.addRules(start, {nullTerm}), CVC5ApiException);
+  ASSERT_THROW(g.addRules(nts, {d_solver.mkBoolean(false)}), CVC5ApiException);
+  ASSERT_THROW(g.addRules(start, {d_solver.mkInteger(0)}), CVC5ApiException);
+  ASSERT_THROW(g.addRules(start, {nts}), CVC5ApiException);
 
   d_solver.synthFun("f", {}, boolean, g);
 
   ASSERT_THROW(g.addRules(start, {d_solver.mkBoolean(false)}),
-               CVC4ApiException);
+               CVC5ApiException);
 }
 
 TEST_F(TestApiBlackGrammar, addAnyConstant)
@@ -89,12 +89,12 @@ TEST_F(TestApiBlackGrammar, addAnyConstant)
   ASSERT_NO_THROW(g.addAnyConstant(start));
   ASSERT_NO_THROW(g.addAnyConstant(start));
 
-  ASSERT_THROW(g.addAnyConstant(nullTerm), CVC4ApiException);
-  ASSERT_THROW(g.addAnyConstant(nts), CVC4ApiException);
+  ASSERT_THROW(g.addAnyConstant(nullTerm), CVC5ApiException);
+  ASSERT_THROW(g.addAnyConstant(nts), CVC5ApiException);
 
   d_solver.synthFun("f", {}, boolean, g);
 
-  ASSERT_THROW(g.addAnyConstant(start), CVC4ApiException);
+  ASSERT_THROW(g.addAnyConstant(start), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackGrammar, addAnyVariable)
@@ -113,12 +113,12 @@ TEST_F(TestApiBlackGrammar, addAnyVariable)
   ASSERT_NO_THROW(g1.addAnyVariable(start));
   ASSERT_NO_THROW(g2.addAnyVariable(start));
 
-  ASSERT_THROW(g1.addAnyVariable(nullTerm), CVC4ApiException);
-  ASSERT_THROW(g1.addAnyVariable(nts), CVC4ApiException);
+  ASSERT_THROW(g1.addAnyVariable(nullTerm), CVC5ApiException);
+  ASSERT_THROW(g1.addAnyVariable(nts), CVC5ApiException);
 
   d_solver.synthFun("f", {}, boolean, g1);
 
-  ASSERT_THROW(g1.addAnyVariable(start), CVC4ApiException);
+  ASSERT_THROW(g1.addAnyVariable(start), CVC5ApiException);
 }
 }  // namespace test
 }  // namespace cvc5
diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp
index 0b67c0013..e7b83f455 100644
--- a/test/unit/api/op_black.cpp
+++ b/test/unit/api/op_black.cpp
@@ -43,13 +43,13 @@ TEST_F(TestApiBlackOp, isNull)
 TEST_F(TestApiBlackOp, opFromKind)
 {
   ASSERT_NO_THROW(d_solver.mkOp(PLUS));
-  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackOp, getIndicesString)
 {
   Op x;
-  ASSERT_THROW(x.getIndices<std::string>(), CVC4ApiException);
+  ASSERT_THROW(x.getIndices<std::string>(), CVC5ApiException);
 
   Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4);
   ASSERT_TRUE(divisible_ot.isIndexed());
@@ -59,7 +59,7 @@ TEST_F(TestApiBlackOp, getIndicesString)
   Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test");
   std::string record_update_idx = record_update_ot.getIndices<std::string>();
   ASSERT_EQ(record_update_idx, "test");
-  ASSERT_THROW(record_update_ot.getIndices<uint32_t>(), CVC4ApiException);
+  ASSERT_THROW(record_update_ot.getIndices<uint32_t>(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackOp, getIndicesUint)
@@ -70,7 +70,7 @@ TEST_F(TestApiBlackOp, getIndicesUint)
   ASSERT_EQ(bitvector_repeat_idx, 5);
   ASSERT_THROW(
       (bitvector_repeat_ot.getIndices<std::pair<uint32_t, uint32_t>>()),
-      CVC4ApiException);
+      CVC5ApiException);
 
   Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
   uint32_t bitvector_zero_extend_idx =
@@ -109,7 +109,7 @@ TEST_F(TestApiBlackOp, getIndicesUint)
   Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5);
   uint32_t tuple_update_idx = tuple_update_ot.getIndices<uint32_t>();
   ASSERT_EQ(tuple_update_idx, 5);
-  ASSERT_THROW(tuple_update_ot.getIndices<std::string>(), CVC4ApiException);
+  ASSERT_THROW(tuple_update_ot.getIndices<std::string>(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackOp, getIndicesPairUint)
@@ -168,7 +168,7 @@ TEST_F(TestApiBlackOp, getIndicesPairUint)
   ASSERT_TRUE((floatingpoint_to_fp_generic_indices
                == std::pair<uint32_t, uint32_t>{4, 25}));
   ASSERT_THROW(floatingpoint_to_fp_generic_ot.getIndices<std::string>(),
-               CVC4ApiException);
+               CVC5ApiException);
 }
 
 TEST_F(TestApiBlackOp, opScopingToString)
diff --git a/test/unit/api/op_white.cpp b/test/unit/api/op_white.cpp
index 4953cdd60..39952739b 100644
--- a/test/unit/api/op_white.cpp
+++ b/test/unit/api/op_white.cpp
@@ -29,7 +29,7 @@ TEST_F(TestApiWhiteOp, opFromKind)
 {
   Op plus(&d_solver, PLUS);
   ASSERT_FALSE(plus.isIndexed());
-  ASSERT_THROW(plus.getIndices<uint32_t>(), CVC4ApiException);
+  ASSERT_THROW(plus.getIndices<uint32_t>(), CVC5ApiException);
   ASSERT_EQ(plus, d_solver.mkOp(PLUS));
 }
 }  // namespace test
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index c5cdf4f8c..361bfa8aa 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -30,7 +30,7 @@ TEST_F(TestApiBlackSolver, recoverableException)
   d_solver.setOption("produce-models", "true");
   Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
   d_solver.assertFormula(x.eqTerm(x).notTerm());
-  ASSERT_THROW(d_solver.getValue(x), CVC4ApiRecoverableException);
+  ASSERT_THROW(d_solver.getValue(x), CVC5ApiRecoverableException);
 }
 
 TEST_F(TestApiBlackSolver, supportsFloatingPoint)
@@ -42,7 +42,7 @@ TEST_F(TestApiBlackSolver, supportsFloatingPoint)
   else
   {
     ASSERT_THROW(d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN),
-                 CVC4ApiException);
+                 CVC5ApiException);
   }
 }
 
@@ -84,7 +84,7 @@ TEST_F(TestApiBlackSolver, getRoundingModeSort)
   }
   else
   {
-    ASSERT_THROW(d_solver.getRoundingModeSort(), CVC4ApiException);
+    ASSERT_THROW(d_solver.getRoundingModeSort(), CVC5ApiException);
   }
 }
 
@@ -109,13 +109,13 @@ TEST_F(TestApiBlackSolver, mkArraySort)
   }
 
   Solver slv;
-  ASSERT_THROW(slv.mkArraySort(boolSort, boolSort), CVC4ApiException);
+  ASSERT_THROW(slv.mkArraySort(boolSort, boolSort), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkBitVectorSort)
 {
   ASSERT_NO_THROW(d_solver.mkBitVectorSort(32));
-  ASSERT_THROW(d_solver.mkBitVectorSort(0), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkBitVectorSort(0), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkFloatingPointSort)
@@ -123,12 +123,12 @@ TEST_F(TestApiBlackSolver, mkFloatingPointSort)
   if (d_solver.supportsFloatingPoint())
   {
     ASSERT_NO_THROW(d_solver.mkFloatingPointSort(4, 8));
-    ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC4ApiException);
-    ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC4ApiException);
+    ASSERT_THROW(d_solver.mkFloatingPointSort(0, 8), CVC5ApiException);
+    ASSERT_THROW(d_solver.mkFloatingPointSort(4, 0), CVC5ApiException);
   }
   else
   {
-    ASSERT_THROW(d_solver.mkFloatingPointSort(4, 8), CVC4ApiException);
+    ASSERT_THROW(d_solver.mkFloatingPointSort(4, 8), CVC5ApiException);
   }
 }
 
@@ -143,10 +143,10 @@ TEST_F(TestApiBlackSolver, mkDatatypeSort)
   ASSERT_NO_THROW(d_solver.mkDatatypeSort(dtypeSpec));
 
   Solver slv;
-  ASSERT_THROW(slv.mkDatatypeSort(dtypeSpec), CVC4ApiException);
+  ASSERT_THROW(slv.mkDatatypeSort(dtypeSpec), CVC5ApiException);
 
   DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list");
-  ASSERT_THROW(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkDatatypeSorts)
@@ -168,11 +168,11 @@ TEST_F(TestApiBlackSolver, mkDatatypeSorts)
   std::vector<DatatypeDecl> decls = {dtypeSpec1, dtypeSpec2};
   ASSERT_NO_THROW(d_solver.mkDatatypeSorts(decls));
 
-  ASSERT_THROW(slv.mkDatatypeSorts(decls), CVC4ApiException);
+  ASSERT_THROW(slv.mkDatatypeSorts(decls), CVC5ApiException);
 
   DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list");
   std::vector<DatatypeDecl> throwsDecls = {throwsDtypeSpec};
-  ASSERT_THROW(d_solver.mkDatatypeSorts(throwsDecls), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkDatatypeSorts(throwsDecls), CVC5ApiException);
 
   /* with unresolved sorts */
   Sort unresList = d_solver.mkUninterpretedSort("ulist");
@@ -187,7 +187,7 @@ TEST_F(TestApiBlackSolver, mkDatatypeSorts)
   std::vector<DatatypeDecl> udecls = {ulist};
   ASSERT_NO_THROW(d_solver.mkDatatypeSorts(udecls, unresSorts));
 
-  ASSERT_THROW(slv.mkDatatypeSorts(udecls, unresSorts), CVC4ApiException);
+  ASSERT_THROW(slv.mkDatatypeSorts(udecls, unresSorts), CVC5ApiException);
 
   /* Note: More tests are in datatype_api_black. */
 }
@@ -203,9 +203,9 @@ TEST_F(TestApiBlackSolver, mkFunctionSort)
   // non-first-class arguments are not allowed
   Sort reSort = d_solver.getRegExpSort();
   ASSERT_THROW(d_solver.mkFunctionSort(reSort, d_solver.getIntegerSort()),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_NO_THROW(d_solver.mkFunctionSort(
       {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()},
       d_solver.getIntegerSort()));
@@ -218,24 +218,24 @@ TEST_F(TestApiBlackSolver, mkFunctionSort)
   ASSERT_THROW(d_solver.mkFunctionSort({d_solver.getIntegerSort(),
                                         d_solver.mkUninterpretedSort("u")},
                                        funSort2),
-               CVC4ApiException);
+               CVC5ApiException);
 
   Solver slv;
   ASSERT_THROW(slv.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
                                   d_solver.getIntegerSort()),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.mkFunctionSort(slv.mkUninterpretedSort("u"),
                                   d_solver.getIntegerSort()),
-               CVC4ApiException);
+               CVC5ApiException);
   std::vector<Sort> sorts1 = {d_solver.getBooleanSort(),
                               slv.getIntegerSort(),
                               d_solver.getIntegerSort()};
   std::vector<Sort> sorts2 = {slv.getBooleanSort(), slv.getIntegerSort()};
   ASSERT_NO_THROW(slv.mkFunctionSort(sorts2, slv.getIntegerSort()));
   ASSERT_THROW(slv.mkFunctionSort(sorts1, slv.getIntegerSort()),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.mkFunctionSort(sorts2, d_solver.getIntegerSort()),
-               CVC4ApiException);
+               CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkParamSort)
@@ -247,7 +247,7 @@ TEST_F(TestApiBlackSolver, mkParamSort)
 TEST_F(TestApiBlackSolver, mkPredicateSort)
 {
   ASSERT_NO_THROW(d_solver.mkPredicateSort({d_solver.getIntegerSort()}));
-  ASSERT_THROW(d_solver.mkPredicateSort({}), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkPredicateSort({}), CVC5ApiException);
   Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
                                          d_solver.getIntegerSort());
   // functions as arguments are allowed
@@ -256,7 +256,7 @@ TEST_F(TestApiBlackSolver, mkPredicateSort)
 
   Solver slv;
   ASSERT_THROW(slv.mkPredicateSort({d_solver.getIntegerSort()}),
-               CVC4ApiException);
+               CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkRecordSort)
@@ -272,7 +272,7 @@ TEST_F(TestApiBlackSolver, mkRecordSort)
   ASSERT_NO_THROW(recSort.getDatatype());
 
   Solver slv;
-  ASSERT_THROW(slv.mkRecordSort(fields), CVC4ApiException);
+  ASSERT_THROW(slv.mkRecordSort(fields), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkSetSort)
@@ -281,7 +281,7 @@ TEST_F(TestApiBlackSolver, mkSetSort)
   ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.getIntegerSort()));
   ASSERT_NO_THROW(d_solver.mkSetSort(d_solver.mkBitVectorSort(4)));
   Solver slv;
-  ASSERT_THROW(slv.mkSetSort(d_solver.mkBitVectorSort(4)), CVC4ApiException);
+  ASSERT_THROW(slv.mkSetSort(d_solver.mkBitVectorSort(4)), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkBagSort)
@@ -290,7 +290,7 @@ TEST_F(TestApiBlackSolver, mkBagSort)
   ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.getIntegerSort()));
   ASSERT_NO_THROW(d_solver.mkBagSort(d_solver.mkBitVectorSort(4)));
   Solver slv;
-  ASSERT_THROW(slv.mkBagSort(d_solver.mkBitVectorSort(4)), CVC4ApiException);
+  ASSERT_THROW(slv.mkBagSort(d_solver.mkBitVectorSort(4)), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkSequenceSort)
@@ -299,7 +299,7 @@ TEST_F(TestApiBlackSolver, mkSequenceSort)
   ASSERT_NO_THROW(d_solver.mkSequenceSort(
       d_solver.mkSequenceSort(d_solver.getIntegerSort())));
   Solver slv;
-  ASSERT_THROW(slv.mkSequenceSort(d_solver.getIntegerSort()), CVC4ApiException);
+  ASSERT_THROW(slv.mkSequenceSort(d_solver.getIntegerSort()), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkUninterpretedSort)
@@ -312,7 +312,7 @@ TEST_F(TestApiBlackSolver, mkSortConstructorSort)
 {
   ASSERT_NO_THROW(d_solver.mkSortConstructorSort("s", 2));
   ASSERT_NO_THROW(d_solver.mkSortConstructorSort("", 2));
-  ASSERT_THROW(d_solver.mkSortConstructorSort("", 0), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkSortConstructorSort("", 0), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkTupleSort)
@@ -321,10 +321,10 @@ TEST_F(TestApiBlackSolver, mkTupleSort)
   Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
                                          d_solver.getIntegerSort());
   ASSERT_THROW(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}),
-               CVC4ApiException);
+               CVC5ApiException);
 
   Solver slv;
-  ASSERT_THROW(slv.mkTupleSort({d_solver.getIntegerSort()}), CVC4ApiException);
+  ASSERT_THROW(slv.mkTupleSort({d_solver.getIntegerSort()}), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkBitVector)
@@ -339,13 +339,13 @@ TEST_F(TestApiBlackSolver, mkBitVector)
   ASSERT_NO_THROW(d_solver.mkBitVector("1010", 16));
   ASSERT_NO_THROW(d_solver.mkBitVector("a09f", 16));
   ASSERT_NO_THROW(d_solver.mkBitVector(8, "-127", 10));
-  ASSERT_THROW(d_solver.mkBitVector(size0, val1), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkBitVector(size0, val2), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkBitVector("", 2), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkBitVector("10", 3), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkBitVector("20", 2), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkBitVector(8, "101010101", 2), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkBitVector(8, "-256", 10), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkBitVector(size0, val1), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkBitVector(size0, val2), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkBitVector("", 2), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkBitVector("10", 3), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkBitVector("20", 2), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkBitVector(8, "101010101", 2), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkBitVector(8, "-256", 10), CVC5ApiException);
   ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("10", 10));
   ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("a", 16));
   ASSERT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101");
@@ -363,10 +363,10 @@ TEST_F(TestApiBlackSolver, mkVar)
   ASSERT_NO_THROW(d_solver.mkVar(funSort));
   ASSERT_NO_THROW(d_solver.mkVar(boolSort, std::string("b")));
   ASSERT_NO_THROW(d_solver.mkVar(funSort, ""));
-  ASSERT_THROW(d_solver.mkVar(Sort()), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkVar(Sort(), "a"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkVar(Sort()), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkVar(Sort(), "a"), CVC5ApiException);
   Solver slv;
-  ASSERT_THROW(slv.mkVar(boolSort, "x"), CVC4ApiException);
+  ASSERT_THROW(slv.mkVar(boolSort, "x"), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkBoolean)
@@ -384,27 +384,27 @@ TEST_F(TestApiBlackSolver, mkRoundingMode)
   else
   {
     ASSERT_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO),
-                 CVC4ApiException);
+                 CVC5ApiException);
   }
 }
 
 TEST_F(TestApiBlackSolver, mkUninterpretedConst)
 {
   ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
-  ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC5ApiException);
   Solver slv;
   ASSERT_THROW(slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1),
-               CVC4ApiException);
+               CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkAbstractValue)
 {
   ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1")));
-  ASSERT_THROW(d_solver.mkAbstractValue(std::string("0")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkAbstractValue(std::string("-1")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkAbstractValue(std::string("1.2")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkAbstractValue("1/2"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkAbstractValue("asdf"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkAbstractValue(std::string("0")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkAbstractValue(std::string("-1")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkAbstractValue(std::string("1.2")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkAbstractValue("1/2"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkAbstractValue("asdf"), CVC5ApiException);
 
   ASSERT_NO_THROW(d_solver.mkAbstractValue((uint32_t)1));
   ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)1));
@@ -412,7 +412,7 @@ TEST_F(TestApiBlackSolver, mkAbstractValue)
   ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)1));
   ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)-1));
   ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)-1));
-  ASSERT_THROW(d_solver.mkAbstractValue(0), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkAbstractValue(0), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkFloatingPoint)
@@ -426,18 +426,18 @@ TEST_F(TestApiBlackSolver, mkFloatingPoint)
   }
   else
   {
-    ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t1), CVC4ApiException);
+    ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t1), CVC5ApiException);
   }
-  ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, Term()), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, t1), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkFloatingPoint(3, 0, t1), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, Term()), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkFloatingPoint(0, 5, t1), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkFloatingPoint(3, 0, t1), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkFloatingPoint(3, 5, t2), CVC5ApiException);
 
   if (d_solver.supportsFloatingPoint())
   {
     Solver slv;
-    ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC4ApiException);
+    ASSERT_THROW(slv.mkFloatingPoint(3, 5, t1), CVC5ApiException);
   }
 }
 
@@ -448,8 +448,8 @@ TEST_F(TestApiBlackSolver, mkEmptySet)
   ASSERT_NO_THROW(d_solver.mkEmptySet(Sort()));
   ASSERT_NO_THROW(d_solver.mkEmptySet(s));
   ASSERT_THROW(d_solver.mkEmptySet(d_solver.getBooleanSort()),
-               CVC4ApiException);
-  ASSERT_THROW(slv.mkEmptySet(s), CVC4ApiException);
+               CVC5ApiException);
+  ASSERT_THROW(slv.mkEmptySet(s), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkEmptyBag)
@@ -459,8 +459,8 @@ TEST_F(TestApiBlackSolver, mkEmptyBag)
   ASSERT_NO_THROW(d_solver.mkEmptyBag(Sort()));
   ASSERT_NO_THROW(d_solver.mkEmptyBag(s));
   ASSERT_THROW(d_solver.mkEmptyBag(d_solver.getBooleanSort()),
-               CVC4ApiException);
-  ASSERT_THROW(slv.mkEmptyBag(s), CVC4ApiException);
+               CVC5ApiException);
+  ASSERT_THROW(slv.mkEmptyBag(s), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkEmptySequence)
@@ -469,7 +469,7 @@ TEST_F(TestApiBlackSolver, mkEmptySequence)
   Sort s = d_solver.mkSequenceSort(d_solver.getBooleanSort());
   ASSERT_NO_THROW(d_solver.mkEmptySequence(s));
   ASSERT_NO_THROW(d_solver.mkEmptySequence(d_solver.getBooleanSort()));
-  ASSERT_THROW(slv.mkEmptySequence(s), CVC4ApiException);
+  ASSERT_THROW(slv.mkEmptySequence(s), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkFalse)
@@ -486,7 +486,7 @@ TEST_F(TestApiBlackSolver, mkNaN)
   }
   else
   {
-    ASSERT_THROW(d_solver.mkNaN(3, 5), CVC4ApiException);
+    ASSERT_THROW(d_solver.mkNaN(3, 5), CVC5ApiException);
   }
 }
 
@@ -498,7 +498,7 @@ TEST_F(TestApiBlackSolver, mkNegZero)
   }
   else
   {
-    ASSERT_THROW(d_solver.mkNegZero(3, 5), CVC4ApiException);
+    ASSERT_THROW(d_solver.mkNegZero(3, 5), CVC5ApiException);
   }
 }
 
@@ -510,7 +510,7 @@ TEST_F(TestApiBlackSolver, mkNegInf)
   }
   else
   {
-    ASSERT_THROW(d_solver.mkNegInf(3, 5), CVC4ApiException);
+    ASSERT_THROW(d_solver.mkNegInf(3, 5), CVC5ApiException);
   }
 }
 
@@ -522,7 +522,7 @@ TEST_F(TestApiBlackSolver, mkPosInf)
   }
   else
   {
-    ASSERT_THROW(d_solver.mkPosInf(3, 5), CVC4ApiException);
+    ASSERT_THROW(d_solver.mkPosInf(3, 5), CVC5ApiException);
   }
 }
 
@@ -534,29 +534,29 @@ TEST_F(TestApiBlackSolver, mkPosZero)
   }
   else
   {
-    ASSERT_THROW(d_solver.mkPosZero(3, 5), CVC4ApiException);
+    ASSERT_THROW(d_solver.mkPosZero(3, 5), CVC5ApiException);
   }
 }
 
 TEST_F(TestApiBlackSolver, mkOp)
 {
   // mkOp(Kind kind, Kind k)
-  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, EQUAL), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, EQUAL), CVC5ApiException);
 
   // mkOp(Kind kind, const std::string& arg)
   ASSERT_NO_THROW(d_solver.mkOp(RECORD_UPDATE, "asdf"));
   ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, "2147483648"));
-  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, "asdf"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, "asdf"), CVC5ApiException);
 
   // mkOp(Kind kind, uint32_t arg)
   ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, 1));
   ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 1));
   ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 1));
-  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, 1), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, 1), CVC5ApiException);
 
   // mkOp(Kind kind, uint32_t arg1, uint32_t arg2)
   ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, 1, 1));
-  ASSERT_THROW(d_solver.mkOp(DIVISIBLE, 1, 2), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkOp(DIVISIBLE, 1, 2), CVC5ApiException);
 
   // mkOp(Kind kind, std::vector<uint32_t> args)
   std::vector<uint32_t> args = {1, 2, 2};
@@ -568,32 +568,32 @@ TEST_F(TestApiBlackSolver, mkPi) { ASSERT_NO_THROW(d_solver.mkPi()); }
 TEST_F(TestApiBlackSolver, mkInteger)
 {
   ASSERT_NO_THROW(d_solver.mkInteger("123"));
-  ASSERT_THROW(d_solver.mkInteger("1.23"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("1/23"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("12/3"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger(".2"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("2."), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger(""), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("asdf"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("1.2/3"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("."), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("/"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("2/"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("/2"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger("1.23"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("1/23"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("12/3"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger(".2"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("2."), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger(""), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("asdf"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("1.2/3"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("."), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("/"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("2/"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("/2"), CVC5ApiException);
 
   ASSERT_NO_THROW(d_solver.mkReal(std::string("123")));
-  ASSERT_THROW(d_solver.mkInteger(std::string("1.23")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger(std::string("1/23")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger(std::string("12/3")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger(std::string(".2")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger(std::string("2.")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger(std::string("")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger(std::string("asdf")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger(std::string("1.2/3")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger(std::string(".")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger(std::string("/")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger(std::string("2/")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger(std::string("/2")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("1.23")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("1/23")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("12/3")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string(".2")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("2.")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("asdf")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("1.2/3")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string(".")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("/")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("2/")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger(std::string("/2")), CVC5ApiException);
 
   int32_t val1 = 1;
   int64_t val2 = -1;
@@ -614,13 +614,13 @@ TEST_F(TestApiBlackSolver, mkReal)
   ASSERT_NO_THROW(d_solver.mkReal("12/3"));
   ASSERT_NO_THROW(d_solver.mkReal(".2"));
   ASSERT_NO_THROW(d_solver.mkReal("2."));
-  ASSERT_THROW(d_solver.mkReal(""), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkReal("asdf"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkReal("1.2/3"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkReal("."), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkReal("/"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkReal("2/"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkReal("/2"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkReal(""), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkReal("asdf"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkReal("1.2/3"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkReal("."), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkReal("/"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkReal("2/"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkReal("/2"), CVC5ApiException);
 
   ASSERT_NO_THROW(d_solver.mkReal(std::string("123")));
   ASSERT_NO_THROW(d_solver.mkReal(std::string("1.23")));
@@ -628,13 +628,13 @@ TEST_F(TestApiBlackSolver, mkReal)
   ASSERT_NO_THROW(d_solver.mkReal(std::string("12/3")));
   ASSERT_NO_THROW(d_solver.mkReal(std::string(".2")));
   ASSERT_NO_THROW(d_solver.mkReal(std::string("2.")));
-  ASSERT_THROW(d_solver.mkReal(std::string("")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkReal(std::string("asdf")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkReal(std::string("1.2/3")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkReal(std::string(".")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkReal(std::string("/")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkReal(std::string("2/")), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkReal(std::string("/2")), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkReal(std::string("")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkReal(std::string("asdf")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkReal(std::string("1.2/3")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkReal(std::string(".")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkReal(std::string("/")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkReal(std::string("2/")), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkReal(std::string("/2")), CVC5ApiException);
 
   int32_t val1 = 1;
   int64_t val2 = -1;
@@ -670,9 +670,9 @@ TEST_F(TestApiBlackSolver, mkRegexpSigma)
 TEST_F(TestApiBlackSolver, mkSepNil)
 {
   ASSERT_NO_THROW(d_solver.mkSepNil(d_solver.getBooleanSort()));
-  ASSERT_THROW(d_solver.mkSepNil(Sort()), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkSepNil(Sort()), CVC5ApiException);
   Solver slv;
-  ASSERT_THROW(slv.mkSepNil(d_solver.getIntegerSort()), CVC4ApiException);
+  ASSERT_THROW(slv.mkSepNil(d_solver.getIntegerSort()), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkString)
@@ -689,9 +689,9 @@ TEST_F(TestApiBlackSolver, mkChar)
 {
   ASSERT_NO_THROW(d_solver.mkChar(std::string("0123")));
   ASSERT_NO_THROW(d_solver.mkChar("aA"));
-  ASSERT_THROW(d_solver.mkChar(""), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkChar("0g0"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkChar("100000"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkChar(""), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkChar("0g0"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkChar("100000"), CVC5ApiException);
   ASSERT_EQ(d_solver.mkChar("abc"), d_solver.mkChar("ABC"));
 }
 
@@ -712,44 +712,44 @@ TEST_F(TestApiBlackSolver, mkTerm)
   ASSERT_NO_THROW(d_solver.mkTerm(PI));
   ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_EMPTY));
   ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_SIGMA));
-  ASSERT_THROW(d_solver.mkTerm(CONST_BITVECTOR), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(CONST_BITVECTOR), CVC5ApiException);
 
   // mkTerm(Kind kind, Term child) const
   ASSERT_NO_THROW(d_solver.mkTerm(NOT, d_solver.mkTrue()));
-  ASSERT_THROW(d_solver.mkTerm(NOT, Term()), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkTerm(NOT, a), CVC4ApiException);
-  ASSERT_THROW(slv.mkTerm(NOT, d_solver.mkTrue()), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(NOT, Term()), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(NOT, a), CVC5ApiException);
+  ASSERT_THROW(slv.mkTerm(NOT, d_solver.mkTrue()), CVC5ApiException);
 
   // mkTerm(Kind kind, Term child1, Term child2) const
   ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, a, b));
-  ASSERT_THROW(d_solver.mkTerm(EQUAL, Term(), b), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkTerm(EQUAL, a, Term()), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkTerm(EQUAL, a, d_solver.mkTrue()), CVC4ApiException);
-  ASSERT_THROW(slv.mkTerm(EQUAL, a, b), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(EQUAL, Term(), b), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(EQUAL, a, Term()), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(EQUAL, a, d_solver.mkTrue()), CVC5ApiException);
+  ASSERT_THROW(slv.mkTerm(EQUAL, a, b), CVC5ApiException);
 
   // mkTerm(Kind kind, Term child1, Term child2, Term child3) const
   ASSERT_NO_THROW(d_solver.mkTerm(
       ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()));
   ASSERT_THROW(
       d_solver.mkTerm(ITE, Term(), d_solver.mkTrue(), d_solver.mkTrue()),
-      CVC4ApiException);
+      CVC5ApiException);
   ASSERT_THROW(
       d_solver.mkTerm(ITE, d_solver.mkTrue(), Term(), d_solver.mkTrue()),
-      CVC4ApiException);
+      CVC5ApiException);
   ASSERT_THROW(
       d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), Term()),
-      CVC4ApiException);
+      CVC5ApiException);
   ASSERT_THROW(d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), b),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(
       slv.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()),
-      CVC4ApiException);
+      CVC5ApiException);
 
   // mkTerm(Kind kind, const std::vector<Term>& children) const
   ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, v1));
-  ASSERT_THROW(d_solver.mkTerm(EQUAL, v2), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkTerm(EQUAL, v3), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkTerm(DISTINCT, v6), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(EQUAL, v2), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(EQUAL, v3), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(DISTINCT, v6), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkTermFromOp)
@@ -795,25 +795,25 @@ TEST_F(TestApiBlackSolver, mkTermFromOp)
   // mkTerm(Op op, Term term) const
   ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1));
   ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm2));
-  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, nilTerm1), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, consTerm1), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm2), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkTerm(opterm1), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, headTerm1), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkTerm(opterm1), CVC4ApiException);
-  ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, nilTerm1), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, consTerm1), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm2), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm1), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, headTerm1), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm1), CVC5ApiException);
+  ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1), CVC5ApiException);
 
   // mkTerm(Op op, Term child) const
   ASSERT_NO_THROW(d_solver.mkTerm(opterm1, a));
   ASSERT_NO_THROW(d_solver.mkTerm(opterm2, d_solver.mkInteger(1)));
   ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, headTerm1, c));
   ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, tailTerm2, c));
-  ASSERT_THROW(d_solver.mkTerm(opterm2, a), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkTerm(opterm1, Term()), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm2, a), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm1, Term()), CVC5ApiException);
   ASSERT_THROW(
       d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver.mkInteger(0)),
-      CVC4ApiException);
-  ASSERT_THROW(slv.mkTerm(opterm1, a), CVC4ApiException);
+      CVC5ApiException);
+  ASSERT_THROW(slv.mkTerm(opterm1, a), CVC5ApiException);
 
   // mkTerm(Op op, Term child1, Term child2) const
   ASSERT_NO_THROW(
@@ -823,31 +823,31 @@ TEST_F(TestApiBlackSolver, mkTermFromOp)
                       d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
   ASSERT_THROW(
       d_solver.mkTerm(opterm2, d_solver.mkInteger(1), d_solver.mkInteger(2)),
-      CVC4ApiException);
-  ASSERT_THROW(d_solver.mkTerm(opterm1, a, b), CVC4ApiException);
+      CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm1, a, b), CVC5ApiException);
   ASSERT_THROW(d_solver.mkTerm(opterm2, d_solver.mkInteger(1), Term()),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.mkTerm(opterm2, Term(), d_solver.mkInteger(1)),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR,
                           consTerm1,
                           d_solver.mkInteger(0),
                           d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)),
-               CVC4ApiException);
+               CVC5ApiException);
 
   // mkTerm(Op op, Term child1, Term child2, Term child3) const
-  ASSERT_THROW(d_solver.mkTerm(opterm1, a, b, a), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm1, a, b, a), CVC5ApiException);
   ASSERT_THROW(
       d_solver.mkTerm(
           opterm2, d_solver.mkInteger(1), d_solver.mkInteger(1), Term()),
-      CVC4ApiException);
+      CVC5ApiException);
 
   // mkTerm(Op op, const std::vector<Term>& children) const
   ASSERT_NO_THROW(d_solver.mkTerm(opterm2, v4));
-  ASSERT_THROW(d_solver.mkTerm(opterm2, v1), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkTerm(opterm2, v2), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkTerm(opterm2, v3), CVC4ApiException);
-  ASSERT_THROW(slv.mkTerm(opterm2, v4), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm2, v1), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm2, v2), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkTerm(opterm2, v3), CVC5ApiException);
+  ASSERT_THROW(slv.mkTerm(opterm2, v4), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkTrue)
@@ -864,28 +864,28 @@ TEST_F(TestApiBlackSolver, mkTuple)
       d_solver.mkTuple({d_solver.getRealSort()}, {d_solver.mkInteger("5")}));
 
   ASSERT_THROW(d_solver.mkTuple({}, {d_solver.mkBitVector("101", 2)}),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.mkTuple({d_solver.mkBitVectorSort(4)},
                                 {d_solver.mkBitVector("101", 2)}),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(
       d_solver.mkTuple({d_solver.getIntegerSort()}, {d_solver.mkReal("5.3")}),
-      CVC4ApiException);
+      CVC5ApiException);
   Solver slv;
   ASSERT_THROW(
       slv.mkTuple({d_solver.mkBitVectorSort(3)}, {slv.mkBitVector("101", 2)}),
-      CVC4ApiException);
+      CVC5ApiException);
   ASSERT_THROW(
       slv.mkTuple({slv.mkBitVectorSort(3)}, {d_solver.mkBitVector("101", 2)}),
-      CVC4ApiException);
+      CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkUniverseSet)
 {
   ASSERT_NO_THROW(d_solver.mkUniverseSet(d_solver.getBooleanSort()));
-  ASSERT_THROW(d_solver.mkUniverseSet(Sort()), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkUniverseSet(Sort()), CVC5ApiException);
   Solver slv;
-  ASSERT_THROW(slv.mkUniverseSet(d_solver.getBooleanSort()), CVC4ApiException);
+  ASSERT_THROW(slv.mkUniverseSet(d_solver.getBooleanSort()), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkConst)
@@ -899,11 +899,11 @@ TEST_F(TestApiBlackSolver, mkConst)
   ASSERT_NO_THROW(d_solver.mkConst(intSort, std::string("i")));
   ASSERT_NO_THROW(d_solver.mkConst(funSort, "f"));
   ASSERT_NO_THROW(d_solver.mkConst(funSort, ""));
-  ASSERT_THROW(d_solver.mkConst(Sort()), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkConst(Sort(), "a"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkConst(Sort()), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkConst(Sort(), "a"), CVC5ApiException);
 
   Solver slv;
-  ASSERT_THROW(slv.mkConst(boolSort), CVC4ApiException);
+  ASSERT_THROW(slv.mkConst(boolSort), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkConstArray)
@@ -914,16 +914,16 @@ TEST_F(TestApiBlackSolver, mkConstArray)
   Term constArr = d_solver.mkConstArray(arrSort, zero);
 
   ASSERT_NO_THROW(d_solver.mkConstArray(arrSort, zero));
-  ASSERT_THROW(d_solver.mkConstArray(Sort(), zero), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkConstArray(arrSort, Term()), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkConstArray(Sort(), zero), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkConstArray(arrSort, Term()), CVC5ApiException);
   ASSERT_THROW(d_solver.mkConstArray(arrSort, d_solver.mkBitVector(1, 1)),
-               CVC4ApiException);
-  ASSERT_THROW(d_solver.mkConstArray(intSort, zero), CVC4ApiException);
+               CVC5ApiException);
+  ASSERT_THROW(d_solver.mkConstArray(intSort, zero), CVC5ApiException);
   Solver slv;
   Term zero2 = slv.mkInteger(0);
   Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
-  ASSERT_THROW(slv.mkConstArray(arrSort2, zero), CVC4ApiException);
-  ASSERT_THROW(slv.mkConstArray(arrSort, zero2), CVC4ApiException);
+  ASSERT_THROW(slv.mkConstArray(arrSort2, zero), CVC5ApiException);
+  ASSERT_THROW(slv.mkConstArray(arrSort, zero2), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, declareDatatype)
@@ -941,11 +941,11 @@ TEST_F(TestApiBlackSolver, declareDatatype)
   ASSERT_NO_THROW(d_solver.declareDatatype(std::string(""), ctors3));
   std::vector<DatatypeConstructorDecl> ctors4;
   ASSERT_THROW(d_solver.declareDatatype(std::string("c"), ctors4),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.declareDatatype(std::string(""), ctors4),
-               CVC4ApiException);
+               CVC5ApiException);
   Solver slv;
-  ASSERT_THROW(slv.declareDatatype(std::string("a"), ctors1), CVC4ApiException);
+  ASSERT_THROW(slv.declareDatatype(std::string("a"), ctors1), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, declareFun)
@@ -956,13 +956,13 @@ TEST_F(TestApiBlackSolver, declareFun)
   ASSERT_NO_THROW(d_solver.declareFun("f1", {}, bvSort));
   ASSERT_NO_THROW(
       d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort));
-  ASSERT_THROW(d_solver.declareFun("f2", {}, funSort), CVC4ApiException);
+  ASSERT_THROW(d_solver.declareFun("f2", {}, funSort), CVC5ApiException);
   // functions as arguments is allowed
   ASSERT_NO_THROW(d_solver.declareFun("f4", {bvSort, funSort}, bvSort));
   ASSERT_THROW(d_solver.declareFun("f5", {bvSort, bvSort}, funSort),
-               CVC4ApiException);
+               CVC5ApiException);
   Solver slv;
-  ASSERT_THROW(slv.declareFun("f1", {}, bvSort), CVC4ApiException);
+  ASSERT_THROW(slv.declareFun("f1", {}, bvSort), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, declareSort)
@@ -1006,30 +1006,30 @@ TEST_F(TestApiBlackSolver, defineFun)
   ASSERT_NO_THROW(d_solver.defineFun("ff", {b1, b2}, bvSort, v1));
   ASSERT_NO_THROW(d_solver.defineFun(f1, {b1, b11}, v1));
   ASSERT_THROW(d_solver.defineFun("ff", {v1, b2}, bvSort, v1),
-               CVC4ApiException);
-  ASSERT_THROW(d_solver.defineFun("fff", {b1}, bvSort, v3), CVC4ApiException);
+               CVC5ApiException);
+  ASSERT_THROW(d_solver.defineFun("fff", {b1}, bvSort, v3), CVC5ApiException);
   ASSERT_THROW(d_solver.defineFun("ffff", {b1}, funSort2, v3),
-               CVC4ApiException);
+               CVC5ApiException);
   // b3 has function sort, which is allowed as an argument
   ASSERT_NO_THROW(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1));
-  ASSERT_THROW(d_solver.defineFun(f1, {v1, b11}, v1), CVC4ApiException);
-  ASSERT_THROW(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException);
-  ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException);
-  ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v3), CVC4ApiException);
-  ASSERT_THROW(d_solver.defineFun(f2, {b1}, v2), CVC4ApiException);
-  ASSERT_THROW(d_solver.defineFun(f3, {b1}, v1), CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFun(f1, {v1, b11}, v1), CVC5ApiException);
+  ASSERT_THROW(d_solver.defineFun(f1, {b1}, v1), CVC5ApiException);
+  ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v2), CVC5ApiException);
+  ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v3), CVC5ApiException);
+  ASSERT_THROW(d_solver.defineFun(f2, {b1}, v2), CVC5ApiException);
+  ASSERT_THROW(d_solver.defineFun(f3, {b1}, v1), CVC5ApiException);
 
   Solver slv;
   Sort bvSort2 = slv.mkBitVectorSort(32);
   Term v12 = slv.mkConst(bvSort2, "v1");
   Term b12 = slv.mkVar(bvSort2, "b1");
   Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
-  ASSERT_THROW(slv.defineFun("f", {}, bvSort, v12), CVC4ApiException);
-  ASSERT_THROW(slv.defineFun("f", {}, bvSort2, v1), CVC4ApiException);
-  ASSERT_THROW(slv.defineFun("ff", {b1, b22}, bvSort2, v12), CVC4ApiException);
-  ASSERT_THROW(slv.defineFun("ff", {b12, b2}, bvSort2, v12), CVC4ApiException);
-  ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort, v12), CVC4ApiException);
-  ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort2, v1), CVC4ApiException);
+  ASSERT_THROW(slv.defineFun("f", {}, bvSort, v12), CVC5ApiException);
+  ASSERT_THROW(slv.defineFun("f", {}, bvSort2, v1), CVC5ApiException);
+  ASSERT_THROW(slv.defineFun("ff", {b1, b22}, bvSort2, v12), CVC5ApiException);
+  ASSERT_THROW(slv.defineFun("ff", {b12, b2}, bvSort2, v12), CVC5ApiException);
+  ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort, v12), CVC5ApiException);
+  ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort2, v1), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, defineFunGlobal)
@@ -1076,18 +1076,18 @@ TEST_F(TestApiBlackSolver, defineFunRec)
   ASSERT_NO_THROW(d_solver.defineFunRec("ff", {b1, b2}, bvSort, v1));
   ASSERT_NO_THROW(d_solver.defineFunRec(f1, {b1, b11}, v1));
   ASSERT_THROW(d_solver.defineFunRec("fff", {b1}, bvSort, v3),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.defineFunRec("ff", {b1, v2}, bvSort, v1),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.defineFunRec("ffff", {b1}, funSort2, v3),
-               CVC4ApiException);
+               CVC5ApiException);
   // b3 has function sort, which is allowed as an argument
   ASSERT_NO_THROW(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1));
-  ASSERT_THROW(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException);
-  ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException);
-  ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException);
-  ASSERT_THROW(d_solver.defineFunRec(f2, {b1}, v2), CVC4ApiException);
-  ASSERT_THROW(d_solver.defineFunRec(f3, {b1}, v1), CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunRec(f1, {b1}, v1), CVC5ApiException);
+  ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC5ApiException);
+  ASSERT_THROW(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC5ApiException);
+  ASSERT_THROW(d_solver.defineFunRec(f2, {b1}, v2), CVC5ApiException);
+  ASSERT_THROW(d_solver.defineFunRec(f3, {b1}, v1), CVC5ApiException);
 
   Solver slv;
   Sort bvSort2 = slv.mkBitVectorSort(32);
@@ -1096,16 +1096,16 @@ TEST_F(TestApiBlackSolver, defineFunRec)
   Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
   ASSERT_NO_THROW(slv.defineFunRec("f", {}, bvSort2, v12));
   ASSERT_NO_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort2, v12));
-  ASSERT_THROW(slv.defineFunRec("f", {}, bvSort, v12), CVC4ApiException);
-  ASSERT_THROW(slv.defineFunRec("f", {}, bvSort2, v1), CVC4ApiException);
+  ASSERT_THROW(slv.defineFunRec("f", {}, bvSort, v12), CVC5ApiException);
+  ASSERT_THROW(slv.defineFunRec("f", {}, bvSort2, v1), CVC5ApiException);
   ASSERT_THROW(slv.defineFunRec("ff", {b1, b22}, bvSort2, v12),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.defineFunRec("ff", {b12, b2}, bvSort2, v12),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort, v12),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort2, v1),
-               CVC4ApiException);
+               CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, defineFunRecWrongLogic)
@@ -1116,8 +1116,8 @@ TEST_F(TestApiBlackSolver, defineFunRecWrongLogic)
   Term b = d_solver.mkVar(bvSort, "b");
   Term v = d_solver.mkConst(bvSort, "v");
   Term f = d_solver.mkConst(funSort, "f");
-  ASSERT_THROW(d_solver.defineFunRec("f", {}, bvSort, v), CVC4ApiException);
-  ASSERT_THROW(d_solver.defineFunRec(f, {b, b}, v), CVC4ApiException);
+  ASSERT_THROW(d_solver.defineFunRec("f", {}, bvSort, v), CVC5ApiException);
+  ASSERT_THROW(d_solver.defineFunRec(f, {b, b}, v), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, defineFunRecGlobal)
@@ -1166,15 +1166,15 @@ TEST_F(TestApiBlackSolver, defineFunsRec)
   ASSERT_NO_THROW(
       d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
   ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{v1, b11}, {b4}}, {v1, v2}),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
-               CVC4ApiException);
+               CVC5ApiException);
 
   Solver slv;
   Sort uSort2 = slv.mkUninterpretedSort("u");
@@ -1191,19 +1191,19 @@ TEST_F(TestApiBlackSolver, defineFunsRec)
   ASSERT_NO_THROW(
       slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v22}));
   ASSERT_THROW(slv.defineFunsRec({f1, f22}, {{b12, b112}, {b42}}, {v12, v22}),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.defineFunsRec({f12, f2}, {{b12, b112}, {b42}}, {v12, v22}),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b1, b112}, {b42}}, {v12, v22}),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b11}, {b42}}, {v12, v22}),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b4}}, {v12, v22}),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v1, v22}),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v2}),
-               CVC4ApiException);
+               CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, defineFunsRecWrongLogic)
@@ -1220,7 +1220,7 @@ TEST_F(TestApiBlackSolver, defineFunsRecWrongLogic)
   Term f1 = d_solver.mkConst(funSort1, "f1");
   Term f2 = d_solver.mkConst(funSort2, "f2");
   ASSERT_THROW(d_solver.defineFunsRec({f1, f2}, {{b, b}, {u}}, {v1, v2}),
-               CVC4ApiException);
+               CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, defineFunsRecGlobal)
@@ -1267,7 +1267,7 @@ TEST_F(TestApiBlackSolver, uFIteration)
 TEST_F(TestApiBlackSolver, getInfo)
 {
   ASSERT_NO_THROW(d_solver.getInfo("name"));
-  ASSERT_THROW(d_solver.getInfo("asdf"), CVC4ApiException);
+  ASSERT_THROW(d_solver.getInfo("asdf"), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getInterpolant)
@@ -1307,7 +1307,7 @@ TEST_F(TestApiBlackSolver, getOp)
   Term exta = d_solver.mkTerm(ext, a);
 
   ASSERT_FALSE(a.hasOp());
-  ASSERT_THROW(a.getOp(), CVC4ApiException);
+  ASSERT_THROW(a.getOp(), CVC5ApiException);
   ASSERT_TRUE(exta.hasOp());
   ASSERT_EQ(exta.getOp(), ext);
 
@@ -1339,14 +1339,14 @@ TEST_F(TestApiBlackSolver, getOp)
 TEST_F(TestApiBlackSolver, getOption)
 {
   ASSERT_NO_THROW(d_solver.getOption("incremental"));
-  ASSERT_THROW(d_solver.getOption("asdf"), CVC4ApiException);
+  ASSERT_THROW(d_solver.getOption("asdf"), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getUnsatAssumptions1)
 {
   d_solver.setOption("incremental", "false");
   d_solver.checkSatAssuming(d_solver.mkFalse());
-  ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
+  ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getUnsatAssumptions2)
@@ -1354,7 +1354,7 @@ TEST_F(TestApiBlackSolver, getUnsatAssumptions2)
   d_solver.setOption("incremental", "true");
   d_solver.setOption("produce-unsat-assumptions", "false");
   d_solver.checkSatAssuming(d_solver.mkFalse());
-  ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
+  ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getUnsatAssumptions3)
@@ -1364,7 +1364,7 @@ TEST_F(TestApiBlackSolver, getUnsatAssumptions3)
   d_solver.checkSatAssuming(d_solver.mkFalse());
   ASSERT_NO_THROW(d_solver.getUnsatAssumptions());
   d_solver.checkSatAssuming(d_solver.mkTrue());
-  ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC4ApiException);
+  ASSERT_THROW(d_solver.getUnsatAssumptions(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getUnsatCore1)
@@ -1372,7 +1372,7 @@ TEST_F(TestApiBlackSolver, getUnsatCore1)
   d_solver.setOption("incremental", "false");
   d_solver.assertFormula(d_solver.mkFalse());
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.getUnsatCore(), CVC4ApiException);
+  ASSERT_THROW(d_solver.getUnsatCore(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getUnsatCore2)
@@ -1381,7 +1381,7 @@ TEST_F(TestApiBlackSolver, getUnsatCore2)
   d_solver.setOption("produce-unsat-cores", "false");
   d_solver.assertFormula(d_solver.mkFalse());
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.getUnsatCore(), CVC4ApiException);
+  ASSERT_THROW(d_solver.getUnsatCore(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getUnsatCore3)
@@ -1431,7 +1431,7 @@ TEST_F(TestApiBlackSolver, getValue1)
   Term t = d_solver.mkTrue();
   d_solver.assertFormula(t);
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.getValue(t), CVC4ApiException);
+  ASSERT_THROW(d_solver.getValue(t), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getValue2)
@@ -1440,7 +1440,7 @@ TEST_F(TestApiBlackSolver, getValue2)
   Term t = d_solver.mkFalse();
   d_solver.assertFormula(t);
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.getValue(t), CVC4ApiException);
+  ASSERT_THROW(d_solver.getValue(t), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getValue3)
@@ -1479,7 +1479,7 @@ TEST_F(TestApiBlackSolver, getValue3)
   ASSERT_NO_THROW(d_solver.getValue(p_f_y));
 
   Solver slv;
-  ASSERT_THROW(slv.getValue(x), CVC4ApiException);
+  ASSERT_THROW(slv.getValue(x), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getQuantifierElimination)
@@ -1489,9 +1489,9 @@ TEST_F(TestApiBlackSolver, getQuantifierElimination)
       d_solver.mkTerm(FORALL,
                       d_solver.mkTerm(BOUND_VAR_LIST, x),
                       d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
-  ASSERT_THROW(d_solver.getQuantifierElimination(Term()), CVC4ApiException);
+  ASSERT_THROW(d_solver.getQuantifierElimination(Term()), CVC5ApiException);
   ASSERT_THROW(d_solver.getQuantifierElimination(Solver().mkBoolean(false)),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_NO_THROW(d_solver.getQuantifierElimination(forall));
 }
 
@@ -1503,10 +1503,10 @@ TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct)
                       d_solver.mkTerm(BOUND_VAR_LIST, x),
                       d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
   ASSERT_THROW(d_solver.getQuantifierEliminationDisjunct(Term()),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(
       d_solver.getQuantifierEliminationDisjunct(Solver().mkBoolean(false)),
-      CVC4ApiException);
+      CVC5ApiException);
   ASSERT_NO_THROW(d_solver.getQuantifierEliminationDisjunct(forall));
 }
 
@@ -1517,7 +1517,7 @@ TEST_F(TestApiBlackSolver, declareSeparationHeap)
   ASSERT_NO_THROW(d_solver.declareSeparationHeap(integer, integer));
   // cannot declare separation logic heap more than once
   ASSERT_THROW(d_solver.declareSeparationHeap(integer, integer),
-               CVC4ApiException);
+               CVC5ApiException);
 }
 
 namespace {
@@ -1547,7 +1547,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm1)
   d_solver.setOption("produce-models", "true");
   Term t = d_solver.mkTrue();
   d_solver.assertFormula(t);
-  ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSeparationHeap(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getSeparationHeapTerm2)
@@ -1556,7 +1556,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm2)
   d_solver.setOption("incremental", "false");
   d_solver.setOption("produce-models", "false");
   checkSimpleSeparationConstraints(&d_solver);
-  ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSeparationHeap(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getSeparationHeapTerm3)
@@ -1567,7 +1567,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm3)
   Term t = d_solver.mkFalse();
   d_solver.assertFormula(t);
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSeparationHeap(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getSeparationHeapTerm4)
@@ -1578,7 +1578,7 @@ TEST_F(TestApiBlackSolver, getSeparationHeapTerm4)
   Term t = d_solver.mkTrue();
   d_solver.assertFormula(t);
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.getSeparationHeap(), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSeparationHeap(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getSeparationHeapTerm5)
@@ -1597,7 +1597,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm1)
   d_solver.setOption("produce-models", "true");
   Term t = d_solver.mkTrue();
   d_solver.assertFormula(t);
-  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getSeparationNilTerm2)
@@ -1606,7 +1606,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm2)
   d_solver.setOption("incremental", "false");
   d_solver.setOption("produce-models", "false");
   checkSimpleSeparationConstraints(&d_solver);
-  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getSeparationNilTerm3)
@@ -1617,7 +1617,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm3)
   Term t = d_solver.mkFalse();
   d_solver.assertFormula(t);
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getSeparationNilTerm4)
@@ -1628,7 +1628,7 @@ TEST_F(TestApiBlackSolver, getSeparationNilTerm4)
   Term t = d_solver.mkTrue();
   d_solver.assertFormula(t);
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSeparationNilTerm(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getSeparationNilTerm5)
@@ -1644,26 +1644,26 @@ TEST_F(TestApiBlackSolver, push1)
 {
   d_solver.setOption("incremental", "true");
   ASSERT_NO_THROW(d_solver.push(1));
-  ASSERT_THROW(d_solver.setOption("incremental", "false"), CVC4ApiException);
-  ASSERT_THROW(d_solver.setOption("incremental", "true"), CVC4ApiException);
+  ASSERT_THROW(d_solver.setOption("incremental", "false"), CVC5ApiException);
+  ASSERT_THROW(d_solver.setOption("incremental", "true"), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, push2)
 {
   d_solver.setOption("incremental", "false");
-  ASSERT_THROW(d_solver.push(1), CVC4ApiException);
+  ASSERT_THROW(d_solver.push(1), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, pop1)
 {
   d_solver.setOption("incremental", "false");
-  ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
+  ASSERT_THROW(d_solver.pop(1), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, pop2)
 {
   d_solver.setOption("incremental", "true");
-  ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
+  ASSERT_THROW(d_solver.pop(1), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, pop3)
@@ -1671,7 +1671,7 @@ TEST_F(TestApiBlackSolver, pop3)
   d_solver.setOption("incremental", "true");
   ASSERT_NO_THROW(d_solver.push(1));
   ASSERT_NO_THROW(d_solver.pop(1));
-  ASSERT_THROW(d_solver.pop(1), CVC4ApiException);
+  ASSERT_THROW(d_solver.pop(1), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, blockModel1)
@@ -1680,7 +1680,7 @@ TEST_F(TestApiBlackSolver, blockModel1)
   Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
   d_solver.assertFormula(x.eqTerm(x));
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
+  ASSERT_THROW(d_solver.blockModel(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, blockModel2)
@@ -1689,7 +1689,7 @@ TEST_F(TestApiBlackSolver, blockModel2)
   Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
   d_solver.assertFormula(x.eqTerm(x));
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
+  ASSERT_THROW(d_solver.blockModel(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, blockModel3)
@@ -1698,7 +1698,7 @@ TEST_F(TestApiBlackSolver, blockModel3)
   d_solver.setOption("block-models", "literals");
   Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
   d_solver.assertFormula(x.eqTerm(x));
-  ASSERT_THROW(d_solver.blockModel(), CVC4ApiException);
+  ASSERT_THROW(d_solver.blockModel(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, blockModel4)
@@ -1718,10 +1718,10 @@ TEST_F(TestApiBlackSolver, blockModelValues1)
   Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
   d_solver.assertFormula(x.eqTerm(x));
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.blockModelValues({}), CVC4ApiException);
-  ASSERT_THROW(d_solver.blockModelValues({Term()}), CVC4ApiException);
+  ASSERT_THROW(d_solver.blockModelValues({}), CVC5ApiException);
+  ASSERT_THROW(d_solver.blockModelValues({Term()}), CVC5ApiException);
   ASSERT_THROW(d_solver.blockModelValues({Solver().mkBoolean(false)}),
-               CVC4ApiException);
+               CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, blockModelValues2)
@@ -1730,7 +1730,7 @@ TEST_F(TestApiBlackSolver, blockModelValues2)
   Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
   d_solver.assertFormula(x.eqTerm(x));
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
+  ASSERT_THROW(d_solver.blockModelValues({x}), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, blockModelValues3)
@@ -1739,7 +1739,7 @@ TEST_F(TestApiBlackSolver, blockModelValues3)
   Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
   d_solver.assertFormula(x.eqTerm(x));
   d_solver.checkSat();
-  ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
+  ASSERT_THROW(d_solver.blockModelValues({x}), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, blockModelValues4)
@@ -1748,7 +1748,7 @@ TEST_F(TestApiBlackSolver, blockModelValues4)
   d_solver.setOption("block-models", "literals");
   Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
   d_solver.assertFormula(x.eqTerm(x));
-  ASSERT_THROW(d_solver.blockModelValues({x}), CVC4ApiException);
+  ASSERT_THROW(d_solver.blockModelValues({x}), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, blockModelValues5)
@@ -1763,9 +1763,9 @@ TEST_F(TestApiBlackSolver, blockModelValues5)
 
 TEST_F(TestApiBlackSolver, setInfo)
 {
-  ASSERT_THROW(d_solver.setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException);
-  ASSERT_THROW(d_solver.setInfo("cvc2-logic", "QF_BV"), CVC4ApiException);
-  ASSERT_THROW(d_solver.setInfo("cvc4-logic", "asdf"), CVC4ApiException);
+  ASSERT_THROW(d_solver.setInfo("cvc4-lagic", "QF_BV"), CVC5ApiException);
+  ASSERT_THROW(d_solver.setInfo("cvc2-logic", "QF_BV"), CVC5ApiException);
+  ASSERT_THROW(d_solver.setInfo("cvc4-logic", "asdf"), CVC5ApiException);
 
   ASSERT_NO_THROW(d_solver.setInfo("source", "asdf"));
   ASSERT_NO_THROW(d_solver.setInfo("category", "asdf"));
@@ -1779,17 +1779,17 @@ TEST_F(TestApiBlackSolver, setInfo)
   ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.0"));
   ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.5"));
   ASSERT_NO_THROW(d_solver.setInfo("smt-lib-version", "2.6"));
-  ASSERT_THROW(d_solver.setInfo("smt-lib-version", ".0"), CVC4ApiException);
+  ASSERT_THROW(d_solver.setInfo("smt-lib-version", ".0"), CVC5ApiException);
 
   ASSERT_NO_THROW(d_solver.setInfo("status", "sat"));
   ASSERT_NO_THROW(d_solver.setInfo("status", "unsat"));
   ASSERT_NO_THROW(d_solver.setInfo("status", "unknown"));
-  ASSERT_THROW(d_solver.setInfo("status", "asdf"), CVC4ApiException);
+  ASSERT_THROW(d_solver.setInfo("status", "asdf"), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, simplify)
 {
-  ASSERT_THROW(d_solver.simplify(Term()), CVC4ApiException);
+  ASSERT_THROW(d_solver.simplify(Term()), CVC5ApiException);
 
   Sort bvSort = d_solver.mkBitVectorSort(32);
   Sort uSort = d_solver.mkUninterpretedSort("u");
@@ -1819,7 +1819,7 @@ TEST_F(TestApiBlackSolver, simplify)
   ASSERT_NE(d_solver.mkTrue(), x_eq_b);
   ASSERT_NE(d_solver.mkTrue(), d_solver.simplify(x_eq_b));
   Solver slv;
-  ASSERT_THROW(slv.simplify(x), CVC4ApiException);
+  ASSERT_THROW(slv.simplify(x), CVC5ApiException);
 
   Term i1 = d_solver.mkConst(d_solver.getIntegerSort(), "i1");
   ASSERT_NO_THROW(d_solver.simplify(i1));
@@ -1865,18 +1865,18 @@ TEST_F(TestApiBlackSolver, simplify)
 TEST_F(TestApiBlackSolver, assertFormula)
 {
   ASSERT_NO_THROW(d_solver.assertFormula(d_solver.mkTrue()));
-  ASSERT_THROW(d_solver.assertFormula(Term()), CVC4ApiException);
+  ASSERT_THROW(d_solver.assertFormula(Term()), CVC5ApiException);
   Solver slv;
-  ASSERT_THROW(slv.assertFormula(d_solver.mkTrue()), CVC4ApiException);
+  ASSERT_THROW(slv.assertFormula(d_solver.mkTrue()), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, checkEntailed)
 {
   d_solver.setOption("incremental", "false");
   ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue()));
-  ASSERT_THROW(d_solver.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
+  ASSERT_THROW(d_solver.checkEntailed(d_solver.mkTrue()), CVC5ApiException);
   Solver slv;
-  ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
+  ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, checkEntailed1)
@@ -1887,11 +1887,11 @@ TEST_F(TestApiBlackSolver, checkEntailed1)
   Term z = d_solver.mkTerm(AND, x, y);
   d_solver.setOption("incremental", "true");
   ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue()));
-  ASSERT_THROW(d_solver.checkEntailed(Term()), CVC4ApiException);
+  ASSERT_THROW(d_solver.checkEntailed(Term()), CVC5ApiException);
   ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTrue()));
   ASSERT_NO_THROW(d_solver.checkEntailed(z));
   Solver slv;
-  ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
+  ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, checkEntailed2)
@@ -1936,27 +1936,27 @@ TEST_F(TestApiBlackSolver, checkEntailed2)
   ASSERT_NO_THROW(d_solver.checkEntailed(d_solver.mkTerm(DISTINCT, x, y)));
   ASSERT_NO_THROW(d_solver.checkEntailed(
       {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)}));
-  ASSERT_THROW(d_solver.checkEntailed(n), CVC4ApiException);
+  ASSERT_THROW(d_solver.checkEntailed(n), CVC5ApiException);
   ASSERT_THROW(d_solver.checkEntailed({n, d_solver.mkTerm(DISTINCT, x, y)}),
-               CVC4ApiException);
+               CVC5ApiException);
   Solver slv;
-  ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC4ApiException);
+  ASSERT_THROW(slv.checkEntailed(d_solver.mkTrue()), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, checkSat)
 {
   d_solver.setOption("incremental", "false");
   ASSERT_NO_THROW(d_solver.checkSat());
-  ASSERT_THROW(d_solver.checkSat(), CVC4ApiException);
+  ASSERT_THROW(d_solver.checkSat(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, checkSatAssuming)
 {
   d_solver.setOption("incremental", "false");
   ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
-  ASSERT_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
+  ASSERT_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()), CVC5ApiException);
   Solver slv;
-  ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
+  ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, checkSatAssuming1)
@@ -1967,11 +1967,11 @@ TEST_F(TestApiBlackSolver, checkSatAssuming1)
   Term z = d_solver.mkTerm(AND, x, y);
   d_solver.setOption("incremental", "true");
   ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
-  ASSERT_THROW(d_solver.checkSatAssuming(Term()), CVC4ApiException);
+  ASSERT_THROW(d_solver.checkSatAssuming(Term()), CVC5ApiException);
   ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTrue()));
   ASSERT_NO_THROW(d_solver.checkSatAssuming(z));
   Solver slv;
-  ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
+  ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, checkSatAssuming2)
@@ -2016,28 +2016,28 @@ TEST_F(TestApiBlackSolver, checkSatAssuming2)
   ASSERT_NO_THROW(d_solver.checkSatAssuming(d_solver.mkTerm(DISTINCT, x, y)));
   ASSERT_NO_THROW(d_solver.checkSatAssuming(
       {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)}));
-  ASSERT_THROW(d_solver.checkSatAssuming(n), CVC4ApiException);
+  ASSERT_THROW(d_solver.checkSatAssuming(n), CVC5ApiException);
   ASSERT_THROW(d_solver.checkSatAssuming({n, d_solver.mkTerm(DISTINCT, x, y)}),
-               CVC4ApiException);
+               CVC5ApiException);
   Solver slv;
-  ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC4ApiException);
+  ASSERT_THROW(slv.checkSatAssuming(d_solver.mkTrue()), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, setLogic)
 {
   ASSERT_NO_THROW(d_solver.setLogic("AUFLIRA"));
-  ASSERT_THROW(d_solver.setLogic("AF_BV"), CVC4ApiException);
+  ASSERT_THROW(d_solver.setLogic("AF_BV"), CVC5ApiException);
   d_solver.assertFormula(d_solver.mkTrue());
-  ASSERT_THROW(d_solver.setLogic("AUFLIRA"), CVC4ApiException);
+  ASSERT_THROW(d_solver.setLogic("AUFLIRA"), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, setOption)
 {
   ASSERT_NO_THROW(d_solver.setOption("bv-sat-solver", "minisat"));
-  ASSERT_THROW(d_solver.setOption("bv-sat-solver", "1"), CVC4ApiException);
+  ASSERT_THROW(d_solver.setOption("bv-sat-solver", "1"), CVC5ApiException);
   d_solver.assertFormula(d_solver.mkTrue());
   ASSERT_THROW(d_solver.setOption("bv-sat-solver", "minisat"),
-               CVC4ApiException);
+               CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, resetAssertions)
@@ -2065,11 +2065,11 @@ TEST_F(TestApiBlackSolver, mkSygusVar)
   ASSERT_NO_THROW(d_solver.mkSygusVar(funSort));
   ASSERT_NO_THROW(d_solver.mkSygusVar(boolSort, std::string("b")));
   ASSERT_NO_THROW(d_solver.mkSygusVar(funSort, ""));
-  ASSERT_THROW(d_solver.mkSygusVar(Sort()), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkSygusVar(Sort()), CVC5ApiException);
   ASSERT_THROW(d_solver.mkSygusVar(d_solver.getNullSort(), "a"),
-               CVC4ApiException);
+               CVC5ApiException);
   Solver slv;
-  ASSERT_THROW(slv.mkSygusVar(boolSort), CVC4ApiException);
+  ASSERT_THROW(slv.mkSygusVar(boolSort), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, mkSygusGrammar)
@@ -2081,16 +2081,16 @@ TEST_F(TestApiBlackSolver, mkSygusGrammar)
 
   ASSERT_NO_THROW(d_solver.mkSygusGrammar({}, {intVar}));
   ASSERT_NO_THROW(d_solver.mkSygusGrammar({boolVar}, {intVar}));
-  ASSERT_THROW(d_solver.mkSygusGrammar({}, {}), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkSygusGrammar({}, {nullTerm}), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkSygusGrammar({}, {boolTerm}), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkSygusGrammar({boolTerm}, {intVar}), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkSygusGrammar({}, {}), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkSygusGrammar({}, {nullTerm}), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkSygusGrammar({}, {boolTerm}), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkSygusGrammar({boolTerm}, {intVar}), CVC5ApiException);
   Solver slv;
   Term boolVar2 = slv.mkVar(slv.getBooleanSort());
   Term intVar2 = slv.mkVar(slv.getIntegerSort());
   ASSERT_NO_THROW(slv.mkSygusGrammar({boolVar2}, {intVar2}));
-  ASSERT_THROW(slv.mkSygusGrammar({boolVar}, {intVar2}), CVC4ApiException);
-  ASSERT_THROW(slv.mkSygusGrammar({boolVar2}, {intVar}), CVC4ApiException);
+  ASSERT_THROW(slv.mkSygusGrammar({boolVar}, {intVar2}), CVC5ApiException);
+  ASSERT_THROW(slv.mkSygusGrammar({boolVar2}, {intVar}), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, synthFun)
@@ -2115,16 +2115,16 @@ TEST_F(TestApiBlackSolver, synthFun)
   ASSERT_NO_THROW(d_solver.synthFun("f1", {x}, boolean));
   ASSERT_NO_THROW(d_solver.synthFun("f2", {x}, boolean, g1));
 
-  ASSERT_THROW(d_solver.synthFun("f3", {nullTerm}, boolean), CVC4ApiException);
-  ASSERT_THROW(d_solver.synthFun("f4", {}, null), CVC4ApiException);
-  ASSERT_THROW(d_solver.synthFun("f6", {x}, boolean, g2), CVC4ApiException);
+  ASSERT_THROW(d_solver.synthFun("f3", {nullTerm}, boolean), CVC5ApiException);
+  ASSERT_THROW(d_solver.synthFun("f4", {}, null), CVC5ApiException);
+  ASSERT_THROW(d_solver.synthFun("f6", {x}, boolean, g2), CVC5ApiException);
   Solver slv;
   Term x2 = slv.mkVar(slv.getBooleanSort());
   ASSERT_NO_THROW(slv.synthFun("f1", {x2}, slv.getBooleanSort()));
   ASSERT_THROW(slv.synthFun("", {}, d_solver.getBooleanSort()),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.synthFun("f1", {x}, d_solver.getBooleanSort()),
-               CVC4ApiException);
+               CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, synthInv)
@@ -2148,8 +2148,8 @@ TEST_F(TestApiBlackSolver, synthInv)
   ASSERT_NO_THROW(d_solver.synthInv("i1", {x}));
   ASSERT_NO_THROW(d_solver.synthInv("i2", {x}, g1));
 
-  ASSERT_THROW(d_solver.synthInv("i3", {nullTerm}), CVC4ApiException);
-  ASSERT_THROW(d_solver.synthInv("i4", {x}, g2), CVC4ApiException);
+  ASSERT_THROW(d_solver.synthInv("i3", {nullTerm}), CVC5ApiException);
+  ASSERT_THROW(d_solver.synthInv("i4", {x}, g2), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, addSygusConstraint)
@@ -2159,11 +2159,11 @@ TEST_F(TestApiBlackSolver, addSygusConstraint)
   Term intTerm = d_solver.mkInteger(1);
 
   ASSERT_NO_THROW(d_solver.addSygusConstraint(boolTerm));
-  ASSERT_THROW(d_solver.addSygusConstraint(nullTerm), CVC4ApiException);
-  ASSERT_THROW(d_solver.addSygusConstraint(intTerm), CVC4ApiException);
+  ASSERT_THROW(d_solver.addSygusConstraint(nullTerm), CVC5ApiException);
+  ASSERT_THROW(d_solver.addSygusConstraint(intTerm), CVC5ApiException);
 
   Solver slv;
-  ASSERT_THROW(slv.addSygusConstraint(boolTerm), CVC4ApiException);
+  ASSERT_THROW(slv.addSygusConstraint(boolTerm), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, addSygusInvConstraint)
@@ -2188,36 +2188,36 @@ TEST_F(TestApiBlackSolver, addSygusInvConstraint)
   ASSERT_NO_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, post));
 
   ASSERT_THROW(d_solver.addSygusInvConstraint(nullTerm, pre, trans, post),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.addSygusInvConstraint(inv, nullTerm, trans, post),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, nullTerm, post),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, nullTerm),
-               CVC4ApiException);
+               CVC5ApiException);
 
   ASSERT_THROW(d_solver.addSygusInvConstraint(intTerm, pre, trans, post),
-               CVC4ApiException);
+               CVC5ApiException);
 
   ASSERT_THROW(d_solver.addSygusInvConstraint(inv1, pre, trans, post),
-               CVC4ApiException);
+               CVC5ApiException);
 
   ASSERT_THROW(d_solver.addSygusInvConstraint(inv, trans, trans, post),
-               CVC4ApiException);
+               CVC5ApiException);
 
   ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, intTerm, post),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, pre, post),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans1, post),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans2, post),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans3, post),
-               CVC4ApiException);
+               CVC5ApiException);
 
   ASSERT_THROW(d_solver.addSygusInvConstraint(inv, pre, trans, trans),
-               CVC4ApiException);
+               CVC5ApiException);
   Solver slv;
   Sort boolean2 = slv.getBooleanSort();
   Sort real2 = slv.getRealSort();
@@ -2227,13 +2227,13 @@ TEST_F(TestApiBlackSolver, addSygusInvConstraint)
   Term post22 = slv.declareFun("post", {real2}, boolean2);
   ASSERT_NO_THROW(slv.addSygusInvConstraint(inv22, pre22, trans22, post22));
   ASSERT_THROW(slv.addSygusInvConstraint(inv, pre22, trans22, post22),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre, trans22, post22),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre22, trans, post22),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre22, trans22, post),
-               CVC4ApiException);
+               CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getSynthSolution)
@@ -2245,18 +2245,18 @@ TEST_F(TestApiBlackSolver, getSynthSolution)
   Term x = d_solver.mkBoolean(false);
   Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
 
-  ASSERT_THROW(d_solver.getSynthSolution(f), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSynthSolution(f), CVC5ApiException);
 
   d_solver.checkSynth();
 
   ASSERT_NO_THROW(d_solver.getSynthSolution(f));
   ASSERT_NO_THROW(d_solver.getSynthSolution(f));
 
-  ASSERT_THROW(d_solver.getSynthSolution(nullTerm), CVC4ApiException);
-  ASSERT_THROW(d_solver.getSynthSolution(x), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSynthSolution(nullTerm), CVC5ApiException);
+  ASSERT_THROW(d_solver.getSynthSolution(x), CVC5ApiException);
 
   Solver slv;
-  ASSERT_THROW(slv.getSynthSolution(f), CVC4ApiException);
+  ASSERT_THROW(slv.getSynthSolution(f), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, getSynthSolutions)
@@ -2268,20 +2268,20 @@ TEST_F(TestApiBlackSolver, getSynthSolutions)
   Term x = d_solver.mkBoolean(false);
   Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
 
-  ASSERT_THROW(d_solver.getSynthSolutions({}), CVC4ApiException);
-  ASSERT_THROW(d_solver.getSynthSolutions({f}), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSynthSolutions({}), CVC5ApiException);
+  ASSERT_THROW(d_solver.getSynthSolutions({f}), CVC5ApiException);
 
   d_solver.checkSynth();
 
   ASSERT_NO_THROW(d_solver.getSynthSolutions({f}));
   ASSERT_NO_THROW(d_solver.getSynthSolutions({f, f}));
 
-  ASSERT_THROW(d_solver.getSynthSolutions({}), CVC4ApiException);
-  ASSERT_THROW(d_solver.getSynthSolutions({nullTerm}), CVC4ApiException);
-  ASSERT_THROW(d_solver.getSynthSolutions({x}), CVC4ApiException);
+  ASSERT_THROW(d_solver.getSynthSolutions({}), CVC5ApiException);
+  ASSERT_THROW(d_solver.getSynthSolutions({nullTerm}), CVC5ApiException);
+  ASSERT_THROW(d_solver.getSynthSolutions({x}), CVC5ApiException);
 
   Solver slv;
-  ASSERT_THROW(slv.getSynthSolutions({x}), CVC4ApiException);
+  ASSERT_THROW(slv.getSynthSolutions({x}), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSolver, tupleProject)
@@ -2315,9 +2315,9 @@ TEST_F(TestApiBlackSolver, tupleProject)
       d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices4), tuple));
 
   ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices5), tuple),
-               CVC4ApiException);
+               CVC5ApiException);
   ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices6), tuple),
-               CVC4ApiException);
+               CVC5ApiException);
 
   std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2};
 
diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp
index 8338ffa2c..c2b924bfa 100644
--- a/test/unit/api/sort_black.cpp
+++ b/test/unit/api/sort_black.cpp
@@ -282,7 +282,7 @@ TEST_F(TestApiBlackSort, getDatatype)
   ASSERT_NO_THROW(dtypeSort.getDatatype());
   // create bv sort, check should fail
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.getDatatype(), CVC4ApiException);
+  ASSERT_THROW(bvSort.getDatatype(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, datatypeSorts)
@@ -291,9 +291,9 @@ TEST_F(TestApiBlackSort, datatypeSorts)
   Sort dtypeSort = create_datatype_sort();
   Datatype dt = dtypeSort.getDatatype();
   ASSERT_FALSE(dtypeSort.isConstructor());
-  ASSERT_THROW(dtypeSort.getConstructorCodomainSort(), CVC4ApiException);
-  ASSERT_THROW(dtypeSort.getConstructorDomainSorts(), CVC4ApiException);
-  ASSERT_THROW(dtypeSort.getConstructorArity(), CVC4ApiException);
+  ASSERT_THROW(dtypeSort.getConstructorCodomainSort(), CVC5ApiException);
+  ASSERT_THROW(dtypeSort.getConstructorDomainSorts(), CVC5ApiException);
+  ASSERT_THROW(dtypeSort.getConstructorArity(), CVC5ApiException);
 
   // get constructor
   DatatypeConstructor dcons = dt[0];
@@ -314,8 +314,8 @@ TEST_F(TestApiBlackSort, datatypeSorts)
   ASSERT_EQ(isConsTerm.getSort().getTesterDomainSort(), dtypeSort);
   Sort booleanSort = d_solver.getBooleanSort();
   ASSERT_EQ(isConsTerm.getSort().getTesterCodomainSort(), booleanSort);
-  ASSERT_THROW(booleanSort.getTesterDomainSort(), CVC4ApiException);
-  ASSERT_THROW(booleanSort.getTesterCodomainSort(), CVC4ApiException);
+  ASSERT_THROW(booleanSort.getTesterDomainSort(), CVC5ApiException);
+  ASSERT_THROW(booleanSort.getTesterCodomainSort(), CVC5ApiException);
 
   // get selector
   DatatypeSelector dselTail = dcons[1];
@@ -323,8 +323,8 @@ TEST_F(TestApiBlackSort, datatypeSorts)
   ASSERT_TRUE(tailTerm.getSort().isSelector());
   ASSERT_EQ(tailTerm.getSort().getSelectorDomainSort(), dtypeSort);
   ASSERT_EQ(tailTerm.getSort().getSelectorCodomainSort(), dtypeSort);
-  ASSERT_THROW(booleanSort.getSelectorDomainSort(), CVC4ApiException);
-  ASSERT_THROW(booleanSort.getSelectorCodomainSort(), CVC4ApiException);
+  ASSERT_THROW(booleanSort.getSelectorDomainSort(), CVC5ApiException);
+  ASSERT_THROW(booleanSort.getSelectorCodomainSort(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, instantiate)
@@ -343,7 +343,7 @@ TEST_F(TestApiBlackSort, instantiate)
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   ASSERT_THROW(
       dtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}),
-      CVC4ApiException);
+      CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getFunctionArity)
@@ -352,7 +352,7 @@ TEST_F(TestApiBlackSort, getFunctionArity)
                                          d_solver.getIntegerSort());
   ASSERT_NO_THROW(funSort.getFunctionArity());
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.getFunctionArity(), CVC4ApiException);
+  ASSERT_THROW(bvSort.getFunctionArity(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getFunctionDomainSorts)
@@ -361,7 +361,7 @@ TEST_F(TestApiBlackSort, getFunctionDomainSorts)
                                          d_solver.getIntegerSort());
   ASSERT_NO_THROW(funSort.getFunctionDomainSorts());
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.getFunctionDomainSorts(), CVC4ApiException);
+  ASSERT_THROW(bvSort.getFunctionDomainSorts(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getFunctionCodomainSort)
@@ -370,7 +370,7 @@ TEST_F(TestApiBlackSort, getFunctionCodomainSort)
                                          d_solver.getIntegerSort());
   ASSERT_NO_THROW(funSort.getFunctionCodomainSort());
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.getFunctionCodomainSort(), CVC4ApiException);
+  ASSERT_THROW(bvSort.getFunctionCodomainSort(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getArrayIndexSort)
@@ -379,7 +379,7 @@ TEST_F(TestApiBlackSort, getArrayIndexSort)
   Sort indexSort = d_solver.mkBitVectorSort(32);
   Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
   ASSERT_NO_THROW(arraySort.getArrayIndexSort());
-  ASSERT_THROW(indexSort.getArrayIndexSort(), CVC4ApiException);
+  ASSERT_THROW(indexSort.getArrayIndexSort(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getArrayElementSort)
@@ -388,7 +388,7 @@ TEST_F(TestApiBlackSort, getArrayElementSort)
   Sort indexSort = d_solver.mkBitVectorSort(32);
   Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
   ASSERT_NO_THROW(arraySort.getArrayElementSort());
-  ASSERT_THROW(indexSort.getArrayElementSort(), CVC4ApiException);
+  ASSERT_THROW(indexSort.getArrayElementSort(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getSetElementSort)
@@ -398,7 +398,7 @@ TEST_F(TestApiBlackSort, getSetElementSort)
   Sort elementSort = setSort.getSetElementSort();
   ASSERT_EQ(elementSort, d_solver.getIntegerSort());
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.getSetElementSort(), CVC4ApiException);
+  ASSERT_THROW(bvSort.getSetElementSort(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getBagElementSort)
@@ -408,7 +408,7 @@ TEST_F(TestApiBlackSort, getBagElementSort)
   Sort elementSort = bagSort.getBagElementSort();
   ASSERT_EQ(elementSort, d_solver.getIntegerSort());
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.getBagElementSort(), CVC4ApiException);
+  ASSERT_THROW(bvSort.getBagElementSort(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getSequenceElementSort)
@@ -418,7 +418,7 @@ TEST_F(TestApiBlackSort, getSequenceElementSort)
   ASSERT_NO_THROW(seqSort.getSequenceElementSort());
   Sort bvSort = d_solver.mkBitVectorSort(32);
   ASSERT_FALSE(bvSort.isSequence());
-  ASSERT_THROW(bvSort.getSequenceElementSort(), CVC4ApiException);
+  ASSERT_THROW(bvSort.getSequenceElementSort(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getUninterpretedSortName)
@@ -426,7 +426,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortName)
   Sort uSort = d_solver.mkUninterpretedSort("u");
   ASSERT_NO_THROW(uSort.getUninterpretedSortName());
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.getUninterpretedSortName(), CVC4ApiException);
+  ASSERT_THROW(bvSort.getUninterpretedSortName(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, isUninterpretedSortParameterized)
@@ -437,7 +437,7 @@ TEST_F(TestApiBlackSort, isUninterpretedSortParameterized)
   Sort siSort = sSort.instantiate({uSort});
   ASSERT_TRUE(siSort.isUninterpretedSortParameterized());
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.isUninterpretedSortParameterized(), CVC4ApiException);
+  ASSERT_THROW(bvSort.isUninterpretedSortParameterized(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts)
@@ -448,7 +448,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts)
   Sort siSort = sSort.instantiate({uSort, uSort});
   ASSERT_EQ(siSort.getUninterpretedSortParamSorts().size(), 2);
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException);
+  ASSERT_THROW(bvSort.getUninterpretedSortParamSorts(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName)
@@ -456,7 +456,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName)
   Sort sSort = d_solver.mkSortConstructorSort("s", 2);
   ASSERT_NO_THROW(sSort.getSortConstructorName());
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.getSortConstructorName(), CVC4ApiException);
+  ASSERT_THROW(bvSort.getSortConstructorName(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity)
@@ -464,7 +464,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity)
   Sort sSort = d_solver.mkSortConstructorSort("s", 2);
   ASSERT_NO_THROW(sSort.getSortConstructorArity());
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.getSortConstructorArity(), CVC4ApiException);
+  ASSERT_THROW(bvSort.getSortConstructorArity(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getBVSize)
@@ -472,7 +472,7 @@ TEST_F(TestApiBlackSort, getBVSize)
   Sort bvSort = d_solver.mkBitVectorSort(32);
   ASSERT_NO_THROW(bvSort.getBVSize());
   Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-  ASSERT_THROW(setSort.getBVSize(), CVC4ApiException);
+  ASSERT_THROW(setSort.getBVSize(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getFPExponentSize)
@@ -482,7 +482,7 @@ TEST_F(TestApiBlackSort, getFPExponentSize)
     Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
     ASSERT_NO_THROW(fpSort.getFPExponentSize());
     Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-    ASSERT_THROW(setSort.getFPExponentSize(), CVC4ApiException);
+    ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException);
   }
 }
 
@@ -493,7 +493,7 @@ TEST_F(TestApiBlackSort, getFPSignificandSize)
     Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
     ASSERT_NO_THROW(fpSort.getFPSignificandSize());
     Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-    ASSERT_THROW(setSort.getFPSignificandSize(), CVC4ApiException);
+    ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException);
   }
 }
 
@@ -518,7 +518,7 @@ TEST_F(TestApiBlackSort, getDatatypeParamSorts)
   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
-  ASSERT_THROW(dtypeSort.getDatatypeParamSorts(), CVC4ApiException);
+  ASSERT_THROW(dtypeSort.getDatatypeParamSorts(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getDatatypeArity)
@@ -534,7 +534,7 @@ TEST_F(TestApiBlackSort, getDatatypeArity)
   ASSERT_NO_THROW(dtypeSort.getDatatypeArity());
   // create bv sort, check should fail
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.getDatatypeArity(), CVC4ApiException);
+  ASSERT_THROW(bvSort.getDatatypeArity(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getTupleLength)
@@ -543,7 +543,7 @@ TEST_F(TestApiBlackSort, getTupleLength)
       {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
   ASSERT_NO_THROW(tupleSort.getTupleLength());
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.getTupleLength(), CVC4ApiException);
+  ASSERT_THROW(bvSort.getTupleLength(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getTupleSorts)
@@ -552,7 +552,7 @@ TEST_F(TestApiBlackSort, getTupleSorts)
       {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
   ASSERT_NO_THROW(tupleSort.getTupleSorts());
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_THROW(bvSort.getTupleSorts(), CVC4ApiException);
+  ASSERT_THROW(bvSort.getTupleSorts(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, sortCompare)
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index d894f9720..9dd803c93 100644
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -43,7 +43,7 @@ TEST_F(TestApiBlackTerm, eq)
 TEST_F(TestApiBlackTerm, getId)
 {
   Term n;
-  ASSERT_THROW(n.getId(), CVC4ApiException);
+  ASSERT_THROW(n.getId(), CVC5ApiException);
   Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
   ASSERT_NO_THROW(x.getId());
   Term y = x;
@@ -62,7 +62,7 @@ TEST_F(TestApiBlackTerm, getKind)
   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
   Term n;
-  ASSERT_THROW(n.getKind(), CVC4ApiException);
+  ASSERT_THROW(n.getKind(), CVC5ApiException);
   Term x = d_solver.mkVar(uSort, "x");
   ASSERT_NO_THROW(x.getKind());
   Term y = d_solver.mkVar(uSort, "y");
@@ -104,7 +104,7 @@ TEST_F(TestApiBlackTerm, getSort)
   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
   Term n;
-  ASSERT_THROW(n.getSort(), CVC4ApiException);
+  ASSERT_THROW(n.getSort(), CVC5ApiException);
   Term x = d_solver.mkVar(bvSort, "x");
   ASSERT_NO_THROW(x.getSort());
   ASSERT_EQ(x.getSort(), bvSort);
@@ -152,7 +152,7 @@ TEST_F(TestApiBlackTerm, getOp)
   Term b = d_solver.mkConst(bvsort, "b");
 
   ASSERT_FALSE(x.hasOp());
-  ASSERT_THROW(x.getOp(), CVC4ApiException);
+  ASSERT_THROW(x.getOp(), CVC5ApiException);
 
   Term ab = d_solver.mkTerm(SELECT, a, b);
   Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
@@ -169,7 +169,7 @@ TEST_F(TestApiBlackTerm, getOp)
   Term fx = d_solver.mkTerm(APPLY_UF, f, x);
 
   ASSERT_FALSE(f.hasOp());
-  ASSERT_THROW(f.getOp(), CVC4ApiException);
+  ASSERT_THROW(f.getOp(), CVC5ApiException);
   ASSERT_TRUE(fx.hasOp());
   std::vector<Term> children(fx.begin(), fx.end());
   // testing rebuild from op and children
@@ -228,21 +228,21 @@ TEST_F(TestApiBlackTerm, notTerm)
   Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
-  ASSERT_THROW(Term().notTerm(), CVC4ApiException);
+  ASSERT_THROW(Term().notTerm(), CVC5ApiException);
   Term b = d_solver.mkTrue();
   ASSERT_NO_THROW(b.notTerm());
   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
-  ASSERT_THROW(x.notTerm(), CVC4ApiException);
+  ASSERT_THROW(x.notTerm(), CVC5ApiException);
   Term f = d_solver.mkVar(funSort1, "f");
-  ASSERT_THROW(f.notTerm(), CVC4ApiException);
+  ASSERT_THROW(f.notTerm(), CVC5ApiException);
   Term p = d_solver.mkVar(funSort2, "p");
-  ASSERT_THROW(p.notTerm(), CVC4ApiException);
+  ASSERT_THROW(p.notTerm(), CVC5ApiException);
   Term zero = d_solver.mkInteger(0);
-  ASSERT_THROW(zero.notTerm(), CVC4ApiException);
+  ASSERT_THROW(zero.notTerm(), CVC5ApiException);
   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  ASSERT_THROW(f_x.notTerm(), CVC4ApiException);
+  ASSERT_THROW(f_x.notTerm(), CVC5ApiException);
   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
-  ASSERT_THROW(sum.notTerm(), CVC4ApiException);
+  ASSERT_THROW(sum.notTerm(), CVC5ApiException);
   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
   ASSERT_NO_THROW(p_0.notTerm());
   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
@@ -258,59 +258,59 @@ TEST_F(TestApiBlackTerm, andTerm)
   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
   Term b = d_solver.mkTrue();
-  ASSERT_THROW(Term().andTerm(b), CVC4ApiException);
-  ASSERT_THROW(b.andTerm(Term()), CVC4ApiException);
+  ASSERT_THROW(Term().andTerm(b), CVC5ApiException);
+  ASSERT_THROW(b.andTerm(Term()), CVC5ApiException);
   ASSERT_NO_THROW(b.andTerm(b));
   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
-  ASSERT_THROW(x.andTerm(b), CVC4ApiException);
-  ASSERT_THROW(x.andTerm(x), CVC4ApiException);
+  ASSERT_THROW(x.andTerm(b), CVC5ApiException);
+  ASSERT_THROW(x.andTerm(x), CVC5ApiException);
   Term f = d_solver.mkVar(funSort1, "f");
-  ASSERT_THROW(f.andTerm(b), CVC4ApiException);
-  ASSERT_THROW(f.andTerm(x), CVC4ApiException);
-  ASSERT_THROW(f.andTerm(f), CVC4ApiException);
+  ASSERT_THROW(f.andTerm(b), CVC5ApiException);
+  ASSERT_THROW(f.andTerm(x), CVC5ApiException);
+  ASSERT_THROW(f.andTerm(f), CVC5ApiException);
   Term p = d_solver.mkVar(funSort2, "p");
-  ASSERT_THROW(p.andTerm(b), CVC4ApiException);
-  ASSERT_THROW(p.andTerm(x), CVC4ApiException);
-  ASSERT_THROW(p.andTerm(f), CVC4ApiException);
-  ASSERT_THROW(p.andTerm(p), CVC4ApiException);
+  ASSERT_THROW(p.andTerm(b), CVC5ApiException);
+  ASSERT_THROW(p.andTerm(x), CVC5ApiException);
+  ASSERT_THROW(p.andTerm(f), CVC5ApiException);
+  ASSERT_THROW(p.andTerm(p), CVC5ApiException);
   Term zero = d_solver.mkInteger(0);
-  ASSERT_THROW(zero.andTerm(b), CVC4ApiException);
-  ASSERT_THROW(zero.andTerm(x), CVC4ApiException);
-  ASSERT_THROW(zero.andTerm(f), CVC4ApiException);
-  ASSERT_THROW(zero.andTerm(p), CVC4ApiException);
-  ASSERT_THROW(zero.andTerm(zero), CVC4ApiException);
+  ASSERT_THROW(zero.andTerm(b), CVC5ApiException);
+  ASSERT_THROW(zero.andTerm(x), CVC5ApiException);
+  ASSERT_THROW(zero.andTerm(f), CVC5ApiException);
+  ASSERT_THROW(zero.andTerm(p), CVC5ApiException);
+  ASSERT_THROW(zero.andTerm(zero), CVC5ApiException);
   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  ASSERT_THROW(f_x.andTerm(b), CVC4ApiException);
-  ASSERT_THROW(f_x.andTerm(x), CVC4ApiException);
-  ASSERT_THROW(f_x.andTerm(f), CVC4ApiException);
-  ASSERT_THROW(f_x.andTerm(p), CVC4ApiException);
-  ASSERT_THROW(f_x.andTerm(zero), CVC4ApiException);
-  ASSERT_THROW(f_x.andTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(f_x.andTerm(b), CVC5ApiException);
+  ASSERT_THROW(f_x.andTerm(x), CVC5ApiException);
+  ASSERT_THROW(f_x.andTerm(f), CVC5ApiException);
+  ASSERT_THROW(f_x.andTerm(p), CVC5ApiException);
+  ASSERT_THROW(f_x.andTerm(zero), CVC5ApiException);
+  ASSERT_THROW(f_x.andTerm(f_x), CVC5ApiException);
   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
-  ASSERT_THROW(sum.andTerm(b), CVC4ApiException);
-  ASSERT_THROW(sum.andTerm(x), CVC4ApiException);
-  ASSERT_THROW(sum.andTerm(f), CVC4ApiException);
-  ASSERT_THROW(sum.andTerm(p), CVC4ApiException);
-  ASSERT_THROW(sum.andTerm(zero), CVC4ApiException);
-  ASSERT_THROW(sum.andTerm(f_x), CVC4ApiException);
-  ASSERT_THROW(sum.andTerm(sum), CVC4ApiException);
+  ASSERT_THROW(sum.andTerm(b), CVC5ApiException);
+  ASSERT_THROW(sum.andTerm(x), CVC5ApiException);
+  ASSERT_THROW(sum.andTerm(f), CVC5ApiException);
+  ASSERT_THROW(sum.andTerm(p), CVC5ApiException);
+  ASSERT_THROW(sum.andTerm(zero), CVC5ApiException);
+  ASSERT_THROW(sum.andTerm(f_x), CVC5ApiException);
+  ASSERT_THROW(sum.andTerm(sum), CVC5ApiException);
   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
   ASSERT_NO_THROW(p_0.andTerm(b));
-  ASSERT_THROW(p_0.andTerm(x), CVC4ApiException);
-  ASSERT_THROW(p_0.andTerm(f), CVC4ApiException);
-  ASSERT_THROW(p_0.andTerm(p), CVC4ApiException);
-  ASSERT_THROW(p_0.andTerm(zero), CVC4ApiException);
-  ASSERT_THROW(p_0.andTerm(f_x), CVC4ApiException);
-  ASSERT_THROW(p_0.andTerm(sum), CVC4ApiException);
+  ASSERT_THROW(p_0.andTerm(x), CVC5ApiException);
+  ASSERT_THROW(p_0.andTerm(f), CVC5ApiException);
+  ASSERT_THROW(p_0.andTerm(p), CVC5ApiException);
+  ASSERT_THROW(p_0.andTerm(zero), CVC5ApiException);
+  ASSERT_THROW(p_0.andTerm(f_x), CVC5ApiException);
+  ASSERT_THROW(p_0.andTerm(sum), CVC5ApiException);
   ASSERT_NO_THROW(p_0.andTerm(p_0));
   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
   ASSERT_NO_THROW(p_f_x.andTerm(b));
-  ASSERT_THROW(p_f_x.andTerm(x), CVC4ApiException);
-  ASSERT_THROW(p_f_x.andTerm(f), CVC4ApiException);
-  ASSERT_THROW(p_f_x.andTerm(p), CVC4ApiException);
-  ASSERT_THROW(p_f_x.andTerm(zero), CVC4ApiException);
-  ASSERT_THROW(p_f_x.andTerm(f_x), CVC4ApiException);
-  ASSERT_THROW(p_f_x.andTerm(sum), CVC4ApiException);
+  ASSERT_THROW(p_f_x.andTerm(x), CVC5ApiException);
+  ASSERT_THROW(p_f_x.andTerm(f), CVC5ApiException);
+  ASSERT_THROW(p_f_x.andTerm(p), CVC5ApiException);
+  ASSERT_THROW(p_f_x.andTerm(zero), CVC5ApiException);
+  ASSERT_THROW(p_f_x.andTerm(f_x), CVC5ApiException);
+  ASSERT_THROW(p_f_x.andTerm(sum), CVC5ApiException);
   ASSERT_NO_THROW(p_f_x.andTerm(p_0));
   ASSERT_NO_THROW(p_f_x.andTerm(p_f_x));
 }
@@ -324,59 +324,59 @@ TEST_F(TestApiBlackTerm, orTerm)
   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
   Term b = d_solver.mkTrue();
-  ASSERT_THROW(Term().orTerm(b), CVC4ApiException);
-  ASSERT_THROW(b.orTerm(Term()), CVC4ApiException);
+  ASSERT_THROW(Term().orTerm(b), CVC5ApiException);
+  ASSERT_THROW(b.orTerm(Term()), CVC5ApiException);
   ASSERT_NO_THROW(b.orTerm(b));
   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
-  ASSERT_THROW(x.orTerm(b), CVC4ApiException);
-  ASSERT_THROW(x.orTerm(x), CVC4ApiException);
+  ASSERT_THROW(x.orTerm(b), CVC5ApiException);
+  ASSERT_THROW(x.orTerm(x), CVC5ApiException);
   Term f = d_solver.mkVar(funSort1, "f");
-  ASSERT_THROW(f.orTerm(b), CVC4ApiException);
-  ASSERT_THROW(f.orTerm(x), CVC4ApiException);
-  ASSERT_THROW(f.orTerm(f), CVC4ApiException);
+  ASSERT_THROW(f.orTerm(b), CVC5ApiException);
+  ASSERT_THROW(f.orTerm(x), CVC5ApiException);
+  ASSERT_THROW(f.orTerm(f), CVC5ApiException);
   Term p = d_solver.mkVar(funSort2, "p");
-  ASSERT_THROW(p.orTerm(b), CVC4ApiException);
-  ASSERT_THROW(p.orTerm(x), CVC4ApiException);
-  ASSERT_THROW(p.orTerm(f), CVC4ApiException);
-  ASSERT_THROW(p.orTerm(p), CVC4ApiException);
+  ASSERT_THROW(p.orTerm(b), CVC5ApiException);
+  ASSERT_THROW(p.orTerm(x), CVC5ApiException);
+  ASSERT_THROW(p.orTerm(f), CVC5ApiException);
+  ASSERT_THROW(p.orTerm(p), CVC5ApiException);
   Term zero = d_solver.mkInteger(0);
-  ASSERT_THROW(zero.orTerm(b), CVC4ApiException);
-  ASSERT_THROW(zero.orTerm(x), CVC4ApiException);
-  ASSERT_THROW(zero.orTerm(f), CVC4ApiException);
-  ASSERT_THROW(zero.orTerm(p), CVC4ApiException);
-  ASSERT_THROW(zero.orTerm(zero), CVC4ApiException);
+  ASSERT_THROW(zero.orTerm(b), CVC5ApiException);
+  ASSERT_THROW(zero.orTerm(x), CVC5ApiException);
+  ASSERT_THROW(zero.orTerm(f), CVC5ApiException);
+  ASSERT_THROW(zero.orTerm(p), CVC5ApiException);
+  ASSERT_THROW(zero.orTerm(zero), CVC5ApiException);
   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  ASSERT_THROW(f_x.orTerm(b), CVC4ApiException);
-  ASSERT_THROW(f_x.orTerm(x), CVC4ApiException);
-  ASSERT_THROW(f_x.orTerm(f), CVC4ApiException);
-  ASSERT_THROW(f_x.orTerm(p), CVC4ApiException);
-  ASSERT_THROW(f_x.orTerm(zero), CVC4ApiException);
-  ASSERT_THROW(f_x.orTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(f_x.orTerm(b), CVC5ApiException);
+  ASSERT_THROW(f_x.orTerm(x), CVC5ApiException);
+  ASSERT_THROW(f_x.orTerm(f), CVC5ApiException);
+  ASSERT_THROW(f_x.orTerm(p), CVC5ApiException);
+  ASSERT_THROW(f_x.orTerm(zero), CVC5ApiException);
+  ASSERT_THROW(f_x.orTerm(f_x), CVC5ApiException);
   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
-  ASSERT_THROW(sum.orTerm(b), CVC4ApiException);
-  ASSERT_THROW(sum.orTerm(x), CVC4ApiException);
-  ASSERT_THROW(sum.orTerm(f), CVC4ApiException);
-  ASSERT_THROW(sum.orTerm(p), CVC4ApiException);
-  ASSERT_THROW(sum.orTerm(zero), CVC4ApiException);
-  ASSERT_THROW(sum.orTerm(f_x), CVC4ApiException);
-  ASSERT_THROW(sum.orTerm(sum), CVC4ApiException);
+  ASSERT_THROW(sum.orTerm(b), CVC5ApiException);
+  ASSERT_THROW(sum.orTerm(x), CVC5ApiException);
+  ASSERT_THROW(sum.orTerm(f), CVC5ApiException);
+  ASSERT_THROW(sum.orTerm(p), CVC5ApiException);
+  ASSERT_THROW(sum.orTerm(zero), CVC5ApiException);
+  ASSERT_THROW(sum.orTerm(f_x), CVC5ApiException);
+  ASSERT_THROW(sum.orTerm(sum), CVC5ApiException);
   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
   ASSERT_NO_THROW(p_0.orTerm(b));
-  ASSERT_THROW(p_0.orTerm(x), CVC4ApiException);
-  ASSERT_THROW(p_0.orTerm(f), CVC4ApiException);
-  ASSERT_THROW(p_0.orTerm(p), CVC4ApiException);
-  ASSERT_THROW(p_0.orTerm(zero), CVC4ApiException);
-  ASSERT_THROW(p_0.orTerm(f_x), CVC4ApiException);
-  ASSERT_THROW(p_0.orTerm(sum), CVC4ApiException);
+  ASSERT_THROW(p_0.orTerm(x), CVC5ApiException);
+  ASSERT_THROW(p_0.orTerm(f), CVC5ApiException);
+  ASSERT_THROW(p_0.orTerm(p), CVC5ApiException);
+  ASSERT_THROW(p_0.orTerm(zero), CVC5ApiException);
+  ASSERT_THROW(p_0.orTerm(f_x), CVC5ApiException);
+  ASSERT_THROW(p_0.orTerm(sum), CVC5ApiException);
   ASSERT_NO_THROW(p_0.orTerm(p_0));
   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
   ASSERT_NO_THROW(p_f_x.orTerm(b));
-  ASSERT_THROW(p_f_x.orTerm(x), CVC4ApiException);
-  ASSERT_THROW(p_f_x.orTerm(f), CVC4ApiException);
-  ASSERT_THROW(p_f_x.orTerm(p), CVC4ApiException);
-  ASSERT_THROW(p_f_x.orTerm(zero), CVC4ApiException);
-  ASSERT_THROW(p_f_x.orTerm(f_x), CVC4ApiException);
-  ASSERT_THROW(p_f_x.orTerm(sum), CVC4ApiException);
+  ASSERT_THROW(p_f_x.orTerm(x), CVC5ApiException);
+  ASSERT_THROW(p_f_x.orTerm(f), CVC5ApiException);
+  ASSERT_THROW(p_f_x.orTerm(p), CVC5ApiException);
+  ASSERT_THROW(p_f_x.orTerm(zero), CVC5ApiException);
+  ASSERT_THROW(p_f_x.orTerm(f_x), CVC5ApiException);
+  ASSERT_THROW(p_f_x.orTerm(sum), CVC5ApiException);
   ASSERT_NO_THROW(p_f_x.orTerm(p_0));
   ASSERT_NO_THROW(p_f_x.orTerm(p_f_x));
 }
@@ -390,59 +390,59 @@ TEST_F(TestApiBlackTerm, xorTerm)
   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
   Term b = d_solver.mkTrue();
-  ASSERT_THROW(Term().xorTerm(b), CVC4ApiException);
-  ASSERT_THROW(b.xorTerm(Term()), CVC4ApiException);
+  ASSERT_THROW(Term().xorTerm(b), CVC5ApiException);
+  ASSERT_THROW(b.xorTerm(Term()), CVC5ApiException);
   ASSERT_NO_THROW(b.xorTerm(b));
   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
-  ASSERT_THROW(x.xorTerm(b), CVC4ApiException);
-  ASSERT_THROW(x.xorTerm(x), CVC4ApiException);
+  ASSERT_THROW(x.xorTerm(b), CVC5ApiException);
+  ASSERT_THROW(x.xorTerm(x), CVC5ApiException);
   Term f = d_solver.mkVar(funSort1, "f");
-  ASSERT_THROW(f.xorTerm(b), CVC4ApiException);
-  ASSERT_THROW(f.xorTerm(x), CVC4ApiException);
-  ASSERT_THROW(f.xorTerm(f), CVC4ApiException);
+  ASSERT_THROW(f.xorTerm(b), CVC5ApiException);
+  ASSERT_THROW(f.xorTerm(x), CVC5ApiException);
+  ASSERT_THROW(f.xorTerm(f), CVC5ApiException);
   Term p = d_solver.mkVar(funSort2, "p");
-  ASSERT_THROW(p.xorTerm(b), CVC4ApiException);
-  ASSERT_THROW(p.xorTerm(x), CVC4ApiException);
-  ASSERT_THROW(p.xorTerm(f), CVC4ApiException);
-  ASSERT_THROW(p.xorTerm(p), CVC4ApiException);
+  ASSERT_THROW(p.xorTerm(b), CVC5ApiException);
+  ASSERT_THROW(p.xorTerm(x), CVC5ApiException);
+  ASSERT_THROW(p.xorTerm(f), CVC5ApiException);
+  ASSERT_THROW(p.xorTerm(p), CVC5ApiException);
   Term zero = d_solver.mkInteger(0);
-  ASSERT_THROW(zero.xorTerm(b), CVC4ApiException);
-  ASSERT_THROW(zero.xorTerm(x), CVC4ApiException);
-  ASSERT_THROW(zero.xorTerm(f), CVC4ApiException);
-  ASSERT_THROW(zero.xorTerm(p), CVC4ApiException);
-  ASSERT_THROW(zero.xorTerm(zero), CVC4ApiException);
+  ASSERT_THROW(zero.xorTerm(b), CVC5ApiException);
+  ASSERT_THROW(zero.xorTerm(x), CVC5ApiException);
+  ASSERT_THROW(zero.xorTerm(f), CVC5ApiException);
+  ASSERT_THROW(zero.xorTerm(p), CVC5ApiException);
+  ASSERT_THROW(zero.xorTerm(zero), CVC5ApiException);
   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  ASSERT_THROW(f_x.xorTerm(b), CVC4ApiException);
-  ASSERT_THROW(f_x.xorTerm(x), CVC4ApiException);
-  ASSERT_THROW(f_x.xorTerm(f), CVC4ApiException);
-  ASSERT_THROW(f_x.xorTerm(p), CVC4ApiException);
-  ASSERT_THROW(f_x.xorTerm(zero), CVC4ApiException);
-  ASSERT_THROW(f_x.xorTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(f_x.xorTerm(b), CVC5ApiException);
+  ASSERT_THROW(f_x.xorTerm(x), CVC5ApiException);
+  ASSERT_THROW(f_x.xorTerm(f), CVC5ApiException);
+  ASSERT_THROW(f_x.xorTerm(p), CVC5ApiException);
+  ASSERT_THROW(f_x.xorTerm(zero), CVC5ApiException);
+  ASSERT_THROW(f_x.xorTerm(f_x), CVC5ApiException);
   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
-  ASSERT_THROW(sum.xorTerm(b), CVC4ApiException);
-  ASSERT_THROW(sum.xorTerm(x), CVC4ApiException);
-  ASSERT_THROW(sum.xorTerm(f), CVC4ApiException);
-  ASSERT_THROW(sum.xorTerm(p), CVC4ApiException);
-  ASSERT_THROW(sum.xorTerm(zero), CVC4ApiException);
-  ASSERT_THROW(sum.xorTerm(f_x), CVC4ApiException);
-  ASSERT_THROW(sum.xorTerm(sum), CVC4ApiException);
+  ASSERT_THROW(sum.xorTerm(b), CVC5ApiException);
+  ASSERT_THROW(sum.xorTerm(x), CVC5ApiException);
+  ASSERT_THROW(sum.xorTerm(f), CVC5ApiException);
+  ASSERT_THROW(sum.xorTerm(p), CVC5ApiException);
+  ASSERT_THROW(sum.xorTerm(zero), CVC5ApiException);
+  ASSERT_THROW(sum.xorTerm(f_x), CVC5ApiException);
+  ASSERT_THROW(sum.xorTerm(sum), CVC5ApiException);
   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
   ASSERT_NO_THROW(p_0.xorTerm(b));
-  ASSERT_THROW(p_0.xorTerm(x), CVC4ApiException);
-  ASSERT_THROW(p_0.xorTerm(f), CVC4ApiException);
-  ASSERT_THROW(p_0.xorTerm(p), CVC4ApiException);
-  ASSERT_THROW(p_0.xorTerm(zero), CVC4ApiException);
-  ASSERT_THROW(p_0.xorTerm(f_x), CVC4ApiException);
-  ASSERT_THROW(p_0.xorTerm(sum), CVC4ApiException);
+  ASSERT_THROW(p_0.xorTerm(x), CVC5ApiException);
+  ASSERT_THROW(p_0.xorTerm(f), CVC5ApiException);
+  ASSERT_THROW(p_0.xorTerm(p), CVC5ApiException);
+  ASSERT_THROW(p_0.xorTerm(zero), CVC5ApiException);
+  ASSERT_THROW(p_0.xorTerm(f_x), CVC5ApiException);
+  ASSERT_THROW(p_0.xorTerm(sum), CVC5ApiException);
   ASSERT_NO_THROW(p_0.xorTerm(p_0));
   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
   ASSERT_NO_THROW(p_f_x.xorTerm(b));
-  ASSERT_THROW(p_f_x.xorTerm(x), CVC4ApiException);
-  ASSERT_THROW(p_f_x.xorTerm(f), CVC4ApiException);
-  ASSERT_THROW(p_f_x.xorTerm(p), CVC4ApiException);
-  ASSERT_THROW(p_f_x.xorTerm(zero), CVC4ApiException);
-  ASSERT_THROW(p_f_x.xorTerm(f_x), CVC4ApiException);
-  ASSERT_THROW(p_f_x.xorTerm(sum), CVC4ApiException);
+  ASSERT_THROW(p_f_x.xorTerm(x), CVC5ApiException);
+  ASSERT_THROW(p_f_x.xorTerm(f), CVC5ApiException);
+  ASSERT_THROW(p_f_x.xorTerm(p), CVC5ApiException);
+  ASSERT_THROW(p_f_x.xorTerm(zero), CVC5ApiException);
+  ASSERT_THROW(p_f_x.xorTerm(f_x), CVC5ApiException);
+  ASSERT_THROW(p_f_x.xorTerm(sum), CVC5ApiException);
   ASSERT_NO_THROW(p_f_x.xorTerm(p_0));
   ASSERT_NO_THROW(p_f_x.xorTerm(p_f_x));
 }
@@ -456,59 +456,59 @@ TEST_F(TestApiBlackTerm, eqTerm)
   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
   Term b = d_solver.mkTrue();
-  ASSERT_THROW(Term().eqTerm(b), CVC4ApiException);
-  ASSERT_THROW(b.eqTerm(Term()), CVC4ApiException);
+  ASSERT_THROW(Term().eqTerm(b), CVC5ApiException);
+  ASSERT_THROW(b.eqTerm(Term()), CVC5ApiException);
   ASSERT_NO_THROW(b.eqTerm(b));
   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
-  ASSERT_THROW(x.eqTerm(b), CVC4ApiException);
+  ASSERT_THROW(x.eqTerm(b), CVC5ApiException);
   ASSERT_NO_THROW(x.eqTerm(x));
   Term f = d_solver.mkVar(funSort1, "f");
-  ASSERT_THROW(f.eqTerm(b), CVC4ApiException);
-  ASSERT_THROW(f.eqTerm(x), CVC4ApiException);
+  ASSERT_THROW(f.eqTerm(b), CVC5ApiException);
+  ASSERT_THROW(f.eqTerm(x), CVC5ApiException);
   ASSERT_NO_THROW(f.eqTerm(f));
   Term p = d_solver.mkVar(funSort2, "p");
-  ASSERT_THROW(p.eqTerm(b), CVC4ApiException);
-  ASSERT_THROW(p.eqTerm(x), CVC4ApiException);
-  ASSERT_THROW(p.eqTerm(f), CVC4ApiException);
+  ASSERT_THROW(p.eqTerm(b), CVC5ApiException);
+  ASSERT_THROW(p.eqTerm(x), CVC5ApiException);
+  ASSERT_THROW(p.eqTerm(f), CVC5ApiException);
   ASSERT_NO_THROW(p.eqTerm(p));
   Term zero = d_solver.mkInteger(0);
-  ASSERT_THROW(zero.eqTerm(b), CVC4ApiException);
-  ASSERT_THROW(zero.eqTerm(x), CVC4ApiException);
-  ASSERT_THROW(zero.eqTerm(f), CVC4ApiException);
-  ASSERT_THROW(zero.eqTerm(p), CVC4ApiException);
+  ASSERT_THROW(zero.eqTerm(b), CVC5ApiException);
+  ASSERT_THROW(zero.eqTerm(x), CVC5ApiException);
+  ASSERT_THROW(zero.eqTerm(f), CVC5ApiException);
+  ASSERT_THROW(zero.eqTerm(p), CVC5ApiException);
   ASSERT_NO_THROW(zero.eqTerm(zero));
   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  ASSERT_THROW(f_x.eqTerm(b), CVC4ApiException);
-  ASSERT_THROW(f_x.eqTerm(x), CVC4ApiException);
-  ASSERT_THROW(f_x.eqTerm(f), CVC4ApiException);
-  ASSERT_THROW(f_x.eqTerm(p), CVC4ApiException);
+  ASSERT_THROW(f_x.eqTerm(b), CVC5ApiException);
+  ASSERT_THROW(f_x.eqTerm(x), CVC5ApiException);
+  ASSERT_THROW(f_x.eqTerm(f), CVC5ApiException);
+  ASSERT_THROW(f_x.eqTerm(p), CVC5ApiException);
   ASSERT_NO_THROW(f_x.eqTerm(zero));
   ASSERT_NO_THROW(f_x.eqTerm(f_x));
   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
-  ASSERT_THROW(sum.eqTerm(b), CVC4ApiException);
-  ASSERT_THROW(sum.eqTerm(x), CVC4ApiException);
-  ASSERT_THROW(sum.eqTerm(f), CVC4ApiException);
-  ASSERT_THROW(sum.eqTerm(p), CVC4ApiException);
+  ASSERT_THROW(sum.eqTerm(b), CVC5ApiException);
+  ASSERT_THROW(sum.eqTerm(x), CVC5ApiException);
+  ASSERT_THROW(sum.eqTerm(f), CVC5ApiException);
+  ASSERT_THROW(sum.eqTerm(p), CVC5ApiException);
   ASSERT_NO_THROW(sum.eqTerm(zero));
   ASSERT_NO_THROW(sum.eqTerm(f_x));
   ASSERT_NO_THROW(sum.eqTerm(sum));
   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
   ASSERT_NO_THROW(p_0.eqTerm(b));
-  ASSERT_THROW(p_0.eqTerm(x), CVC4ApiException);
-  ASSERT_THROW(p_0.eqTerm(f), CVC4ApiException);
-  ASSERT_THROW(p_0.eqTerm(p), CVC4ApiException);
-  ASSERT_THROW(p_0.eqTerm(zero), CVC4ApiException);
-  ASSERT_THROW(p_0.eqTerm(f_x), CVC4ApiException);
-  ASSERT_THROW(p_0.eqTerm(sum), CVC4ApiException);
+  ASSERT_THROW(p_0.eqTerm(x), CVC5ApiException);
+  ASSERT_THROW(p_0.eqTerm(f), CVC5ApiException);
+  ASSERT_THROW(p_0.eqTerm(p), CVC5ApiException);
+  ASSERT_THROW(p_0.eqTerm(zero), CVC5ApiException);
+  ASSERT_THROW(p_0.eqTerm(f_x), CVC5ApiException);
+  ASSERT_THROW(p_0.eqTerm(sum), CVC5ApiException);
   ASSERT_NO_THROW(p_0.eqTerm(p_0));
   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
   ASSERT_NO_THROW(p_f_x.eqTerm(b));
-  ASSERT_THROW(p_f_x.eqTerm(x), CVC4ApiException);
-  ASSERT_THROW(p_f_x.eqTerm(f), CVC4ApiException);
-  ASSERT_THROW(p_f_x.eqTerm(p), CVC4ApiException);
-  ASSERT_THROW(p_f_x.eqTerm(zero), CVC4ApiException);
-  ASSERT_THROW(p_f_x.eqTerm(f_x), CVC4ApiException);
-  ASSERT_THROW(p_f_x.eqTerm(sum), CVC4ApiException);
+  ASSERT_THROW(p_f_x.eqTerm(x), CVC5ApiException);
+  ASSERT_THROW(p_f_x.eqTerm(f), CVC5ApiException);
+  ASSERT_THROW(p_f_x.eqTerm(p), CVC5ApiException);
+  ASSERT_THROW(p_f_x.eqTerm(zero), CVC5ApiException);
+  ASSERT_THROW(p_f_x.eqTerm(f_x), CVC5ApiException);
+  ASSERT_THROW(p_f_x.eqTerm(sum), CVC5ApiException);
   ASSERT_NO_THROW(p_f_x.eqTerm(p_0));
   ASSERT_NO_THROW(p_f_x.eqTerm(p_f_x));
 }
@@ -522,59 +522,59 @@ TEST_F(TestApiBlackTerm, impTerm)
   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
   Term b = d_solver.mkTrue();
-  ASSERT_THROW(Term().impTerm(b), CVC4ApiException);
-  ASSERT_THROW(b.impTerm(Term()), CVC4ApiException);
+  ASSERT_THROW(Term().impTerm(b), CVC5ApiException);
+  ASSERT_THROW(b.impTerm(Term()), CVC5ApiException);
   ASSERT_NO_THROW(b.impTerm(b));
   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
-  ASSERT_THROW(x.impTerm(b), CVC4ApiException);
-  ASSERT_THROW(x.impTerm(x), CVC4ApiException);
+  ASSERT_THROW(x.impTerm(b), CVC5ApiException);
+  ASSERT_THROW(x.impTerm(x), CVC5ApiException);
   Term f = d_solver.mkVar(funSort1, "f");
-  ASSERT_THROW(f.impTerm(b), CVC4ApiException);
-  ASSERT_THROW(f.impTerm(x), CVC4ApiException);
-  ASSERT_THROW(f.impTerm(f), CVC4ApiException);
+  ASSERT_THROW(f.impTerm(b), CVC5ApiException);
+  ASSERT_THROW(f.impTerm(x), CVC5ApiException);
+  ASSERT_THROW(f.impTerm(f), CVC5ApiException);
   Term p = d_solver.mkVar(funSort2, "p");
-  ASSERT_THROW(p.impTerm(b), CVC4ApiException);
-  ASSERT_THROW(p.impTerm(x), CVC4ApiException);
-  ASSERT_THROW(p.impTerm(f), CVC4ApiException);
-  ASSERT_THROW(p.impTerm(p), CVC4ApiException);
+  ASSERT_THROW(p.impTerm(b), CVC5ApiException);
+  ASSERT_THROW(p.impTerm(x), CVC5ApiException);
+  ASSERT_THROW(p.impTerm(f), CVC5ApiException);
+  ASSERT_THROW(p.impTerm(p), CVC5ApiException);
   Term zero = d_solver.mkInteger(0);
-  ASSERT_THROW(zero.impTerm(b), CVC4ApiException);
-  ASSERT_THROW(zero.impTerm(x), CVC4ApiException);
-  ASSERT_THROW(zero.impTerm(f), CVC4ApiException);
-  ASSERT_THROW(zero.impTerm(p), CVC4ApiException);
-  ASSERT_THROW(zero.impTerm(zero), CVC4ApiException);
+  ASSERT_THROW(zero.impTerm(b), CVC5ApiException);
+  ASSERT_THROW(zero.impTerm(x), CVC5ApiException);
+  ASSERT_THROW(zero.impTerm(f), CVC5ApiException);
+  ASSERT_THROW(zero.impTerm(p), CVC5ApiException);
+  ASSERT_THROW(zero.impTerm(zero), CVC5ApiException);
   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  ASSERT_THROW(f_x.impTerm(b), CVC4ApiException);
-  ASSERT_THROW(f_x.impTerm(x), CVC4ApiException);
-  ASSERT_THROW(f_x.impTerm(f), CVC4ApiException);
-  ASSERT_THROW(f_x.impTerm(p), CVC4ApiException);
-  ASSERT_THROW(f_x.impTerm(zero), CVC4ApiException);
-  ASSERT_THROW(f_x.impTerm(f_x), CVC4ApiException);
+  ASSERT_THROW(f_x.impTerm(b), CVC5ApiException);
+  ASSERT_THROW(f_x.impTerm(x), CVC5ApiException);
+  ASSERT_THROW(f_x.impTerm(f), CVC5ApiException);
+  ASSERT_THROW(f_x.impTerm(p), CVC5ApiException);
+  ASSERT_THROW(f_x.impTerm(zero), CVC5ApiException);
+  ASSERT_THROW(f_x.impTerm(f_x), CVC5ApiException);
   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
-  ASSERT_THROW(sum.impTerm(b), CVC4ApiException);
-  ASSERT_THROW(sum.impTerm(x), CVC4ApiException);
-  ASSERT_THROW(sum.impTerm(f), CVC4ApiException);
-  ASSERT_THROW(sum.impTerm(p), CVC4ApiException);
-  ASSERT_THROW(sum.impTerm(zero), CVC4ApiException);
-  ASSERT_THROW(sum.impTerm(f_x), CVC4ApiException);
-  ASSERT_THROW(sum.impTerm(sum), CVC4ApiException);
+  ASSERT_THROW(sum.impTerm(b), CVC5ApiException);
+  ASSERT_THROW(sum.impTerm(x), CVC5ApiException);
+  ASSERT_THROW(sum.impTerm(f), CVC5ApiException);
+  ASSERT_THROW(sum.impTerm(p), CVC5ApiException);
+  ASSERT_THROW(sum.impTerm(zero), CVC5ApiException);
+  ASSERT_THROW(sum.impTerm(f_x), CVC5ApiException);
+  ASSERT_THROW(sum.impTerm(sum), CVC5ApiException);
   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
   ASSERT_NO_THROW(p_0.impTerm(b));
-  ASSERT_THROW(p_0.impTerm(x), CVC4ApiException);
-  ASSERT_THROW(p_0.impTerm(f), CVC4ApiException);
-  ASSERT_THROW(p_0.impTerm(p), CVC4ApiException);
-  ASSERT_THROW(p_0.impTerm(zero), CVC4ApiException);
-  ASSERT_THROW(p_0.impTerm(f_x), CVC4ApiException);
-  ASSERT_THROW(p_0.impTerm(sum), CVC4ApiException);
+  ASSERT_THROW(p_0.impTerm(x), CVC5ApiException);
+  ASSERT_THROW(p_0.impTerm(f), CVC5ApiException);
+  ASSERT_THROW(p_0.impTerm(p), CVC5ApiException);
+  ASSERT_THROW(p_0.impTerm(zero), CVC5ApiException);
+  ASSERT_THROW(p_0.impTerm(f_x), CVC5ApiException);
+  ASSERT_THROW(p_0.impTerm(sum), CVC5ApiException);
   ASSERT_NO_THROW(p_0.impTerm(p_0));
   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
   ASSERT_NO_THROW(p_f_x.impTerm(b));
-  ASSERT_THROW(p_f_x.impTerm(x), CVC4ApiException);
-  ASSERT_THROW(p_f_x.impTerm(f), CVC4ApiException);
-  ASSERT_THROW(p_f_x.impTerm(p), CVC4ApiException);
-  ASSERT_THROW(p_f_x.impTerm(zero), CVC4ApiException);
-  ASSERT_THROW(p_f_x.impTerm(f_x), CVC4ApiException);
-  ASSERT_THROW(p_f_x.impTerm(sum), CVC4ApiException);
+  ASSERT_THROW(p_f_x.impTerm(x), CVC5ApiException);
+  ASSERT_THROW(p_f_x.impTerm(f), CVC5ApiException);
+  ASSERT_THROW(p_f_x.impTerm(p), CVC5ApiException);
+  ASSERT_THROW(p_f_x.impTerm(zero), CVC5ApiException);
+  ASSERT_THROW(p_f_x.impTerm(f_x), CVC5ApiException);
+  ASSERT_THROW(p_f_x.impTerm(sum), CVC5ApiException);
   ASSERT_NO_THROW(p_f_x.impTerm(p_0));
   ASSERT_NO_THROW(p_f_x.impTerm(p_f_x));
 }
@@ -588,39 +588,39 @@ TEST_F(TestApiBlackTerm, iteTerm)
   Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
   Term b = d_solver.mkTrue();
-  ASSERT_THROW(Term().iteTerm(b, b), CVC4ApiException);
-  ASSERT_THROW(b.iteTerm(Term(), b), CVC4ApiException);
-  ASSERT_THROW(b.iteTerm(b, Term()), CVC4ApiException);
+  ASSERT_THROW(Term().iteTerm(b, b), CVC5ApiException);
+  ASSERT_THROW(b.iteTerm(Term(), b), CVC5ApiException);
+  ASSERT_THROW(b.iteTerm(b, Term()), CVC5ApiException);
   ASSERT_NO_THROW(b.iteTerm(b, b));
   Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   ASSERT_NO_THROW(b.iteTerm(x, x));
   ASSERT_NO_THROW(b.iteTerm(b, b));
-  ASSERT_THROW(b.iteTerm(x, b), CVC4ApiException);
-  ASSERT_THROW(x.iteTerm(x, x), CVC4ApiException);
-  ASSERT_THROW(x.iteTerm(x, b), CVC4ApiException);
+  ASSERT_THROW(b.iteTerm(x, b), CVC5ApiException);
+  ASSERT_THROW(x.iteTerm(x, x), CVC5ApiException);
+  ASSERT_THROW(x.iteTerm(x, b), CVC5ApiException);
   Term f = d_solver.mkVar(funSort1, "f");
-  ASSERT_THROW(f.iteTerm(b, b), CVC4ApiException);
-  ASSERT_THROW(x.iteTerm(b, x), CVC4ApiException);
+  ASSERT_THROW(f.iteTerm(b, b), CVC5ApiException);
+  ASSERT_THROW(x.iteTerm(b, x), CVC5ApiException);
   Term p = d_solver.mkVar(funSort2, "p");
-  ASSERT_THROW(p.iteTerm(b, b), CVC4ApiException);
-  ASSERT_THROW(p.iteTerm(x, b), CVC4ApiException);
+  ASSERT_THROW(p.iteTerm(b, b), CVC5ApiException);
+  ASSERT_THROW(p.iteTerm(x, b), CVC5ApiException);
   Term zero = d_solver.mkInteger(0);
-  ASSERT_THROW(zero.iteTerm(x, x), CVC4ApiException);
-  ASSERT_THROW(zero.iteTerm(x, b), CVC4ApiException);
+  ASSERT_THROW(zero.iteTerm(x, x), CVC5ApiException);
+  ASSERT_THROW(zero.iteTerm(x, b), CVC5ApiException);
   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
-  ASSERT_THROW(f_x.iteTerm(b, b), CVC4ApiException);
-  ASSERT_THROW(f_x.iteTerm(b, x), CVC4ApiException);
+  ASSERT_THROW(f_x.iteTerm(b, b), CVC5ApiException);
+  ASSERT_THROW(f_x.iteTerm(b, x), CVC5ApiException);
   Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
-  ASSERT_THROW(sum.iteTerm(x, x), CVC4ApiException);
-  ASSERT_THROW(sum.iteTerm(b, x), CVC4ApiException);
+  ASSERT_THROW(sum.iteTerm(x, x), CVC5ApiException);
+  ASSERT_THROW(sum.iteTerm(b, x), CVC5ApiException);
   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
   ASSERT_NO_THROW(p_0.iteTerm(b, b));
   ASSERT_NO_THROW(p_0.iteTerm(x, x));
-  ASSERT_THROW(p_0.iteTerm(x, b), CVC4ApiException);
+  ASSERT_THROW(p_0.iteTerm(x, b), CVC5ApiException);
   Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
   ASSERT_NO_THROW(p_f_x.iteTerm(b, b));
   ASSERT_NO_THROW(p_f_x.iteTerm(x, x));
-  ASSERT_THROW(p_f_x.iteTerm(x, b), CVC4ApiException);
+  ASSERT_THROW(p_f_x.iteTerm(x, b), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackTerm, termAssignment)
@@ -650,7 +650,7 @@ TEST_F(TestApiBlackTerm, termChildren)
   ASSERT_EQ(t1[0], two);
   ASSERT_EQ(t1.getNumChildren(), 2);
   Term tnull;
-  ASSERT_THROW(tnull.getNumChildren(), CVC4ApiException);
+  ASSERT_THROW(tnull.getNumChildren(), CVC5ApiException);
 
   // apply term f(2)
   Sort intSort = d_solver.getIntegerSort();
@@ -661,7 +661,7 @@ TEST_F(TestApiBlackTerm, termChildren)
   ASSERT_EQ(t2.getNumChildren(), 2);
   ASSERT_EQ(t2[0], f);
   ASSERT_EQ(t2[1], two);
-  ASSERT_THROW(tnull[0], CVC4ApiException);
+  ASSERT_THROW(tnull[0], CVC5ApiException);
 }
 
 TEST_F(TestApiBlackTerm, getInteger)
@@ -679,15 +679,15 @@ TEST_F(TestApiBlackTerm, getInteger)
   Term int11 = d_solver.mkInteger("18446744073709551616");
   Term int12 = d_solver.mkInteger("-0");
 
-  ASSERT_THROW(d_solver.mkInteger(""), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("-"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("-1-"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("0.0"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("-0.1"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("012"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("0000"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("-01"), CVC4ApiException);
-  ASSERT_THROW(d_solver.mkInteger("-00"), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkInteger(""), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("-"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("-1-"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("0.0"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("-0.1"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("012"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("0000"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("-01"), CVC5ApiException);
+  ASSERT_THROW(d_solver.mkInteger("-00"), CVC5ApiException);
 
   ASSERT_TRUE(!int1.isInt32() && !int1.isUInt32() && !int1.isInt64()
               && !int1.isUInt64() && int1.isInteger());
@@ -760,7 +760,7 @@ TEST_F(TestApiBlackTerm, substitute)
   ASSERT_EQ(xpx.substitute(x, one), onepone);
   ASSERT_EQ(onepone.substitute(one, x), xpx);
   // incorrect due to type
-  ASSERT_THROW(xpx.substitute(one, ttrue), CVC4ApiException);
+  ASSERT_THROW(xpx.substitute(one, ttrue), CVC5ApiException);
 
   // simultaneous substitution
   Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y");
@@ -776,28 +776,28 @@ TEST_F(TestApiBlackTerm, substitute)
 
   // incorrect substitution due to arity
   rs.pop_back();
-  ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException);
+  ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException);
 
   // incorrect substitution due to types
   rs.push_back(ttrue);
-  ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException);
+  ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException);
 
   // null cannot substitute
   Term tnull;
-  ASSERT_THROW(tnull.substitute(one, x), CVC4ApiException);
-  ASSERT_THROW(xpx.substitute(tnull, x), CVC4ApiException);
-  ASSERT_THROW(xpx.substitute(x, tnull), CVC4ApiException);
+  ASSERT_THROW(tnull.substitute(one, x), CVC5ApiException);
+  ASSERT_THROW(xpx.substitute(tnull, x), CVC5ApiException);
+  ASSERT_THROW(xpx.substitute(x, tnull), CVC5ApiException);
   rs.pop_back();
   rs.push_back(tnull);
-  ASSERT_THROW(xpy.substitute(es, rs), CVC4ApiException);
+  ASSERT_THROW(xpy.substitute(es, rs), CVC5ApiException);
   es.clear();
   rs.clear();
   es.push_back(x);
   rs.push_back(y);
-  ASSERT_THROW(tnull.substitute(es, rs), CVC4ApiException);
+  ASSERT_THROW(tnull.substitute(es, rs), CVC5ApiException);
   es.push_back(tnull);
   rs.push_back(one);
-  ASSERT_THROW(xpx.substitute(es, rs), CVC4ApiException);
+  ASSERT_THROW(xpx.substitute(es, rs), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackTerm, constArray)
@@ -810,7 +810,7 @@ TEST_F(TestApiBlackTerm, constArray)
 
   ASSERT_EQ(constarr.getKind(), CONST_ARRAY);
   ASSERT_EQ(constarr.getConstArrayBase(), one);
-  ASSERT_THROW(a.getConstArrayBase(), CVC4ApiException);
+  ASSERT_THROW(a.getConstArrayBase(), CVC5ApiException);
 
   arrsort =
       d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort());
@@ -837,7 +837,7 @@ TEST_F(TestApiBlackTerm, constSequenceElements)
   // A seq.unit app is not a constant sequence (regardless of whether it is
   // applied to a constant).
   Term su = d_solver.mkTerm(SEQ_UNIT, d_solver.mkReal(1));
-  ASSERT_THROW(su.getConstSequenceElements(), CVC4ApiException);
+  ASSERT_THROW(su.getConstSequenceElements(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackTerm, termScopedToString)
diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp
index 71ad2b1f4..8af29a8e4 100644
--- a/test/unit/main/interactive_shell_black.cpp
+++ b/test/unit/main/interactive_shell_black.cpp
@@ -39,7 +39,7 @@ class TestMainBlackInteractiveShell : public TestInternal
     d_sout.reset(new std::stringstream);
     d_options.set(options::in, d_sin.get());
     d_options.set(options::out, d_sout.get());
-    d_options.set(options::inputLanguage, language::input::LANG_CVC4);
+    d_options.set(options::inputLanguage, language::input::LANG_CVC);
     d_solver.reset(new cvc5::api::Solver(&d_options));
     d_symman.reset(new SymbolManager(d_solver.get()));
   }
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 94eb3ae83..2309c0ac7 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -623,7 +623,7 @@ TEST_F(TestNodeBlackNode, dagifier)
       OR, fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy);
 
   std::stringstream sstr;
-  sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC4);
+  sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC);
   sstr << Node::dag(false) << n;  // never dagify
   ASSERT_EQ(sstr.str(),
             "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = "
diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp
index 1e8e210ca..b6c433663 100644
--- a/test/unit/parser/parser_black.cpp
+++ b/test/unit/parser/parser_black.cpp
@@ -193,7 +193,7 @@ class TestParserBlackParser : public TestInternal
 class TestParserBlackCvCParser : public TestParserBlackParser
 {
  protected:
-  TestParserBlackCvCParser() : TestParserBlackParser(LANG_CVC4) {}
+  TestParserBlackCvCParser() : TestParserBlackParser(LANG_CVC) {}
 };
 
 TEST_F(TestParserBlackCvCParser, good_inputs)
diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp
index b8c12eee2..4ed036202 100644
--- a/test/unit/parser/parser_builder_black.cpp
+++ b/test/unit/parser/parser_builder_black.cpp
@@ -81,7 +81,7 @@ TEST_F(TestParseBlackParserBuilder, empty_file_input)
   ASSERT_NE(filename, nullptr);
 
   checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), filename)
-                      .withInputLanguage(LANG_CVC4));
+                      .withInputLanguage(LANG_CVC));
 
   remove(filename);
   free(filename);
@@ -96,7 +96,7 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input)
   fs.close();
 
   checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), filename)
-                     .withInputLanguage(LANG_CVC4));
+                     .withInputLanguage(LANG_CVC));
 
   remove(filename);
   free(filename);
@@ -105,14 +105,14 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input)
 TEST_F(TestParseBlackParserBuilder, empty_string_input)
 {
   checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), "foo")
-                      .withInputLanguage(LANG_CVC4)
+                      .withInputLanguage(LANG_CVC)
                       .withStringInput(""));
 }
 
 TEST_F(TestParseBlackParserBuilder, true_string_input)
 {
   checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), "foo")
-                     .withInputLanguage(LANG_CVC4)
+                     .withInputLanguage(LANG_CVC)
                      .withStringInput("TRUE"));
 }
 
@@ -120,7 +120,7 @@ TEST_F(TestParseBlackParserBuilder, empty_stream_input)
 {
   std::stringstream ss("", std::ios_base::in);
   checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), "foo")
-                      .withInputLanguage(LANG_CVC4)
+                      .withInputLanguage(LANG_CVC)
                       .withStreamInput(ss));
 }
 
@@ -128,7 +128,7 @@ TEST_F(TestParseBlackParserBuilder, true_stream_input)
 {
   std::stringstream ss("TRUE", std::ios_base::in);
   checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), "foo")
-                     .withInputLanguage(LANG_CVC4)
+                     .withInputLanguage(LANG_CVC)
                      .withStreamInput(ss));
 }
 
diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp
index d75e5881d..ccf26cbbd 100644
--- a/test/unit/theory/theory_sets_type_rules_white.cpp
+++ b/test/unit/theory/theory_sets_type_rules_white.cpp
@@ -53,7 +53,7 @@ TEST_F(TestTheoryWhiteSetsTypeRuleApi, singleton_term)
   //    (singleton (singleton_op Int) 1)
   //    (as emptyset (Set Real)))
   ASSERT_THROW(d_solver.mkTerm(UNION, singletonInt, emptyReal),
-               CVC4ApiException);
+               CVC5ApiException);
   // (union
   //    (singleton (singleton_op Real) 1)
   //    (as emptyset (Set Real)))
diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp
index 4a3afb281..1078a0e4e 100644
--- a/test/unit/util/boolean_simplification_black.cpp
+++ b/test/unit/util/boolean_simplification_black.cpp
@@ -72,7 +72,7 @@ class TestUtilBlackBooleanSimplification : public TestNode
     Assert(BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD >= 10);
 
     std::cout << expr::ExprSetDepth(-1)
-              << language::SetLanguage(language::output::LANG_CVC4);
+              << language::SetLanguage(language::output::LANG_CVC);
   }
 
   // assert equality up to commuting children
diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp
index 8e9595009..37937769c 100644
--- a/test/unit/util/output_black.cpp
+++ b/test/unit/util/output_black.cpp
@@ -69,7 +69,7 @@ TEST_F(TestUtilBlackOutput, output)
   Debug.on("foo");
   Debug("foo") << "testing3";
 
-  CVC4Message() << "a message";
+  CVC5Message() << "a message";
   Warning() << "bad warning!";
   Chat() << "chatty";
   Notice() << "note";
@@ -136,7 +136,7 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
   ASSERT_FALSE(Debug.isOn("foo"));
   ASSERT_FALSE(Trace.isOn("foo"));
   ASSERT_FALSE(Warning.isOn());
-  ASSERT_FALSE(CVC4Message.isOn());
+  ASSERT_FALSE(CVC5Message.isOn());
   ASSERT_FALSE(Notice.isOn());
   ASSERT_FALSE(Chat.isOn());
 
@@ -147,7 +147,7 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
   cout << "warning" << std::endl;
   Warning() << failure() << std::endl;
   cout << "message" << std::endl;
-  CVC4Message() << failure() << std::endl;
+  CVC5Message() << failure() << std::endl;
   cout << "notice" << std::endl;
   Notice() << failure() << std::endl;
   cout << "chat" << std::endl;
@@ -185,7 +185,7 @@ TEST_F(TestUtilBlackOutput, simple_print)
   ASSERT_EQ(d_chatStream.str(), std::string());
   d_chatStream.str("");
 
-  CVC4Message() << "baz foo";
+  CVC5Message() << "baz foo";
   ASSERT_EQ(d_messageStream.str(), std::string());
   d_messageStream.str("");
 
@@ -229,7 +229,7 @@ TEST_F(TestUtilBlackOutput, simple_print)
   ASSERT_EQ(d_chatStream.str(), std::string("baz foo"));
   d_chatStream.str("");
 
-  CVC4Message() << "baz foo";
+  CVC5Message() << "baz foo";
   ASSERT_EQ(d_messageStream.str(), std::string("baz foo"));
   d_messageStream.str("");
author	Aina Niemetz <aina.niemetz@gmail.com>	2021-04-15 13:04:55 -0700
committer	GitHub <noreply@github.com>	2021-04-15 20:04:55 +0000
commit	77bca094a140b35341257f125a55212ff0108250 (patch)
tree	1d3369b9be5fc4c3e8cb279ae5ea662e59cbcb3e /test
parent	63647b1d79df6f287ea6599958b16fce44b8271d (diff)