From 1c4129e24bbdeb70a2022b09029805f14eea05a9 Mon Sep 17 00:00:00 2001
From: Arthur Carcano <arthur.carcano@ocamlpro.com>
Date: Thu, 27 Jun 2024 15:40:45 +0200
Subject: [PATCH] Add conflicts on solvers versions outside depopt range

We want to nudge our users to install versions of the solvers that are
actually compatible with smtml. To this end, I added a conflict with
solver versions that are outside of the depopt range.
---
 dune-project | 11 ++++++++++-
 smtml.opam   |  6 +++++-
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/dune-project b/dune-project
index 96f08b63..8b5feba7 100644
--- a/dune-project
+++ b/dune-project
@@ -22,15 +22,24 @@
  (synopsis "A Front-end library for SMT solvers in OCaml")
  (description "A Multi Back-end Front-end for SMT Solvers in OCaml.")
  ; Optional solver dependencies
+ ; Change here sould be mirrored in "conflicts"
  (depopts
   (z3
    (and
     (>= "4.12.2")
-    (<= "4.13")))
+    (< "4.14")))
   colibri2
   (bitwuzla-cxx
    (>= "0.4.0"))
   cvc5)
+ (conflicts
+  (z3
+   (or
+    (< "4.12.2")
+    (>= "4.14")))
+   (bitwuzla-cxx
+    (< "0.4.0"))
+ )
  (depends
   dune
   (ocaml
diff --git a/smtml.opam b/smtml.opam
index 5c5cf81b..eff16af7 100644
--- a/smtml.opam
+++ b/smtml.opam
@@ -20,11 +20,15 @@ depends: [
   "bisect_ppx" {with-test & >= "2.5.0"}
 ]
 depopts: [
-  "z3" {>= "4.12.2" & <= "4.13"}
+  "z3" {>= "4.12.2" & < "4.14"}
   "colibri2"
   "bitwuzla-cxx" {>= "0.4.0"}
   "cvc5"
 ]
+conflicts: [
+  "z3" {< "4.12.2" | >= "4.14"}
+  "bitwuzla-cxx" {< "0.4.0"}
+]
 build: [
   ["dune" "subst"] {dev}
   [