add bitwuzla as a solver

Author: vrindisbacher

src/Language/Fixpoint/Smt/Interface.hs

@@ -306,6 +306,10 @@ makeContext' cfg ctxLog
                       Process.defaultConfig
                              { Process.exe = "cvc5"
                              , Process.args = ["--incremental", "-L", "smtlib2"] }
+         Bitwuzla    -> makeProcess ctxLog $
+                      Process.defaultConfig
+                             { Process.exe = "bitwuzla"
+                             , Process.args = ["--lang", "smt2"] }
        solver <- SMTLIB.Backends.initSolver SMTLIB.Backends.Queuing backend
        loud <- isLoud
        return Ctx { ctxSolver  = solver
@@ -457,7 +461,8 @@ makeMbqi cfg
 z3_options :: [Builder]
 z3_options
   = [ "(set-option :auto-config false)"
-    , "(set-option :model true)" ]
+    , "(set-option :model true)"
+    , "(set-option :sat.smt true)" ]
 
 
 

src/Language/Fixpoint/Types/Config.hs

@@ -146,7 +146,7 @@ instance Read RESTOrdering where
 
 ---------------------------------------------------------------------------------------
 
-data SMTSolver = Z3 | Z3mem | Cvc4 | Cvc5 | Mathsat 
+data SMTSolver = Z3 | Z3mem | Cvc4 | Cvc5 | Mathsat | Bitwuzla
                  deriving (Eq, Data, Typeable, Generic)
 
 instance Default SMTSolver where
@@ -158,6 +158,7 @@ instance Show SMTSolver where
   show Cvc4    = "cvc4"
   show Cvc5    = "cvc5"
   show Mathsat = "mathsat"
+  show Bitwuzla = "bitwuzla"
 
 instance S.Store SMTSolver