Fix Assertion (compiler warning) in theory/bv/theory_bv.cpp
authorAina Niemetz <aina.niemetz@gmail.com>
Wed, 9 Aug 2017 22:27:33 +0000 (15:27 -0700)
committerAina Niemetz <aina.niemetz@gmail.com>
Wed, 9 Aug 2017 22:27:33 +0000 (15:27 -0700)
src/theory/bv/theory_bv.cpp

index 1a59687dbd7e5cb3e008424373aa4bf5c62e3a54..fcd7312664b2ed70c863b4f272335e011c2cf077 100644 (file)
@@ -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() ){