diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java
index 94b11f4ed92..cc95b117946 100644
--- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java
+++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java
@@ -129,6 +129,10 @@ public RewriterResult execute(K k, Optional<Integer> depth) {
                     args.add("--smt-prelude");
                     args.add(smtOptions.smtPrelude);
                 }
+                if (smtOptions.smtTimeout != null) {
+                    args.add("--smt-timeout");
+                    args.add(Integer.toString(smtOptions.smtTimeout));
+                }
                 koreCommand = args.toArray(koreCommand);
                 if (backendOptions.dryRun) {
                     System.out.println(String.join(" ", koreCommand));
@@ -222,6 +226,10 @@ public K search(K initialConfiguration, Optional<Integer> depth, Optional<Intege
                     args.add("--smt-prelude");
                     args.add(smtOptions.smtPrelude);
                 }
+                if (smtOptions.smtTimeout != null) {
+                    args.add("--smt-timeout");
+                    args.add(Integer.toString(smtOptions.smtTimeout));
+                }
                 koreCommand = args.toArray(koreCommand);
                 if (backendOptions.dryRun) {
                     System.out.println(String.join(" ", koreCommand));
@@ -313,6 +321,10 @@ private List<String> buildCommonProvingCommand(String defPath, String specPath,
                     args.add("--smt-prelude");
                     args.add(smtOptions.smtPrelude);
                 }
+                if (smtOptions.smtTimeout != null) {
+                    args.add("--smt-timeout");
+                    args.add(Integer.toString(smtOptions.smtTimeout));
+                }
                 if (kProveOptions.debugScript != null) {
                     if (!kProveOptions.debugger) {
                         throw KEMException.criticalError("Can only use --debug-script with --debugger.");
diff --git a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
index be98722ed52..db6fde3fbc4 100644
--- a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
+++ b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
@@ -41,16 +41,13 @@ public Class<SMTSolver> enumClass() {
     @Parameter(names={"--smt-prelude", "--smt_prelude"}, description="Path to the SMT prelude file.", hidden = true)
     public String smtPrelude;
 
+    @Parameter(names="--smt-timeout", description="Timeout for calls to the SMT solver, in milliseconds.", hidden = true)
+    public Integer smtTimeout = null;
+
     @Parameter(names="--z3-jni", description="Invokes Z3 as JNI library. Default is external process. " +
             "JNI is slightly faster, but can potentially lead to JVM crash.", hidden = true)
     public boolean z3JNI = false;
 
-    @Parameter(names="--z3-cnstr-timeout", description="The default soft timeout (in milli seconds) of Z3 for checking constraint satisfiability.", hidden = true)
-    public int z3CnstrTimeout = 50;
-
-    @Parameter(names="--z3-impl-timeout", description="The default soft timeout (in milli seconds) of Z3 for checking implication.", hidden = true)
-    public int z3ImplTimeout = 5000;
-
     @Parameter(names="--z3-tactic", description="The solver tactic to use to check satisfiability in Z3.", hidden = true)
     public String z3Tactic;
 }