From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 13 Jun 2019 06:33:17 +0000 (-0500)
Subject: Fix warning (#3053)
X-Git-Tag: cvc5-1.0.0~4112
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c324e6a40974040c02c8c9f948dbb332401b624c;p=cvc5.git

Fix warning (#3053)
---

diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
index 9160546f9..7b966f2c6 100644
--- a/src/proof/er/er_proof.cpp
+++ b/src/proof/er/er_proof.cpp
@@ -333,7 +333,7 @@ prop::SatLiteral resolveModify(
     std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>& dest,
     const prop::SatClause& src)
 {
-  bool foundPivot = false;
+  CVC4_UNUSED bool foundPivot = false;
   prop::SatLiteral pivot(0, false);
 
   for (prop::SatLiteral lit : src)
@@ -341,8 +341,10 @@ prop::SatLiteral resolveModify(
     auto negationLocation = dest.find(~lit);
     if (negationLocation != dest.end())
     {
+#ifdef CVC4_ASSERTIONS
       Assert(!foundPivot);
       foundPivot = true;
+#endif
       dest.erase(negationLocation);
       pivot = ~lit;
     }