diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 1166ef9966b..6d83aac85b5 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -228,6 +228,23 @@ void InferProofCons::convert(InferenceId infer,
         {
           useBuffer = true;
         }
+        else
+        {
+          // More aggressive: lift to original form and use extended rewriting.
+          // A common case that this covers is arithmetic bound conflicts like
+          // (= (str.len @purifyN) 5) where @purifyN is the purification skolem
+          // for (str.++ "ABCDEF" x).
+          Node psrco = SkolemManager::getOriginalForm(psrc);
+          if (psb.applyPredTransform(psrco,
+                                     conc,
+                                     exps,
+                                     MethodId::SB_DEFAULT,
+                                     MethodId::SBA_SEQUENTIAL,
+                                     MethodId::RW_EXT_REWRITE))
+          {
+            useBuffer = psb.applyPredTransform(psrc, psrco, {});
+          }
+        }
       }
       else
       {