From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 9 Aug 2017 22:27:33 +0000 (-0700)
Subject: Fix Assertion (compiler warning) in theory/bv/theory_bv.cpp
X-Git-Tag: cvc5-1.0.0~5688
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b725191b5edc9d2fcdabab0abb42f60cb124e59b;p=cvc5.git

Fix Assertion (compiler warning) in theory/bv/theory_bv.cpp
---

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 1a59687db..fcd731266 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -510,7 +510,8 @@ bool TheoryBV::doExtfInferences( std::vector< Node >& terms ) {
   std::map< Node, Node > op_map;
   for( unsigned j=0; j<terms.size(); j++ ){
     TNode n = terms[j];
-    Assert( n.getKind()==kind::BITVECTOR_TO_NAT || kind::INT_TO_BITVECTOR );
+    Assert (n.getKind() == kind::BITVECTOR_TO_NAT
+            || n.getKind() == kind::INT_TO_BITVECTOR );
     if( n.getKind()==kind::BITVECTOR_TO_NAT ){
       //range lemmas
       if( d_extf_range_infer.find( n )==d_extf_range_infer.end() ){