Typing error in extraction of values from counterexamples
The following example exposes an error with typing during RAC using values from counterexample
module Int32
type t = < range -0x8000_0000 0x7fff_ffff >
end
module Main_module
use Int32
use bv.BV64
let rec f (n : Int32.t) (min : Int32.t) : Int32.t
ensures { min = result } = n
end
The command
why3 prove ../tests/model_proj_bug.mlw -P CVC4,1.8,counterexamples --check-ce
results in
The following counterexample model could not be verified
(both RAC terminated because cannot import value from model: Cannot import projection t'int, argument type t is not value type t1):
File model_proj_bug.mlw:
Line 9:
min = {t'int => 0}
n = {t'int => 0}
Line 10:
min = {t'int => 0}
n = {t'int => 0}