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

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 896cf5dff..1cdad589b 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1722,8 +1722,8 @@ void TermGenEnv::collectSignatureInformation() {
   d_func_args.clear();
   TypeNode tnull;
   for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){
-    if( !getTermDatabase()->d_op_map[it->first].empty() ){
-      Node nn = getTermDatabase()->d_op_map[it->first][0];
+    if( getTermDatabase()->getNumGroundTerms( it->first )>0 ){
+      Node nn = getTermDatabase()->getGroundTerm( it->first, 0 );
       Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl;
       if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){
         bool do_enum = true;