diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-10-08 20:16:57 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-08 20:16:57 -0700 |
commit | f0340df210f2bb2a0a5fd95e0d9e6a8548cf1fc7 (patch) | |
tree | e29569290d9df29739b4391ef326fa9a8bdf507b | |
parent | 0d310d6716d1ab679cd466a2e47e5c0f6cdd8569 (diff) |
Fix compiler warnings. (#2601)
-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() ){ |