diff --git a/developers/docker-ci/Dockerfile b/developers/docker-ci/Dockerfile
index 4e7a048961..71dac05cb0 100644
--- 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
index a3c59f4ba6..c7e34d49c7 100644
--- 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