Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring of term database, other refactoring. Bug fixes for cbqi+datatypes.

1 files changed, 1 insertions, 3 deletions

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 47c2e1c5b..b7d82bc9e 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -458,9 +458,7 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node
     //check constraints
     for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
       //apply substitution to the tconstraint
-      Node cons = it->first.substitute( p->getTermDatabase()->d_vars[d_q].begin(),
-                                        p->getTermDatabase()->d_vars[d_q].end(),
-                                        terms.begin(), terms.end() );
+      Node cons = p->getTermDatabase()->getInstantiatedNode( it->first, d_q, terms );
       cons = it->second ? cons : cons.negate();
       if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){
         return true;