Use unary_plus_exprt in smt2 conversion

danpoe · danpoe · commit 083561f94428 · 2018-09-10T16:32:52.000+01:00
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -1053,8 +1053,7 @@ void smt2_convt::convert_expr(const exprt &expr)
   else if(expr.id()==ID_unary_plus)
   {
     // A no-op (apart from type promotion)
-    assert(expr.operands().size()==1);
-    convert_expr(expr.op0());
+    convert_expr(to_unary_plus_expr(expr).op());
   }
   else if(expr.id()==ID_sign)
   {

Original file line number	Diff line number	Diff line change
`@@ -1053,8 +1053,7 @@ void smt2_convt::convert_expr(const exprt &expr)`
`1053`	`1053`	`else if(expr.id()==ID_unary_plus)`
`1054`	`1054`	`{`
`1055`	`1055`	`// A no-op (apart from type promotion)`
`1056`		`- assert(expr.operands().size()==1);`
`1057`		`- convert_expr(expr.op0());`
	`1056`	`+ convert_expr(to_unary_plus_expr(expr).op());`
`1058`	`1057`	`}`
`1059`	`1058`	`else if(expr.id()==ID_sign)`
`1060`	`1059`	`{`