diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-08-09 15:27:33 -0700 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2017-08-09 15:27:33 -0700 |
| commit | b725191b5edc9d2fcdabab0abb42f60cb124e59b (patch) | |
| tree | e53ee6b9c62c09c5ee2413c830c33a5be7034312 | |
| parent | 7415a23edde7cc115fea19e8084ec15baa01c311 (diff) | |
Fix Assertion (compiler warning) in theory/bv/theory_bv.cpp
| -rw-r--r-- | src/theory/bv/theory_bv.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
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() ){ |