From adefd8864cc439ef34221c81430820d513176c13 Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Fri, 20 Sep 2024 17:34:20 -0700
Subject: [PATCH] KD: Allow passing extra params to the solver

---
 Data/SBV/Tools/KDKernel.hs |  4 +++-
 Data/SBV/Tools/KDUtils.hs  | 14 ++++++++------
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/Data/SBV/Tools/KDKernel.hs b/Data/SBV/Tools/KDKernel.hs
index 2ccfa9fa9..7d03f6b1d 100644
--- a/Data/SBV/Tools/KDKernel.hs
+++ b/Data/SBV/Tools/KDKernel.hs
@@ -102,7 +102,9 @@ lemmaGen cfg what nms inputProp by = do
     tab <- start (kdVerbose cfg) what nms
 
     let underlyingSolver = kdSolverConfig cfg
-        solver           = underlyingSolver{verbose = verbose underlyingSolver || kdVerbose cfg}
+        solver           = underlyingSolver{ verbose   = verbose   underlyingSolver || kdVerbose cfg
+                                           , extraArgs = extraArgs underlyingSolver ++ kdExtraSolverArgs cfg
+                                           }
 
         nm = intercalate "." nms
 
diff --git a/Data/SBV/Tools/KDUtils.hs b/Data/SBV/Tools/KDUtils.hs
index 60e59b1fc..9616d14d9 100644
--- a/Data/SBV/Tools/KDUtils.hs
+++ b/Data/SBV/Tools/KDUtils.hs
@@ -31,16 +31,18 @@ import Data.SBV.Core.Symbolic  (SMTConfig)
 import Data.SBV.Provers.Prover (defaultSMTCfg, z3, cvc5)
 
 -- | Keeping track of KD options/state
-data KDConfig = KDConfig { kdRibbonLength :: Int        -- ^ Lenght of the line as we print the proof
-                         , kdVerbose      :: Bool       -- ^ Run verbose
-                         , kdSolverConfig :: SMTConfig  -- ^ The backend solver to use
+data KDConfig = KDConfig { kdRibbonLength    :: Int        -- ^ Lenght of the line as we print the proof
+                         , kdVerbose         :: Bool       -- ^ Run verbose
+                         , kdExtraSolverArgs :: [String]   -- ^ Extra command line arguments to pass to the solver
+                         , kdSolverConfig    :: SMTConfig  -- ^ The backend solver to use
                          }
 
 -- | Default KD-config uses the default SBV config (which is z3)
 defaultKDConfig :: KDConfig
-defaultKDConfig = KDConfig { kdRibbonLength = 40
-                           , kdVerbose      = False
-                           , kdSolverConfig = defaultSMTCfg
+defaultKDConfig = KDConfig { kdRibbonLength    = 40
+                           , kdVerbose         = False
+                           , kdExtraSolverArgs = []
+                           , kdSolverConfig    = defaultSMTCfg
                            }
 
 -- | Run KD proof with z3 configuration.