# HG changeset patch
# User wenzelm
# Date 1736347792 -3600
# Node ID a1743b71092e2a8b3b0829b45d6996d03655b3c0
# Parent  31b1c203357ac8491f2448b863b326dd59148b06# Parent  e4a2858ba7e27822798932e51f952fd5b2adaae2
merged

diff -r 31b1c203357a -r a1743b71092e Admin/components/components.sha1
--- a/Admin/components/components.sha1	Wed Jan 08 15:10:09 2025 +0100
+++ b/Admin/components/components.sha1	Wed Jan 08 15:49:52 2025 +0100
@@ -47,6 +47,7 @@
 e99560d0b7cb9bafde2b0ec1a3a95af315918a25 cvc4-1.8.tar.gz
 9e0d91f9f3bc0b69e60e50ca683cfcdcbfee6d62 cvc5-1.0.2.tar.gz
 fb4dce7e622c5e3daf56e7db190e05c34985c9f6 cvc5-1.1.1.tar.gz
+061ab74da6f101b7cf9935d0dac0bf58c62b19b5 cvc5-1.2.0-1.tar.gz
 9cd7fa5e32187383fbf461d3643cf982a318e39d cvc5-1.2.0.tar.gz
 842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz
 cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz
diff -r 31b1c203357a -r a1743b71092e src/HOL/Tools/Nunchaku/nunchaku.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku.ML	Wed Jan 08 15:10:09 2025 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML	Wed Jan 08 15:49:52 2025 +0100
@@ -277,9 +277,6 @@
               (print_n "External tool \"nunchaku\" cannot execute"; (unknownN, NONE))
             | Nunchaku_Not_Found =>
               (print_n "External tool \"nunchaku\" not found"; (unknownN, NONE))
-            | CVC4_Cannot_Execute =>
-              (print_n "External tool \"cvc4\" cannot execute"; (unknownN, NONE))
-            | CVC4_Not_Found => (print_n "External tool \"cvc4\" not found"; (unknownN, NONE))
             | Unknown_Error (code, msg) =>
               (print_n ("Error: " ^ unprefix_error msg ^
                  (if code = 0 then "" else " (code " ^ string_of_int code ^ ")"));
diff -r 31b1c203357a -r a1743b71092e src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Wed Jan 08 15:10:09 2025 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Wed Jan 08 15:49:52 2025 +0100
@@ -33,8 +33,6 @@
   | Nunchaku_Var_Not_Set
   | Nunchaku_Cannot_Execute
   | Nunchaku_Not_Found
-  | CVC4_Cannot_Execute
-  | CVC4_Not_Found
   | Unknown_Error of int * string
 
   val nunchaku_home_env_var: string
@@ -70,8 +68,6 @@
 | Nunchaku_Var_Not_Set
 | Nunchaku_Cannot_Execute
 | Nunchaku_Not_Found
-| CVC4_Cannot_Execute
-| CVC4_Not_Found
 | Unknown_Error of int * string;
 
 val nunchaku_home_env_var = "NUNCHAKU_HOME";
diff -r 31b1c203357a -r a1743b71092e src/Pure/Admin/component_cvc5.scala
--- a/src/Pure/Admin/component_cvc5.scala	Wed Jan 08 15:10:09 2025 +0100
+++ b/src/Pure/Admin/component_cvc5.scala	Wed Jan 08 15:49:52 2025 +0100
@@ -60,21 +60,22 @@
         Isabelle_System.make_directory(platform_dir)
 
         val exe_path = Path.explode("cvc5").exe_if(platform.is_windows)
+        val exe_bin_path = Path.explode("cvc5-bin").exe_if(platform.is_windows)
+
         val exe = platform_dir + exe_path
+        val exe_bin = platform_dir + exe_bin_path
 
         Isabelle_System.download_file(download, archive_path, progress = progress)
         Isabelle_System.extract(archive_path, download_dir, strip = true)
-        Isabelle_System.copy_file(download_dir + Path.basic("bin") + exe_path, platform_dir)
-        File.set_executable(exe)
+
+        Isabelle_System.copy_file(download_dir + Path.basic("bin") + exe_path, exe_bin)
+        File.set_executable(exe_bin)
 
-        if (platform.is_arm) {
-          Isabelle_System.move_file(exe, exe.ext("bin"))
-          File.write(exe, """#!/usr/bin/env bash
+        File.write(exe, """#!/usr/bin/env bash
 
-"$CVC5_HOME/cvc5.bin" "$@"
+"$CVC5_HOME/cvc5-bin" "$@"
 """)
-          File.set_executable(exe)
-        }
+        File.set_executable(exe)
       }
     }