diff options
| -rw-r--r-- | src/api/cvc4cpp.cpp | 2 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 10 |
2 files changed, 7 insertions, 5 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index c8248d803..be7c5c665 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -544,10 +544,12 @@ namespace { bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; } +#ifdef CVC4_ASSERTIONS bool isDefinedIntKind(CVC4::Kind k) { return k != CVC4::Kind::UNDEFINED_KIND && k != CVC4::Kind::LAST_KIND; } +#endif Kind intToExtKind(CVC4::Kind k) { 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() ){ |