diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-18 22:33:22 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-01-18 22:33:22 +0100 |
commit | 4d3e24e52765b03d8e6f36afe7de6168e8740693 (patch) | |
tree | c5b3e7230e56db21cef630bbc95d94b7e3476618 /src/theory/theory_model.cpp | |
parent | 9d677333439c15677b6891ee8f6bd368a5df9f0a (diff) |
Bug fix rewriter for fun defs.
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 5ddb1c31a..2a8e21059 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -591,6 +591,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if( options::finiteModelFind() ){ tep.d_fixed_usort_card = true; for( std::map< TypeNode, unsigned >::iterator it = eqc_usort_count.begin(); it != eqc_usort_count.end(); ++it ){ + Trace("model-builder") << "Fixed bound (#eqc) for " << it->first << " : " << it->second << std::endl; tep.d_fixed_card[it->first] = Integer(it->second); } typeConstSet.setTypeEnumeratorProperties( &tep ); |