diff options
| author | Guy <katz911@gmail.com> | 2016-06-20 10:17:04 -0700 |
|---|---|---|
| committer | Guy <katz911@gmail.com> | 2016-06-20 10:17:04 -0700 |
| commit | 4b8972fec229012812bb7edc9e315c2e54f7c059 (patch) | |
| tree | 930d63632dc3eb3e945967dee4e442b76c26ee3a /src/smt/smt_engine.cpp | |
| parent | 150863561376c8cb7b170793f693352eab582ba9 (diff) | |
| parent | dc27675a9b9aa0346122390afdb28280f4495e9c (diff) | |
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d5874c52f..69a150cc9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -94,6 +94,7 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/sort_inference.h" #include "theory/strings/theory_strings.h" +#include "theory/sep/theory_sep.h" #include "theory/substitutions.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" @@ -1844,8 +1845,8 @@ void SmtEngine::setDefaults() { } } //counterexample-guided instantiation for non-sygus - // enable if any quantifiers with arithmetic or datatypes - if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) ) ) || + // enable if any possible quantifiers with arithmetic, datatypes or bitvectors + if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) || options::cbqiAll() ){ if( !options::cbqi.wasSetByUser() ){ options::cbqi.set( true ); @@ -3985,6 +3986,10 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl; dumpAssertions("post-strings-pp", d_assertions); } + if( d_smt.d_logic.isTheoryEnabled(THEORY_SEP) ) { + //separation logic solver needs to register the entire input + ((theory::sep::TheorySep*)d_smt.d_theoryEngine->theoryOf(THEORY_SEP))->processAssertions( d_assertions.ref() ); + } if( d_smt.d_logic.isQuantified() ){ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl; //remove rewrite rules |