GitLab

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 ....).