diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-11 10:54:32 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-11 10:54:32 +0100 |
commit | 97470da31e14104f807fb33b2b3423e583e10726 (patch) | |
tree | 516e79d981cfaa0c59c6b51981ebb2fcd4c1a698 /src/theory/quantifiers/inst_strategy_cbqi.cpp | |
parent | 81dca680f6c88d10b56a0ed065d470d907766e21 (diff) |
Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation.
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 8 |
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; } |