Changed and invalid counterexamples after elimination
!564 (merged) changes countless counterexamples in the SPARK testsuite. In many cases they can even be detected as invalid by the SPARK counterexample printer (e.g. invalid range values). This behaviour currently blocks the merge of upstream Why3 into SPARK Why3.
It seems that in these cases relevant definitions aren't available until the generation of the third prover model, where the prover isn't capable any more to generate a valid model.
I have tried to make the transformation eliminate_definition_conditionally
less strict by eliminating only the definitions of recursive functions (as before this MR) and constants, see diff below. This seems to resolve the issue in SPARK but breaks just one of the Petiot experiments (R4).
-let eliminate_definition_conditionally =
- Trans.on_meta Detect_polymorphism.meta_monomorphic_types_only
- (function
- | [] -> eliminate_definition
- | _ ->
- Trans.on_meta Inlining.meta_get_counterexmp
- (function
- | [] -> eliminate_recursion
- | _ -> eliminate_definition))
+let eliminate_const_definition =
+ eliminate_definition_gen (fun ls -> ls.ls_args = [])
+
+let eliminate_definition_conditionally =
+ Trans.on_meta Detect_polymorphism.meta_monomorphic_types_only
+ (function
+ | [] -> eliminate_definition
+ | _ ->
+ Trans.on_meta Inlining.meta_get_counterexmp
+ (function
+ | [] -> eliminate_recursion
+ | _ -> Trans.compose eliminate_recursion eliminate_const_definition))