From 9ab5b4f9371104c4dbc590cd3bbf56518c0cc273 Mon Sep 17 00:00:00 2001
From: Johannes Kanig <kanig@adacore.com>
Date: Mon, 27 Nov 2023 19:10:02 +0900
Subject: [PATCH] remove cvc4 from project files

---
 defaults.gpr                               | 2 +-
 examples/apps/ping/ping.gpr                | 1 +
 examples/apps/spdm_responder/build_lib.gpr | 2 +-
 3 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/defaults.gpr b/defaults.gpr
index 7b5524aa4..81ff9b0a3 100644
--- a/defaults.gpr
+++ b/defaults.gpr
@@ -65,7 +65,7 @@ abstract project Defaults is
 
    Proof_Switches :=
    (
-      "--prover=z3,cvc4,altergo",
+      "--prover=z3,cvc5,altergo",
       "--steps=0",
       "--timeout=60",
       "--memlimit=1500",
diff --git a/examples/apps/ping/ping.gpr b/examples/apps/ping/ping.gpr
index f93242cd4..709b3d75e 100644
--- a/examples/apps/ping/ping.gpr
+++ b/examples/apps/ping/ping.gpr
@@ -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;
diff --git a/examples/apps/spdm_responder/build_lib.gpr b/examples/apps/spdm_responder/build_lib.gpr
index 90d27c8b5..57bb88dba 100644
--- a/examples/apps/spdm_responder/build_lib.gpr
+++ b/examples/apps/spdm_responder/build_lib.gpr
@@ -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;