1 files changed, 9 insertions, 10 deletions
diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index 1caae9b5e..67554525a 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -18,16 +18,15 @@
 #include "theory/bv/theory_bv_utils.h"
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
-using namespace CVC4::theory::bv::utils;
-
-const TermId CVC4::theory::bv::UndefinedTermId = -1; 
-const ReasonId CVC4::theory::bv::UndefinedReasonId = -1;
-const ReasonId CVC4::theory::bv::AxiomReasonId = -2;
-
+using namespace CVC5;
+using namespace CVC5::context;
+using namespace CVC5::theory;
+using namespace CVC5::theory::bv;
+using namespace CVC5::theory::bv::utils;
+
+const TermId CVC5::theory::bv::UndefinedTermId = -1;
+const ReasonId CVC5::theory::bv::UndefinedReasonId = -1;
+const ReasonId CVC5::theory::bv::AxiomReasonId = -2;
 
 bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) {
   Debug("bv-inequality") << "InequalityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n";