Fix compiler warnings. (#2601)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index c8248d8037f9847fd6a1d60497ecf632871a6a0b..be7c5c665a74f5929850a90269561f1081b148aa 100644 (file)
--- 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 3348799933c2dee78a6376ede172b7a4430e88da..c9aef98286adf266f30ac33529a7956b5012da8b 100644 (file)
--- 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() ){