From f493ea93e925e3ad9bfe0036e1d876d5600d5b30 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 22 Oct 2021 20:27:14 -0500
Subject: [PATCH] Remove spurious assertoin (#7458)

Fixes #7439. That benchmark is now "unknown".
---
 src/theory/quantifiers/entailment_check.cpp | 1 -
 1 file changed, 1 deletion(-)

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
-- 
2.30.2