diff --git a/pyk/package/version b/pyk/package/version
index 2635392e288..44516207be3 100644
--- a/pyk/package/version
+++ b/pyk/package/version
@@ -1 +1 @@
-0.1.447
+0.1.448
diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml
index 4bd4491d8cd..412c91ea1bd 100644
--- a/pyk/pyproject.toml
+++ b/pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.447"
+version = "0.1.448"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/pyk/src/pyk/cli/args.py b/pyk/src/pyk/cli/args.py
index 4504bab520d..47b633cf637 100644
--- a/pyk/src/pyk/cli/args.py
+++ b/pyk/src/pyk/cli/args.py
@@ -101,6 +101,12 @@ def smt_args(self) -> ArgumentParser:
             type=int,
             help='Number of times to retry SMT queries with scaling timeouts.',
         )
+        args.add_argument(
+            '--smt-tactic',
+            dest='smt_tactic',
+            type=str,
+            help='Z3 tactic to use when checking satisfiability. Example: (check-sat-using smt)',
+        )
         return args
 
     @cached_property
diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py
index e80ccb1f3f8..754e520c2a0 100644
--- a/pyk/src/pyk/kore/rpc.py
+++ b/pyk/src/pyk/kore/rpc.py
@@ -850,6 +850,7 @@ def __init__(
         smt_timeout: int | None = None,
         smt_retry_limit: int | None = None,
         smt_reset_interval: int | None = None,
+        smt_tactic: str | None = None,
         command: str | Iterable[str] | None = None,
         bug_report: BugReport | None = None,
         haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE,
@@ -881,6 +882,8 @@ def __init__(
             smt_server_args += ['--smt-retry-limit', str(smt_retry_limit)]
         if smt_reset_interval:
             smt_server_args += ['--smt-reset-interval', str(smt_reset_interval)]
+        if smt_tactic:
+            smt_server_args += ['--smt-tactic', smt_tactic]
 
         haskell_log_args = (
             [
@@ -980,6 +983,7 @@ def __init__(
         smt_timeout: int | None = None,
         smt_retry_limit: int | None = None,
         smt_reset_interval: int | None = None,
+        smt_tactic: str | None = None,
         command: str | Iterable[str] | None,
         bug_report: BugReport | None = None,
         haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE,
@@ -1027,6 +1031,7 @@ def __init__(
             smt_timeout=smt_timeout,
             smt_retry_limit=smt_retry_limit,
             smt_reset_interval=smt_reset_interval,
+            smt_tactic=smt_tactic,
             command=args,
             bug_report=bug_report,
             haskell_log_format=haskell_log_format,
@@ -1045,6 +1050,7 @@ def kore_server(
     bug_report: BugReport | None = None,
     smt_timeout: int | None = None,
     smt_retry_limit: int | None = None,
+    smt_tactic: str | None = None,
     haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE,
     haskell_log_entries: Iterable[str] = (),
     log_axioms_file: Path | None = None,
@@ -1059,6 +1065,7 @@ def kore_server(
             bug_report=bug_report,
             smt_timeout=smt_timeout,
             smt_retry_limit=smt_retry_limit,
+            smt_tactic=smt_tactic,
             haskell_log_format=haskell_log_format,
             haskell_log_entries=haskell_log_entries,
             log_axioms_file=log_axioms_file,
@@ -1072,6 +1079,7 @@ def kore_server(
         bug_report=bug_report,
         smt_timeout=smt_timeout,
         smt_retry_limit=smt_retry_limit,
+        smt_tactic=smt_tactic,
         haskell_log_format=haskell_log_format,
         haskell_log_entries=haskell_log_entries,
         log_axioms_file=log_axioms_file,