Missing changes (thanks to @someplaceguy)

HOL-Theorem-Prover · Jan 15, 2024 · cd78400 · cd78400
1 parent c60f050
commit cd78400
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/developers/docker-ci/Dockerfile b/developers/docker-ci/Dockerfile
@@ -31,7 +31,7 @@ ENV HOL4_Z3_EXECUTABLE=${Z3_VERSION:+/ML/z3-${Z3_VERSION}/bin/z3}
 
 # if --build-arg CVC_VERSION=5, set HOL4_CVC_EXECUTABLE to its full path,
 # or set to null otherwise.
-ENV HOL4_CVC_EXECUTABLE=${CVC_VERSION:+/ML/cvc${Z3_VERSION}-Linux}
+ENV HOL4_CVC_EXECUTABLE=${CVC_VERSION:+/ML/cvc${CVC_VERSION}-Linux}
 
 # if --build-arg YICES_VERSION=1.0.40, set HOL4_YICES_EXECUTABLE to its full path,
 # or set to null otherwise.

diff --git a/src/HolSmt/CVC.sml b/src/HolSmt/CVC.sml
@@ -28,7 +28,10 @@ structure CVC = struct
   fun mk_CVC_fun name pre cmd_stem post goal =
     case OS.Process.getEnv "HOL4_CVC_EXECUTABLE" of
       SOME file =>
-        SolverSpec.make_solver pre (file ^ cmd_stem) post goal
+        if file = "" then
+           raise Feedback.mk_HOL_ERR "CVC" name error_msg
+        else
+           SolverSpec.make_solver pre (file ^ cmd_stem) post goal
     | NONE =>
         raise Feedback.mk_HOL_ERR "CVC" name error_msg