### Steps to reproduce the issue 1. Instrument and compile the input file product.c using the command: e-acsl-gcc.sh -c product.c The content of product.c is as follows: ```C /*@ requires n >= 0; @ ensures \result == \product(0, n-1, \lambda integer k; t[k]); @*/ int array_product(int t[], int n) { int p = 1; for(int i = 0; i < n; i++) p *= t[i]; return p; } int main() { int arr[1] = {2}; int product = array_product(arr, 1); /*@ assert product == 2; */ return 0; } ``` ### Expected behaviour The instrumentation process should complete successfully, and Frama-C should generate three output files: ./a.out, ./a.out.frama-c, and ./a.out.e-acsl. ### Actual behaviour During the instrumentation of the input file, Frama-C reports "Terminated" and causes the entire WSL environment to crash. The complete output for the command is as follows: ``` ++ /home/doge/.opam/4.14.1/bin/frama-c -keep-unused-functions none -machdep gcc_x86_64 '-cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 ' -no-frama-c-stdlib ./product.c -e-acsl -e-acsl-share=/home/doge/.opam/4.14.1/bin/../share/frama-c/share/e-acsl -then-last -print -ocode a.out.frama.c Terminated ``` ### Contextual information - Frama-C installation mode: Opam - Frama-C version: 31.0 (Gallium) - Plug-in used: E-ACSL - OS name: WSL 2 - OS version: Windows 11, Ubuntu 24.04 Reported on behalf of Wenjian Chai (chaiwj@ios.ac.cn)