add special cases to handle setting timeouts for SBV-based solvers

fixes #1808

* Yices still does not work due to unexpected
  behavior after a timeout is triggered
  (see: LeventErkok/sbv#735)

* the special cases for CVC4/5 are addressed in
  the 11.1.5 release for SBV (which is not compatible
  with cryptol as it requires GHC 9.8)

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
 

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)

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