diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-07 17:38:53 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-07 17:38:59 +0100 |
commit | 4ad0191e20e4d812d9a5dc3a733153cb10f6d728 (patch) | |
tree | f25fa219a0d464ca7a30b40d27fa45b05ff33638 /src/smt | |
parent | 3a3a57583fd8bd4af5c3b99b0047c9b20de38bb1 (diff) |
Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor improvement to performance of E-matching.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 577fa7413..c59d87d40 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1358,7 +1358,11 @@ void SmtEngine::setDefaults() { options::finiteModelFind.set( true ); } } - + if( options::finiteModelFind() ){ + if( !options::quantConflictFind.wasSetByUser() ){ + options::quantConflictFind.set( false ); + } + } //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){ |