Skip to content

Commit 320ab53

Browse files
committed
Rename variable for clarity
This bit vector is not necessarily filled with zeros. Also, use `pop_back` to avoid an iterator dance.
1 parent 440ea26 commit 320ab53

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

src/solvers/flattening/bv_utils.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -615,10 +615,10 @@ literalt bv_utilst::overflow_negate(const bvt &bv)
615615
// a overflow on unary- can only happen with the smallest
616616
// representable number 100....0
617617

618-
bvt zeros(bv);
619-
zeros.erase(--zeros.end());
618+
bvt should_be_zeros(bv);
619+
should_be_zeros.pop_back();
620620

621-
return prop.land(bv[bv.size()-1], !prop.lor(zeros));
621+
return prop.land(bv[bv.size() - 1], !prop.lor(should_be_zeros));
622622
}
623623

624624
void bv_utilst::incrementer(

0 commit comments

Comments
 (0)