diff --git a/dune-project b/dune-project index 82fa7de7..0d664aa8 100644 --- a/dune-project +++ b/dune-project @@ -40,7 +40,7 @@ z3) (conflicts (bitwuzla-cxx - (< "0.4.0")) + (< "0.6.0")) (z3 (or (< "4.12.2") diff --git a/smtml.opam b/smtml.opam index 4c4f9d7b..de0eb7b0 100644 --- a/smtml.opam +++ b/smtml.opam @@ -46,7 +46,7 @@ depends: [ ] depopts: ["alt-ergo-lib" "bitwuzla-cxx" "colibri2" "cvc5" "z3"] conflicts: [ - "bitwuzla-cxx" {< "0.4.0"} + "bitwuzla-cxx" {< "0.6.0"} "z3" {< "4.12.2" | >= "4.14"} ] build: [ diff --git a/src/bitwuzla_mappings.default.ml b/src/bitwuzla_mappings.default.ml index 712b8a0f..e36bb975 100644 --- a/src/bitwuzla_mappings.default.ml +++ b/src/bitwuzla_mappings.default.ml @@ -4,15 +4,6 @@ include Mappings_intf -(* Hack: this was a hack to try and run bitwuzla in Owi *) -let leak = - let leaky_list = ref [] in - let mutex = Mutex.create () in - fun module_ -> - Mutex.lock mutex; - leaky_list := module_ :: !leaky_list; - Mutex.unlock mutex - module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct open B @@ -511,13 +502,7 @@ end include ( Mappings.Make (struct - module Make () = struct - let bitwuzla = (module Bitwuzla_cxx.Make () : Bitwuzla_cxx.S) - - let () = leak bitwuzla - - include Fresh_bitwuzla ((val bitwuzla)) - end + module Make () = Fresh_bitwuzla (Bitwuzla_cxx.Make ()) let is_available = true