Improvement: Noop Update in Unsat Core-Based Interpolation

[Heizmann]

If an update a[i]=v in a trace is useless for proving infeasibility the corresponding SMT formula (= a' (store a i v)) is in the unsatisfiable core because we need the information about the connection of a' and a.
This lead to interpolants of the form Ǝ i. a[i]=v that are usually useless and costly. We could avoid this by temporarily by changing the update to a[i]=tmp /\ tmp = v for an auxiliary variable tmp.