From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 23 Oct 2021 01:27:14 +0000 (-0500)
Subject: Remove spurious assertoin (#7458)
X-Git-Tag: cvc5-1.0.0~991
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f493ea93e925e3ad9bfe0036e1d876d5600d5b30;p=cvc5.git

Remove spurious assertoin (#7458)

Fixes #7439. That benchmark is now "unknown".
---

diff --git a/src/theory/quantifiers/entailment_check.cpp b/src/theory/quantifiers/entailment_check.cpp
index 543414a4e..bdbad9405 100644
--- a/src/theory/quantifiers/entailment_check.cpp
+++ b/src/theory/quantifiers/entailment_check.cpp
@@ -60,7 +60,6 @@ Node EntailmentCheck::evaluateTerm2(TNode n,
     {
       if (!subsRep)
       {
-        Assert(d_qstate.hasTerm(it->second));
         ret = d_qstate.getRepresentative(it->second);
       }
       else