projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 6d10b46)
Remove spurious assertoin (#7458)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 23 Oct 2021 01:27:14 +0000 (20:27 -0500)
committerGitHub <noreply@github.com>
Sat, 23 Oct 2021 01:27:14 +0000 (01:27 +0000)
Fixes #7439. That benchmark is now "unknown".

src/theory/quantifiers/entailment_check.cpp patch | blob | history

diff --git a/src/theory/quantifiers/entailment_check.cpp b/src/theory/quantifiers/entailment_check.cpp
index 543414a4e8dd3ff88eae145308dcf440b20c749a..bdbad940561bf1ef6a76c784b549dd00c7309c49 100644 (file)
--- 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