1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 6b7fc699b..96e143244 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -77,7 +77,8 @@ TheoryModel* SolverState::getModel() { return d_valuation.getModel(); }
 Node SolverState::getLengthExp(Node t, std::vector<Node>& exp, Node te)
 {
   Assert(areEqual(t, te));
-  Node lt = utils::mkNLength(te);
+  Node lt = NodeManager::currentNM()->mkNode(STRING_LENGTH, t);
+  lt = rewrite(lt);
   if (hasTerm(lt))
   {
     // use own length if it exists, leads to shorter explanation
@@ -116,7 +117,8 @@ Node SolverState::explainNonEmpty(Node s)
   {
     return s.eqNode(emp).negate();
   }
-  Node sLen = utils::mkNLength(s);
+  Node sLen = NodeManager::currentNM()->mkNode(STRING_LENGTH, s);
+  sLen = rewrite(sLen);
   if (areDisequal(sLen, d_zero))
   {
     return sLen.eqNode(d_zero).negate();