diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 334879993..c9aef9828 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1899,11 +1899,11 @@ void SmtEngine::setDefaults() { } //counterexample-guided instantiation for non-sygus // 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) - || d_logic.isTheoryEnabled(THEORY_FP)) + if ((d_logic.isQuantified() + && (d_logic.isTheoryEnabled(THEORY_ARITH) + || d_logic.isTheoryEnabled(THEORY_DATATYPES) + || d_logic.isTheoryEnabled(THEORY_BV) + || d_logic.isTheoryEnabled(THEORY_FP))) || options::cbqiAll()) { if( !options::cbqi.wasSetByUser() ){ |