@tautschnig, @kroening, anything controversial about merging this?

The only question I'm aware of was a missing regression test or any kind of example where errors had been triggered. As far as I recall, this would only become necessary when using dereferencet (pointer-analysis/dereference.h).

I looked at this; I'd say that the multi-ary expressions should not be used for pointer arithmetic to begin with. The rule should be that all operands in a multi-ary expression must have the same type.

@kroening make_binary isn't used widely, git grep -l make_binary suggests that 3/8 users are pointer-related:

analyses/goto_check.cpp
analyses/local_bitvector_analysis.cpp
analyses/local_may_alias.cpp
goto-symex/adjust_float_expressions.cpp
pointer-analysis/dereference.cpp
solvers/prop/bdd_expr.cpp
solvers/refinement/refine_arithmetic.cpp
solvers/smt2/smt2_conv.cpp
util/expr_util.cpp
util/expr_util.h

I'll try to clean this up and remove the source of multi-ary pointer expressions (that should be the simplifier).

Thank you! If we wanted to be very conservative, we could check the rule "all operands must have same type" with an assertion, while at it.

I haven't tweaked the simplifier, but instead removed all uses of make_binary in contexts where such would not be safe - and added a check in make_binary to make sure no future such use creeps in.