split_vc fails for Z3
Hi,
why3prove
seems to have problems to apply the transformation split_vc
for Z3.
The attached file contains two modules, M1
and M2
, that only differ in the order of declaration of two functions. When I execute prove
on M1 the program fail to generate vc files:
$ why3 prove -P z3 -a split_vc -o tmp bugz3.mlw -T M1
Failure in transformation encoding_smt_if_poly
Failure in transformation enco_poly:guards
Ident seq is not yet declared