diff options
Diffstat (limited to 'src/theory/quantifiers/equality_query.cpp')
| -rw-r--r-- | src/theory/quantifiers/equality_query.cpp | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index c60c98d70..def27fe5a 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -172,11 +172,6 @@ int EqualityQueryQuantifiersEngine::getRepScore(Node n, return -2; }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type return -2; - } - else if (options::lteRestrictInstClosure() - && (!d_tdb->isInstClosure(n) || !d_tdb->hasTermCurrent(n, false))) - { - return -1; }else if( options::instMaxLevel()!=-1 ){ //score prefer lowest instantiation level if( n.hasAttribute(InstLevelAttribute()) ){ |