Functions in CE models not consistent with axioms in the source code
In the tests bench/check-ce/let_function_logic.mlw
, bench/check-ce/call-val-function.mlw
, bench/check-ce/vall_function.mlw
(and maybe some others), the SMT solver returns a model with some functions that are not consistent with the axioms in the .mlw
file.
The consequence is that we can have CE classified as good
while it should not be the case.