From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 9 Oct 2018 03:16:57 +0000 (-0700)
Subject: Fix compiler warnings. (#2601)
X-Git-Tag: cvc5-1.0.0~4445
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f0340df210f2bb2a0a5fd95e0d9e6a8548cf1fc7;p=cvc5.git

Fix compiler warnings. (#2601)
---

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() ){