diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-13 13:36:28 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-13 13:36:28 -0500 |
| commit | 5887766342258361d3635a5b29a015dadb9ebe83 (patch) | |
| tree | 04a9ce1bceb5e5c4d0a715eda0ca9689ac424c58 /src/theory/quantifiers_engine.cpp | |
| parent | ca1b17c8bba3681643a1a3de19d32b038c38aceb (diff) | |
Minor changes to sep logic, epr, quantifier splitting.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index dc3f0cdd5..5b50526c4 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -349,7 +349,7 @@ void QuantifiersEngine::presolve() { } void QuantifiersEngine::ppNotifyAssertions( std::vector< Node >& assertions ) { - Trace("quant-engine-proc") << "ppNotifyAssertions in QE" << std::endl; + Trace("quant-engine-proc") << "ppNotifyAssertions in QE, #assertions = " << assertions.size() << " check epr = " << (d_qepr!=NULL) << std::endl; if( ( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ) || d_qepr!=NULL ){ for( unsigned i=0; i<assertions.size(); i++ ) { if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){ |