From b725191b5edc9d2fcdabab0abb42f60cb124e59b Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 9 Aug 2017 15:27:33 -0700
Subject: [PATCH] Fix Assertion (compiler warning) in theory/bv/theory_bv.cpp

---
 src/theory/bv/theory_bv.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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