From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 30 Apr 2018 19:17:13 +0000 (-0700)
Subject: Remove dead code in bv-to-bool preprocessing pass (#1828)
X-Git-Tag: cvc5-1.0.0~5107
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=859b55b3ba0d6aa43b71e05bdc83480313c107ac;p=cvc5.git

Remove dead code in bv-to-bool preprocessing pass (#1828)

Fixes Coverity issue 1468436. As Coverity correctly detects,
kind::BITVECTOR_XOR is dealt with in an if-statement before the switch
statement on kind. This is because kind::XOR is binary while
kind::BITVECTOR_XOR is n-ary (as a comment in the code correctly
indicates).
---

diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
index b01a60031..745a16979 100644
--- a/src/preprocessing/passes/bv_to_bool.cpp
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -214,7 +214,6 @@ Node BVToBool::convertBvTerm(TNode node)
   {
     case kind::BITVECTOR_OR: new_kind = kind::OR; break;
     case kind::BITVECTOR_AND: new_kind = kind::AND; break;
-    case kind::BITVECTOR_XOR: new_kind = kind::XOR; break;
     case kind::BITVECTOR_NOT: new_kind = kind::NOT; break;
     default: Unhandled();
   }