Use unary_plus_exprt in bitvector flattening

danpoe · danpoe · commit 1f01bbf739e8 · 2018-09-10T16:32:52.000+01:00
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
@@ -249,8 +249,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
     return convert_unary_minus(to_unary_expr(expr));
   else if(expr.id()==ID_unary_plus)
   {
-    assert(expr.operands().size()==1);
-    return convert_bitvector(expr.op0());
+    return convert_bitvector(to_unary_plus_expr(expr).op());
   }
   else if(expr.id()==ID_abs)
     return convert_abs(to_abs_expr(expr));

Original file line number	Diff line number	Diff line change
`@@ -249,8 +249,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)`
`249`	`249`	`return convert_unary_minus(to_unary_expr(expr));`
`250`	`250`	`else if(expr.id()==ID_unary_plus)`
`251`	`251`	`{`
`252`		`- assert(expr.operands().size()==1);`
`253`		`- return convert_bitvector(expr.op0());`
	`252`	`+ return convert_bitvector(to_unary_plus_expr(expr).op());`
`254`	`253`	`}`
`255`	`254`	`else if(expr.id()==ID_abs)`
`256`	`255`	`return convert_abs(to_abs_expr(expr));`