Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation.

1 files changed, 6 insertions, 2 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 39cde56e8..b26f24c63 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -621,8 +621,12 @@ bool InstStrategyCegqi::addLemma( Node lem ) {
 
 bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
   if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){
-    //only legal if current quantified formula contains n
-    return TermDb::containsTerm( d_curr_quant, n );
+    if( n.getKind()==SKOLEM && d_quantEngine->getTermDatabase()->containsVtsTerm( n ) ){
+      return true;
+    }else{
+      //only legal if current quantified formula contains n
+      return TermDb::containsTerm( d_curr_quant, n );
+    }
   }else{
     return true;
   }