From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 25 Jan 2022 04:01:13 +0000 (-0800)
Subject: [Strings] Remove redundant call to rewriter (#7978)
X-Git-Tag: cvc5-1.0.0~510
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b9308b9b9cf07b02318d772a508781971603be2c;p=cvc5.git

[Strings] Remove redundant call to rewriter (#7978)

The term being rewritten was already rewritten a couple of lines above.
---

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;