From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 19 Mar 2020 06:01:05 +0000 (-0500)
Subject: Remove spurious assertion (#4117)
X-Git-Tag: cvc5-1.0.0~3476
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9c960866c9e71e543c5688aac826a8150c899ca6;p=cvc5.git

Remove spurious assertion (#4117)

Fixes #4106.

The assertion was the wrong polarity (should have been Assert(options::cbqiAll()); but regardless is no longer an invariant of CEGQI).
---

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index dafcc365e..8273f2c91 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -134,8 +134,6 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
               }else{
                 Assert(false);
               }                  
-            }else{
-              Assert(!options::cbqiAll());
             }
           }
         }