From dcafcf2bee8030e5308692accedf6e9b928986c4 Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Tue, 28 Nov 2023 14:37:23 -0800
Subject: [PATCH] Access to openSMT

---
 Data/SBV.hs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Data/SBV.hs b/Data/SBV.hs
index 3367eded9..54b6c1220 100644
--- a/Data/SBV.hs
+++ b/Data/SBV.hs
@@ -131,6 +131,8 @@
 --
 --   * DReal from CMU: <http://dreal.github.io/>
 --
+--   * OpenSMT from Università della Svizzera italiana <https://verify.inf.usi.ch/opensmt>
+--
 --   * Z3 from Microsoft: <http://github.com/Z3Prover/z3/wiki>
 --
 -- SBV requires recent versions of these solvers; please see the file
@@ -402,7 +404,7 @@ module Data.SBV (
   -- $verbosity
 
   -- ** Solvers
-  , boolector, bitwuzla, cvc4, cvc5, yices, dReal, z3, mathSAT, abc
+  , boolector, bitwuzla, cvc4, cvc5, yices, dReal, z3, mathSAT, abc, openSMT
   -- ** Configurations
   , defaultSolverConfig, defaultSMTCfg, defaultDeltaSMTCfg, sbvCheckSolverInstallation, getAvailableSolvers
   , setLogic, Logic(..), setOption, setInfo, setTimeOut