Counterexample for one-region record
In new_ide, when a counterexample is given for a type with only one mutable region, the id which is used to refer to a variable of such type is then reused for a variable of its only mutable type. The problem is that the model_trace is not changed. An example of this is (bench/ce/arrays.mlw):
module A
use import int.Int
use import array.Array
let f2 (a:array int) : unit
requires { a.length >= 2 }
ensures { a[0] <> a[1] }
= a[0] <- 42
end
It can be seen because the counterexample is a = (0 => 42...) instead of a.elts = (0 => 42 ....).