diff --git a/regression/cbmc/Pointer_Arithmetic15/main.c b/regression/cbmc/Pointer_Arithmetic15/main.c index 99873ad6a46..3e866c37d30 100644 --- a/regression/cbmc/Pointer_Arithmetic15/main.c +++ b/regression/cbmc/Pointer_Arithmetic15/main.c @@ -15,5 +15,9 @@ int main() a = p - q; + // mixing types: the C front-end will insert casts + unsigned long long u; + p = (p + a) + u; + assert(0); } diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 69795588a62..ebc6ba93b48 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -439,16 +439,24 @@ simplify_exprt::resultt<> simplify_exprt::simplify_plus(const plus_exprt &expr) expr.op0().id() == ID_plus && expr.op0().type().id() == ID_pointer && expr.op0().operands().size() == 2) { - plus_exprt op0 = to_plus_expr(expr.op0()); + plus_exprt result = to_plus_expr(expr.op0()); + if(as_const(result).op0().type().id() != ID_pointer) + result.op0().swap(result.op1()); + const exprt &op1 = as_const(result).op1(); - if(op0.op1().id() == ID_plus) - to_plus_expr(op0.op1()).add_to_operands(expr.op1()); + if(op1.id() == ID_plus) + { + plus_exprt new_op1 = to_plus_expr(op1); + new_op1.add_to_operands( + typecast_exprt::conditional_cast(expr.op1(), new_op1.op0().type())); + result.op1() = simplify_plus(new_op1); + } else - op0.op1()=plus_exprt(op0.op1(), expr.op1()); - - auto result = op0; - - result.op1() = simplify_plus(to_plus_expr(result.op1())); + { + plus_exprt new_op1{ + op1, typecast_exprt::conditional_cast(expr.op1(), op1.type())}; + result.op1() = simplify_plus(new_op1); + } return changed(simplify_plus(result)); }