Memory mismatch counterexample has wrong stored value

[nunoplopes]

./alive-tv ../tests/alive-tv/refinement/nondet-fail.srctgt.llproduces:

ERROR: Mismatch in memory

Mismatch in null
Source value: poison
Target value: poison

The issue is that these days the refinement ptr is given by a UF (|#idx_refinement|) whose inputs are quantified variables.
There isn't an obvious way to get the right pointer, but we should be able to analyze the function interpretation in the model and get the non-default value. There should be only one.