projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
7415a23
)
Fix Assertion (compiler warning) in theory/bv/theory_bv.cpp
author
Aina Niemetz
<aina.niemetz@gmail.com>
Wed, 9 Aug 2017 22:27:33 +0000
(15:27 -0700)
committer
Aina Niemetz
<aina.niemetz@gmail.com>
Wed, 9 Aug 2017 22:27:33 +0000
(15:27 -0700)
src/theory/bv/theory_bv.cpp
patch
|
blob
|
history
diff --git
a/src/theory/bv/theory_bv.cpp
b/src/theory/bv/theory_bv.cpp
index 1a59687dbd7e5cb3e008424373aa4bf5c62e3a54..fcd7312664b2ed70c863b4f272335e011c2cf077 100644
(file)
--- 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() ){