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.

3 files changed, 14 insertions, 14 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;