From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 26 Jun 2018 17:58:25 +0000 (-0500)
Subject: Remove unnecessary code in register quantifier internal (#2092)
X-Git-Tag: cvc5-1.0.0~4947
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a29329e74e79dc89bfe849d6cbd6ac6720c9e94b;p=cvc5.git

Remove unnecessary code in register quantifier internal (#2092)
---

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 1fa3514c8..37f11f9cd 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -799,8 +799,6 @@ void QuantifiersEngine::registerQuantifierInternal(Node f)
       // this call
       Assert(d_lemmas_waiting.size() == prev_lemma_waiting);
     }
-    // TODO (#2020): remove this
-    Node ceBody = d_term_util->getInstConstantBody(f);
     Trace("quant-debug") << "...finish." << std::endl;
     d_quants[f] = true;
     AlwaysAssert(d_lemmas_waiting.size() == prev_lemma_waiting);