1 files changed, 32 insertions, 0 deletions
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 06a86935f..41c07f5cf 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -127,6 +127,14 @@ void SolverState::eqNotifyNewClass(TNode t)
   {
     addEndpointsToEqcInfo(t, t, t);
   }
+  else if (k == STRING_SUBSTR)
+  {
+    if (t[1].isConst() && t[1].getConst<Rational>().isZero() && t[2].isConst())
+    {
+      EqcInfo* ei = getOrMakeEqcInfo(t);
+      ei->d_prefixes.push_back(t);
+    }
+  }
 }
 
 void SolverState::eqNotifyPreMerge(TNode t1, TNode t2)
@@ -162,6 +170,30 @@ void SolverState::eqNotifyPreMerge(TNode t1, TNode t2)
     {
       e1->d_normalizedLength.set(e2->d_normalizedLength);
     }
+
+    if (t1.isConst())
+    {
+      for (const Node& prefix : e2->d_prefixes)
+      {
+        EqcInfo* e3 = getOrMakeEqcInfo(prefix[0]);
+        setPendingConflictWhen(e3->addEndpointConst(t1.eqNode(t2), Node::null(), false));
+      }
+    }
+    else if (t2.isConst())
+    {
+      for (const Node& prefix : e1->d_prefixes)
+      {
+        EqcInfo* e3 = getOrMakeEqcInfo(prefix[0]);
+        setPendingConflictWhen(e3->addEndpointConst(t1.eqNode(t2), Node::null(), false));
+      }
+    }
+    else
+    {
+      for (const Node& prefix : e2->d_prefixes)
+      {
+        e1->d_prefixes.push_back(prefix);
+      }
+    }
   }
 }