From b9308b9b9cf07b02318d772a508781971603be2c Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 24 Jan 2022 20:01:13 -0800
Subject: [PATCH] [Strings] Remove redundant call to rewriter (#7978)

The term being rewritten was already rewritten a couple of lines above.
---
 src/theory/strings/inference_manager.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index c7020869f..b12833b05 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -243,7 +243,6 @@ bool InferenceManager::sendSplit(Node a, Node b, InferenceId infer, bool preq)
   InferInfo iiSplit(infer);
   iiSplit.d_sim = this;
   iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq));
-  eq = rewrite(eq);
   addPendingPhaseRequirement(eq, preq);
   addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSplit)));
   return true;
-- 
2.30.2