./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.
./alive-tv ../tests/alive-tv/refinement/nondet-fail.srctgt.llproduces: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.