diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs
index 407f3fe24..1554d923a 100644
--- a/src/Cryptol/Symbolic/SBV.hs
+++ b/src/Cryptol/Symbolic/SBV.hs
@@ -110,11 +110,36 @@ proverConfigs =
 setTimeoutSecs ::
   Int {- ^ seconds -} ->
   SBV.SMTConfig -> SBV.SMTConfig
-setTimeoutSecs s cfg = cfg
-  { SBV.solverSetOptions =
-    SBV.OptionKeyword ":timeout" [show (toInteger s * 1000)] :
-    filter (not . isTimeout) (SBV.solverSetOptions cfg) }
+setTimeoutSecs s cfg = case SBV.name (SBV.solver cfg) of
+  SBV.Yices -> cfg'
+  -- FIXME: although this correctly sets the timeout for Yices,
+  -- SBV crashes due to an unexpected response from Yices after
+  -- a timeout is hit.
+  -- see:
+  --   https://github.com/LeventErkok/sbv/issues/735
+  --   https://github.com/SRI-CSL/yices2/issues/547
+    { SBV.extraArgs =
+      ["--timeout", show (toInteger s)] ++
+      SBV.extraArgs cfg' }
+  -- NOTE: in sbv 11.1.5 these special cases are handled
+  -- by a new 'SetTimeOut' constructor for 'SMTOption'
+  SBV.CVC4 -> cfg'
+    { SBV.extraArgs =
+      ["--tlimit-per", show (toInteger s * 1000)] ++
+      SBV.extraArgs cfg' }
+  SBV.CVC5 -> cfg'
+    { SBV.extraArgs =
+      ["--tlimit-per", show (toInteger s * 1000)] ++
+      SBV.extraArgs cfg' }
+  _ -> cfg'
+    { SBV.solverSetOptions =
+      SBV.OptionKeyword ":timeout" [show (toInteger s * 1000)] :
+      (SBV.solverSetOptions cfg') }
   where
+    cfg' = cfg
+      { SBV.solverSetOptions =
+        filter (not . isTimeout) (SBV.solverSetOptions cfg) }
+
     isTimeout (SBV.OptionKeyword k _) = k == ":timeout"
     isTimeout _ = False
 
diff --git a/tests/issues/issue_1808.icry b/tests/issues/issue_1808.icry
new file mode 100644
index 000000000..f4cbee6d9
--- /dev/null
+++ b/tests/issues/issue_1808.icry
@@ -0,0 +1,14 @@
+:set proverTimeout=1
+
+:l ../../examples/funstuff/NQueens.cry
+
+:set prover=sbv-z3
+:sat nQueens : (Solution 50)
+
+:set prover=sbv-cvc5
+:sat nQueens : (Solution 50)
+
+// FIXME:
+//   broken due to: https://github.com/LeventErkok/sbv/issues/735
+// :set prover=sbv-yices
+// :sat nQueens : (Solution 50)
\ No newline at end of file
diff --git a/tests/issues/issue_1808.icry.stdout b/tests/issues/issue_1808.icry.stdout
new file mode 100644
index 000000000..1ce911618
--- /dev/null
+++ b/tests/issues/issue_1808.icry.stdout
@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+Unknown.
+  Reason: timeout
+Unknown.
+  Reason: timeout