projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 92fad93)
Eliminate spurious assertion (#3976)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 9 Mar 2020 22:44:39 +0000 (17:44 -0500)
committerGitHub <noreply@github.com>
Mon, 9 Mar 2020 22:44:39 +0000 (15:44 -0700)
src/theory/quantifiers/cegqi/ceg_instantiator.cpp patch | blob | history

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 34e66da9ea7c946c952c20e5d6508401ca001022..0dc8f262eb9da8d7227417c9399ff83e36a84ee0 100644 (file)
--- 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);