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 dafcc365ed5f7b7f4d23855045a9dad33a5d640e..8273f2c9121be1bcb00f0b62f939e5cc574d84b2 100644 (file)
--- 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());
             }
           }
         }