From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 9 Mar 2020 22:44:39 +0000 (-0500)
Subject: Eliminate spurious assertion (#3976)
X-Git-Tag: cvc5-1.0.0~3541
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7ccbc8647811439112951e20d0ec9e4b8448d1de;p=cvc5.git

Eliminate spurious assertion (#3976)
---

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 34e66da9e..0dc8f262e 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -478,7 +478,6 @@ void CegInstantiator::activateInstantiationVariable(Node v, unsigned index)
     if( tn.isReal() ){
       vinst = new ArithInstantiator(tn, d_parent->getVtsTermCache());
     }else if( tn.isSort() ){
-      Assert(options::quantEpr());
       vinst = new EprInstantiator(tn);
     }else if( tn.isDatatype() ){
       vinst = new DtInstantiator(tn);