Skip to content

Commit 7849645

Browse files
Refactoring in boolbvt::convert_abs
1 parent 05b3d18 commit 7849645

File tree

1 file changed

+3
-7
lines changed

1 file changed

+3
-7
lines changed

src/solvers/flattening/boolbv_abs.cpp

Lines changed: 3 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -16,24 +16,20 @@ Author: Daniel Kroening, [email protected]
1616

1717
bvt boolbvt::convert_abs(const exprt &expr)
1818
{
19-
std::size_t width=boolbv_width(expr.type());
19+
const std::size_t width = boolbv_width(expr.type());
2020

2121
if(width==0)
2222
return conversion_failed(expr);
2323

2424
const exprt::operandst &operands=expr.operands();
25-
26-
if(operands.size()!=1)
27-
throw "abs takes one operand";
28-
25+
DATA_INVARIANT(operands.size() == 1, "abs takes one operand");
2926
const exprt &op0=expr.op0();
30-
3127
const bvt &op_bv=convert_bv(op0);
3228

3329
if(op0.type()!=expr.type())
3430
return conversion_failed(expr);
3531

36-
bvtypet bvtype=get_bvtype(expr.type());
32+
const bvtypet bvtype = get_bvtype(expr.type());
3733

3834
if(bvtype==bvtypet::IS_FIXED ||
3935
bvtype==bvtypet::IS_SIGNED ||

0 commit comments

Comments
 (0)