summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHaniel Barbosa <hanielbbarbosa@gmail.com>2019-06-13 01:33:17 -0500
committerAndres Noetzli <andres.noetzli@gmail.com>2019-06-12 23:33:16 -0700
commitc324e6a40974040c02c8c9f948dbb332401b624c (patch)
tree0980281a64a1812575020f1d77fa7d2c19410d72
parentc83ce8f341f88bbffcae8fd2bfbed5c33abf4f66 (diff)
Fix warning (#3053)
-rw-r--r--src/proof/er/er_proof.cpp4
1 files changed, 3 insertions, 1 deletions
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback