diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-24 16:56:23 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-24 16:56:41 -0500 |
| commit | 21ac21a2ff3ba3eeac4deabf0c4b79ca4cc8df77 (patch) | |
| tree | ec0f4edcec8ed1c89db9c917a0136b5199021696 /src/theory/quantifiers/ambqi_builder.cpp | |
| parent | bcfe5eed9c79e7bd3c32b5ce8e96a54bcff4099f (diff) | |
Fixes and simplifications for fmf mbqi.
Diffstat (limited to 'src/theory/quantifiers/ambqi_builder.cpp')
| -rw-r--r-- | src/theory/quantifiers/ambqi_builder.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index de55ecdba..bc638080f 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -774,10 +774,9 @@ bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) { if( itut!=fm->d_uf_terms.end() ){ for( size_t i=0; i<itut->second.size(); i++ ){ Node n = itut->second[i]; - if( d_qe->getTermDatabase()->isTermActive( n ) ){ - Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl; - fapps.push_back( n ); - } + // only consider unique up to congruence (in model equality engine)? + Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl; + fapps.push_back( n ); } } if( fapps.empty() ){ |