Increase level for SPARK proofs of the runtime

AdaCore · Nov 4, 2024 · dd8869e · dd8869e
1 parent c69c59a
commit dd8869e
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/support/data/runtime_build.gpr.in b/support/data/runtime_build.gpr.in
@@ -64,12 +64,13 @@ project Runtime_Build is
     for Proof_Switches ("Ada") use ("-j0", "--level=2", "--function-sandboxing=off", "--counterexamples=off");
 
     --  Specialize the command-line for more complex units (-j0 is implied)
+    for Proof_Switches ("a-strmap.adb") use ("--level=3");
     for Proof_Switches ("a-strfix.adb") use ("--level=4");
     for Proof_Switches ("a-strsea.adb") use ("--level=4");
     for Proof_Switches ("a-strsup.adb") use ("--level=4", "--timeout=30");
     for Proof_Switches ("i-c.adb") use ("--level=4", "--timeout=120");
     for Proof_Switches ("s-arit32.adb") use ("--level=3", "--prover=all");
-    for Proof_Switches ("s-arit64.adb") use ("--level=3", "--prover=all");
+    for Proof_Switches ("s-arit64.adb") use ("--level=4", "--prover=all");
     for Proof_Switches ("s-expmod.adb") use ("--level=2");
     for Proof_Switches ("s-imgboo.adb") use ("--level=3");
     for Proof_Switches ("s-valboo.adb") use ("--level=3");