6 files changed, 29 insertions, 24 deletions
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index da6b1bd58..f2596ceeb 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -19,9 +19,9 @@ find_package(ANTLR3 3.4 REQUIRED)
 find_package(Java COMPONENTS Runtime REQUIRED)
 
 #-----------------------------------------------------------------------------#
-# libcvc4parser source files
+# libcvc5parser source files
 
-set(libcvc4parser_src_files
+set(libcvc5parser_src_files
   antlr_input.cpp
   antlr_input.h
   antlr_input_imports.cpp
@@ -96,28 +96,28 @@ foreach(lang Cvc Smt2 Tptp)
     ${gen_src_files} PROPERTIES COMPILE_FLAGS "-Wno-all -Wno-error")
 
   # Add generated source files to the parser source files
-  list(APPEND libcvc4parser_src_files ${gen_src_files})
+  list(APPEND libcvc5parser_src_files ${gen_src_files})
 endforeach()
 
 #-----------------------------------------------------------------------------#
-# libcvc4parser configuration
+# libcvc5parser configuration
 
-add_library(cvc4parser ${libcvc4parser_src_files})
-set_target_properties(cvc4parser PROPERTIES SOVERSION ${CVC5_SOVERSION})
-target_compile_definitions(cvc4parser PRIVATE -D__BUILDING_CVC4PARSERLIB)
-target_link_libraries(cvc4parser PUBLIC cvc4)
-target_link_libraries(cvc4parser PRIVATE ANTLR3)
+add_library(cvc5parser ${libcvc5parser_src_files})
+set_target_properties(cvc5parser PROPERTIES SOVERSION ${CVC5_SOVERSION})
+target_compile_definitions(cvc5parser PRIVATE -D__BUILDING_CVC5PARSERLIB)
+target_link_libraries(cvc5parser PUBLIC cvc5)
+target_link_libraries(cvc5parser PRIVATE ANTLR3)
 
-install(TARGETS cvc4parser
-  EXPORT cvc4-targets
+install(TARGETS cvc5parser
+  EXPORT cvc5-targets
   DESTINATION ${CMAKE_INSTALL_LIBDIR})
 
 # The generated lexer/parser files define some functions as
 # __declspec(dllexport) via the ANTLR3_API macro, which leads to lots of
-# unresolved symbols when linking against libcvc4parser.
+# unresolved symbols when linking against libcvc5parser.
 # -Wl,--export-all-symbols makes sure that all symbols are exported when
 # building a DLL.
 if(CVC5_WINDOWS_BUILD)
-  set_target_properties(cvc4parser
+  set_target_properties(cvc5parser
     PROPERTIES LINK_FLAGS "-Wl,--export-all-symbols")
 endif()
diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h
index 595a2d784..e9d1d0758 100644
--- a/src/parser/antlr_tracing.h
+++ b/src/parser/antlr_tracing.h
@@ -44,7 +44,8 @@
  */
 
 /** A "System" object, just like in Java! */
-static struct __Cvc4System {
+static struct __Cvc5System
+{
   /**
    * Helper class just to handle arbitrary string concatenation
    * with Java syntax.  In C++ you cannot do "char*" + "char*",
@@ -76,7 +77,11 @@ static struct __Cvc4System {
 // These are highly dependent on the bugs in a particular ANTLR release.
 // These seem to work with ANTLR 3.3 as of 4/23/2011.  A different trick
 // works with ANTLR 3.2.  EXPECT LOTS OF COMPILER WARNINGS.
-#define println(x) println(({int failed=0;__Cvc4System::JavaPrinter()+x;}))
+#define println(x)                   \
+  println(({                         \
+    int failed = 0;                  \
+    __Cvc5System::JavaPrinter() + x; \
+  }))
 #undef ANTLR3_FPRINTF
 #define ANTLR3_FPRINTF(args...) {int failed=0;fprintf(args);}
 #undef ANTLR3_PRINTF
diff --git a/src/parser/input.h b/src/parser/input.h
index fb7ce2b40..47453e367 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -25,7 +25,7 @@
 #include <vector>
 
 #include "api/cpp/cvc5.h"
-#include "cvc4_export.h"
+#include "cvc5_export.h"
 #include "options/language.h"
 #include "parser/parser_exception.h"
 
@@ -78,7 +78,7 @@ class Parser;
  * for the given input language and attach it to an input source of the
  * appropriate type.
  */
-class CVC4_EXPORT Input
+class CVC5_EXPORT Input
 {
   friend class Parser; // for parseError, parseCommand, parseExpr
   friend class ParserBuilder;
diff --git a/src/parser/parser.h b/src/parser/parser.h
index da35606c1..42baf98cd 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -23,7 +23,7 @@
 #include <string>
 
 #include "api/cpp/cvc5.h"
-#include "cvc4_export.h"
+#include "cvc5_export.h"
 #include "expr/kind.h"
 #include "expr/symbol_manager.h"
 #include "expr/symbol_table.h"
@@ -101,7 +101,7 @@ inline std::ostream& operator<<(std::ostream& out, SymbolType type) {
  * name of the file, line number and column information, and in-scope
  * declarations.
  */
-class CVC4_EXPORT Parser
+class CVC5_EXPORT Parser
 {
   friend class ParserBuilder;
 private:
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index b0f9e35e6..5d73fedfa 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -20,7 +20,7 @@
 
 #include <string>
 
-#include "cvc4_export.h"
+#include "cvc5_export.h"
 #include "options/language.h"
 #include "parser/input.h"
 
@@ -42,7 +42,7 @@ class Parser;
  * called any number of times on an instance and will generate a fresh
  * parser each time.
  */
-class CVC4_EXPORT ParserBuilder
+class CVC5_EXPORT ParserBuilder
 {
   enum InputType {
     FILE_INPUT,
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index 0372661a2..124013183 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -19,16 +19,16 @@
 #define CVC5__PARSER__PARSER_EXCEPTION_H
 
 #include <iostream>
-#include <string>
 #include <sstream>
+#include <string>
 
 #include "base/exception.h"
-#include "cvc4_export.h"
+#include "cvc5_export.h"
 
 namespace cvc5 {
 namespace parser {
 
-class CVC4_EXPORT ParserException : public Exception
+class CVC5_EXPORT ParserException : public Exception
 {
  public:
   // Constructors