try specifying full path to z3

src/halmos/config.py

@@ -1,6 +1,7 @@
 import argparse
 import os
 import re
+import shutil
 import sys
 from collections import OrderedDict
 from collections.abc import Callable, Generator
@@ -441,7 +442,7 @@ class Config:
 
     solver_command: str = arg(
         help="use the given command when invoking the solver",
-        global_default="z3.exe" if os.name == "nt" else "z3",
+        global_default=shutil.which("z3"),
         metavar="COMMAND",
         group=solver,
     )