From 9c960866c9e71e543c5688aac826a8150c899ca6 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 19 Mar 2020 01:01:05 -0500
Subject: 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).
---
 src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 2 --
 1 file changed, 2 deletions(-)

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());
             }
           }
         }
-- 
cgit v1.2.3