1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 614a5e6e0..898c0f1b7 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -546,7 +546,10 @@ bool RegExpSolver::checkPDerivative(
       {
         std::vector<Node> noExplain;
         noExplain.push_back(atom);
-        noExplain.push_back(x.eqNode(d_emptyString));
+        if (x != d_emptyString)
+        {
+          noExplain.push_back(x.eqNode(d_emptyString));
+        }
         std::vector<Node> iexp = nf_exp;
         iexp.insert(iexp.end(), noExplain.begin(), noExplain.end());
         d_im.sendInference(iexp, noExplain, d_false, InferenceId::STRINGS_RE_DELTA_CONF);