Lost counterexamples after reduction of prover models
MR !577 (merged) changed the structure for the model generation to counter the lost model values in SPARK introduced by !564 (merged). Many model values were gained by the former MR, but a number of model variables revelant for check-ce were lost, should be recovered. These tests are currently XFAIL in bench/ce-bench
.
-
bench/ce/bv32: missing model:
requires
in the first model seems to prevent model generation altogether (cannot fix?) -
bench/ce/jlamp0: missing loop variables (before iteration): no queried term for variable
a2
in model parser
Edited by Benedikt Becker