From f0340df210f2bb2a0a5fd95e0d9e6a8548cf1fc7 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 8 Oct 2018 20:16:57 -0700 Subject: [PATCH] Fix compiler warnings. (#2601) --- src/api/cvc4cpp.cpp | 2 ++ 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() ){ -- 2.30.2