Suggested steps too low

[treiher]

Describe the bug
The suggested steps are in some cases too low for a successful proof. While 1672 steps are suggested, 1768 steps are required.

$ run_spat -Ptest.gpr --suggest
[...]
package Prove is
   for Proof_Switches ("rflx-arrays-tests.adb") use ("--prover=Z3", "--steps=1672", "--timeout=1");
end Prove;

$ sparkprof -Ptest -u rflx-arrays-tests
---------------------------------------------------------------------------------------
UNIT                                                  MAX STEPS    MAX TIME  TOTAL TIME
[...]
rflx-arrays-tests                                       1768 steps     0.0 s     0.0 s

Here is the relevant .spark file: rflx-arrays-tests.spark.txt

Used version: run_spat V1.1.3 (compiled by SYSTEM_NAME_GNAT Community 2020 (20200429-93))

[Jellix]

I can confirm the defect.

Maximum number of steps reported in that file is '1864090' Z3 steps, which by the Z3 formula (steps - 450_000) / 800 should translate into the expected 1768 steps.

Instead, spat seems to pick up '1786890' Z3 steps as maximum, which by above formula result in the reported 1672 steps.

No obvious reason why that would happen, I'll investigate.

[Jellix]

Fixed in v1.1.4 and fix merged to main branch.