[WP] Assertion failed in Instance tactic called from a custom strategy

Steps to reproduce the issue

I tried to narrow down the example, but it's hard to determine where is the problem exactly. I have an example file foo_lemma.c and a custom strategy plugin strategy_foo.ml.

Essentially the strategy tries to guide the solvers by finding witnesses in the hypotheses to instantiate existentially quantified predicates in the goal. It follows the iterative nature of the T predicates by unfolding them one step at a time until success. As recommended by the WP manual, the custom strategy only uses pre-defined tactics (namely Definition and Instance).

Launch frama-c -wp -load-module strategy_foo.ml -wp-auto Foo:T foo_lemma.c.

Expected behaviour

Frama-C should prove the lemma or at least not fail.

Actual behaviour

Frama-C fails with the following error:

[wp] foo_lemma.c:55: Warning: 
  [Instance] Exception <File "src/plugins/qed/term.ml", line 2516, characters 4-10: Assertion failed>
[kernel] Current source was: foo_lemma.c:55
  The full backtrace is:
  Raised at ProverSearch.fork in file "src/plugins/wp/ProverSearch.ml", line 57, characters 6-13
  Called from ProverSearch.lookup in file "src/plugins/wp/ProverSearch.ml", line 62, characters 10-33
  Called from ProverSearch.first in file "src/plugins/wp/ProverSearch.ml", line 84, characters 25-54
  Called from ProverScript.Env.search in file "src/plugins/wp/ProverScript.ml", line 192, characters 12-62
  Called from ProverScript.autosearch in file "src/plugins/wp/ProverScript.ml", line 299, characters 8-34
  Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
  Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
  Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
  Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
  Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
  Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
  Called from Task.Monad.progress in file "src/libraries/utils/task.ml" (inlined), line 98, characters 19-29
  Called from Task.progress in file "src/libraries/utils/task.ml", line 363, characters 14-36
  Re-raised at Task.progress in file "src/libraries/utils/task.ml", line 369, characters 6-13
  Called from Task.server_progress.(fun) in file "src/libraries/utils/task.ml", line 475, characters 14-27
  Called from Stdlib__list.find_all.find in file "list.ml", line 242, characters 17-20
  Called from Task.server_progress in file "src/libraries/utils/task.ml", line 473, characters 22-273
  Called from Task.on_idle.(fun) in file "src/libraries/utils/task.ml", line 344, characters 14-18
  Called from Register.do_wp_proofs in file "src/plugins/wp/register.ml", line 656, characters 4-33
  Called from Register.cmdline_run in file "src/plugins/wp/register.ml", line 722, characters 8-26
  Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 280, characters 14-17
  Re-raised at Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 280, characters 41-48
  Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 281, characters 2-12
  Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 281, characters 2-12
  Called from Stdlib__queue.iter.iter in file "queue.ml", line 121, characters 6-15
  Called from Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
  Called from Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
  Called from Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
  Called from Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
  
  Unexpected error (File "src/plugins/qed/term.ml", line 2516, characters 4-10: Assertion failed).
  Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
  Your Frama-C version is 24.0 (Chromium).
  Note that a version and a backtrace alone often do not contain enough
  information to understand the bug. Guidelines for reporting bugs are at:
  https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs

Contextual information

• Frama-C installation mode: Opam
• Frama-C version: 24.0 (Chromium)
• Plug-in used: WP
• OS name: Ubuntu
• OS version: 20.04.4 LTS

Additional information

I tried to see if the error would raise in GUI mode by manually activating the custom tactics in the editor instead of using -wp-auto Foo:T:
frama-c-gui -wp -load-module strategy_foo.ml foo_lemma.c

It turns out that it won't raise an error dialog, but the following stderr message ** (frama-c-gui:426361): CRITICAL **: 17:47:51.667: GSourceFunc: callback raised an exception, and the GUI remains in a somewhat stuck state. This could be another issue by itself maybe.

---

I tracked down the error: the assertion fails here (qed/term.ml:2516), from the call here (wp/TacInstance.ml:163).

It seems that for some reason (maybe related to the way I wrote my tactic?), the variable x chosen to unbind phi actually is not fresh (enough). On a local version of Frama-C I tried to replace the code at line 157 with the following:

          let pool = F.pool ~copy:env.feedback#pool () in
          List.iter (F.add_var pool) (F.e_vars (F.QED.lc_repr phi));
          let x = F.fresh pool tau in

Basically I'm force-ensuring that the subsequent assertion will not fail, and this seems to solve the problem, as far as I can tell.