[WP] non-termination of strategies with Filter
Steps to reproduce the issue
On the attached example
running the following command
frama-c code.c -wp -wp-rte -wp-prover=tip -wp-timeout 1 -wp-prop vhm_preserved
to apply a strategy with Filter does not seem to terminate:
strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec.
strategy EagerAltErgo: \prover("alt-ergo",10); // run Alt-Ergo for 10 sec.
//Loops for vhm_preserved
strategy FilterProver:
FastAltErgo,
\tactic("Wp.filter"
,\goal(_)
,\children(EagerAltErgo)
),
EagerAltErgo;
proof FilterProver: vhm_preserved;
Expected behaviour
Termination.
Actual behaviour
Strategy application of Filter tactic with WP does not terminate.
Contextual information
- Frama-C installation mode: opam from GIT pub
- Frama-C version: first version of the strategy mechanism (https://git.frama-c.com/pub/frama-c.git#3396bd), also the recent update on master on pub (by the branch fix/wp/strategies)
- Plug-in used: WP with Why3 1.6.0 and Alt-Ergo 2.4.3
- OS name: Ubuntu
- OS version: 22.04
Additional information (optional)
It seems that similar non-termination was observed with Split but I do not have an example by hand.