From 931f74c27d80b0a0f023b3d0c183f1bf3e645655 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Wed, 6 Nov 2024 08:52:09 +0000 Subject: [PATCH 1/2] Bump bitwuzla conflict 0.4.0 -> 0.6.0 --- dune-project | 2 +- smtml.opam | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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: [ From aa3f118c9738f245816d3159c47932675e2580cc Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Wed, 6 Nov 2024 09:10:52 +0000 Subject: [PATCH 2/2] Remove leaky hack in bitwuzla's mappigns --- src/bitwuzla_mappings.default.ml | 17 +---------------- 1 file changed, 1 insertion(+), 16 deletions(-) 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