Skip to content

Commit

Permalink
remove cvc4 from project files
Browse files Browse the repository at this point in the history
  • Loading branch information
kanigsson committed Nov 28, 2023
1 parent 3198368 commit 9ab5b4f
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 2 deletions.
2 changes: 1 addition & 1 deletion defaults.gpr
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ abstract project Defaults is

Proof_Switches :=
(
"--prover=z3,cvc4,altergo",
"--prover=z3,cvc5,altergo",
"--steps=0",
"--timeout=60",
"--memlimit=1500",
Expand Down
1 change: 1 addition & 0 deletions examples/apps/ping/ping.gpr
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ project Ping is
package Prove is
for Proof_Switches ("Ada") use Defaults.Proof_Switches;
for Proof_Switches ("rflx-rflx_arithmetic.adb") use ("--prover=Z3,altergo,cvc5,colibri", "--timeout=120");
for Proof_Switches ("rflx-icmp-message.adb") use ("--timeout=120");
end Prove;

end Ping;
2 changes: 1 addition & 1 deletion examples/apps/spdm_responder/build_lib.gpr
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ project Build_Lib is

package Prove is
for Proof_Switches ("Ada") use Defaults.Proof_Switches;
for Proof_Switches ("responder.adb") use ("--prover=z3,cvc4", "--steps=64000", "--memlimit=6000", "--timeout=600");
for Proof_Switches ("responder.adb") use ("--prover=z3,cvc5", "--steps=64000", "--memlimit=6000", "--timeout=600");
end Prove;

end Build_Lib;

0 comments on commit 9ab5b4f

Please sign in to comment.