Typing error in smt generated for CVC4/cvc5 with range types
Consider this simple example:
module Main_module
type t = < range 0 1 >
type s = { c3 : t }
let f (s0 : s) : int
requires { s0 = { c3 = (0 : t) } }
ensures { true }
= 1
end
If I run why3 prove xxx.mlw -a split_vc -P cvc4
, CVC4 complains about a typing error on subexpressions. The same problem exists when running cvc5.
I bisected and I found the problematic commit: b1290b92. It is related to the remove_unused transformation.
cc @marche who wrote this commit.