diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-18 18:44:48 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-18 18:44:48 +0100 |
commit | ba02a5247204abc3b6d38a61f5f7d31f23e765ac (patch) | |
tree | 770de1e338ace6ae0889fb557f4617c00c639894 /src/theory/quantifiers/term_database.cpp | |
parent | 3a2aed30267a33ff78006aec6a5b36aad96feb09 (diff) |
Compute model basis only for fmf. Add another co-datatype regression.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5dc8bb384..a95de086a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -398,9 +398,11 @@ void TermDb::reset( Theory::Effort effort ){ if( !it->second.empty() ){ for( unsigned i=0; i<it->second.size(); i++ ){ Node n = it->second[i]; - computeModelBasisArgAttribute( n ); if( hasTermCurrent( n ) ){ if( !n.getAttribute(NoMatchAttribute()) ){ + if( options::finiteModelFind() ){ + computeModelBasisArgAttribute( n ); + } computeArgReps( n ); if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){ NoMatchAttribute nma; |