diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-23 14:03:49 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-23 14:03:57 +0200 |
| commit | 2064e455674aab26e3632da31998bda8b3fff5f9 (patch) | |
| tree | 524988e058f1fd4c3e79ed5ea73b3f805c6dd42a /src/theory/quantifiers_engine.cpp | |
| parent | 49747c4574eec3cfa192ffb6e6a2451b949e8b3e (diff) | |
Do not throw error when codatatype is not well-founded. Add option for disabling codatatype reasoning. Minor cleanup.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 4855083a8..c1ad62cd9 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -186,6 +186,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } Trace("quant-engine-debug") << std::endl; Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl; + Trace("quant-engine-debug") << " Theory engine finished : " << !d_te->needCheck() << std::endl; if( !getMasterEqualityEngine()->consistent() ){ Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl; @@ -229,7 +230,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl; for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_MODEL; quant_e++ ){ for( int i=0; i<(int)qm.size(); i++ ){ - Trace("quant-engine-debug") << "Check " << d_modules[i]->identify().c_str() << "..." << std::endl; + Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl; qm[i]->check( e, quant_e ); } //flush all current lemmas |