Fix debug

3 files changed, 1 insertions, 24 deletions

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index c24a8806b..032409dae 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1047,8 +1047,6 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       {
         // can infer that this string must be empty
         Node eq = nfkv[index_k].eqNode(d_emptyString);
-        // Trace("strings-lemma") << "Strings: Infer " << eq << " from " <<
-        // eq_exp << std::endl;
         Assert(!d_state.areEqual(d_emptyString, nfkv[index_k]));
         d_im.sendInference(curr_exp, eq, "N_EndpointEmp");
         index_k++;
@@ -1320,7 +1318,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
           size_t cIndex = index;
           Node constStr = TheoryStringsRewriter::collectConstantStringAt(
               nfcv, cIndex, false);
-          Assert(!const_str.isNull());
+          Assert(!constStr.isNull());
           CVC4::String stra = constStr.getConst<String>();
           CVC4::String strb = nextConstStr.getConst<String>();
           // Since `nc` is non-empty, we start with character 1
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 174661ac8..0016e5658 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -3496,23 +3496,6 @@ bool TheoryStringsRewriter::canConstantContainList( Node c, std::vector< Node >&
   return true;
 }
 
-Node TheoryStringsRewriter::getNextConstantAt(const std::vector<Node>& vec,
-                                              size_t& start_index,
-                                              size_t& end_index,
-                                              bool isRev)
-{
-  while( vec.size()>start_index && !vec[ start_index ].isConst() ){
-    //return Node::null();
-    start_index++;
-  }
-  if( start_index<vec.size() ){    
-    end_index = start_index;
-    return collectConstantStringAt( vec, end_index, isRev );
-  }else{
-    return Node::null();
-  }
-}
-
 Node TheoryStringsRewriter::collectConstantStringAt(
     const std::vector<Node>& vec, size_t& end_index, bool isRev)
 {
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 1557e9d77..8bef8c110 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -283,10 +283,6 @@ class TheoryStringsRewriter : public TheoryRewriter
   * same as above but with n = str.++( l ) instead of l
   */
   static bool canConstantContainConcat(Node c, Node n, int& firstc, int& lastc);
-  static Node getNextConstantAt(const std::vector<Node>& vec,
-                                size_t& start_index,
-                                size_t& end_index,
-                                bool isRev);
   static Node collectConstantStringAt(const std::vector<Node>& vec,
                                       size_t& end_index,
                                       bool isRev);