diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
| commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
| tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /src/theory/quantifiers_engine.cpp | |
| parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) | |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e399af71d..686843189 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -250,7 +250,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; if( options::quantEpr() ){ - Assert( !options::incrementalSolving() ); + Assert(!options::incrementalSolving()); d_qepr.reset(new quantifiers::QuantEPR); } //---- end utilities @@ -660,7 +660,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ return; }else{ //should only fail reset if added a lemma - Assert( false ); + Assert(false); } } } @@ -742,7 +742,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_hasAddedLemma ){ break; }else{ - Assert( !d_conflict ); + Assert(!d_conflict); if (quant_e == QuantifiersModule::QEFFORT_CONFLICT) { if( e==Theory::EFFORT_FULL ){ @@ -812,7 +812,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ setIncomplete = true; break; }else{ - Assert( qmd!=NULL ); + Assert(qmd != NULL); Trace("quant-engine-debug2") << "Complete for " << q << " due to " << qmd->identify().c_str() << std::endl; } } @@ -899,7 +899,7 @@ void QuantifiersEngine::registerQuantifierInternal(Node f) Trace("quant") << " : " << f << std::endl; unsigned prev_lemma_waiting = d_lemmas_waiting.size(); ++(d_statistics.d_num_quant); - Assert( f.getKind()==FORALL ); + Assert(f.getKind() == FORALL); // register with utilities for (unsigned i = 0; i < d_util.size(); i++) { |