diff options
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 180ccc448..5eca87903 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -118,14 +118,9 @@ Node InstMatch::get( int i ) { return d_vals[i]; } -void InstMatch::getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst ){ +void InstMatch::getTerms( Node f, std::vector< Node >& inst ){ for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - Node val = get( i ); - if( val.isNull() ){ - Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i ); - val = qe->getTermDatabase()->getModelBasisTerm( ic.getType() ); - } - inst.push_back( val ); + inst.push_back( d_vals[i] ); } } |