From 36c86d9545b9ee0da1454e5645b2eba5184cdb7d Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 19 Mar 2024 13:12:53 +0100
Subject: [PATCH 1/3] compile lib_usage with `Dune`

---
 dune | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100644 dune

diff --git a/dune b/dune
deleted file mode 100644
index 261d36616..000000000
--- a/dune
+++ /dev/null
@@ -1 +0,0 @@
-(data_only_dirs examples)

From 6d63abdf886dbed097af6118c979bed275084085 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 19 Mar 2024 13:21:49 +0100
Subject: [PATCH 2/3] Update the lib_usage example

---
 examples/lib_usage.ml | 22 ++++++++--------------
 1 file changed, 8 insertions(+), 14 deletions(-)

diff --git a/examples/lib_usage.ml b/examples/lib_usage.ml
index 84084cb98..1a9079d3b 100644
--- a/examples/lib_usage.ml
+++ b/examples/lib_usage.ml
@@ -84,24 +84,18 @@ let typed, _env = Typechecker.type_file parsed
 
 let pbs = Typechecker.split_goals_and_cnf typed
 
-module SAT = Fun_sat.Make(Theory.Main_Default)
+module SAT = Fun_sat_frontend.Make(Theory.Main_Default)
 module FE = Frontend.Make(SAT)
 
 let () =
   List.iter
     (fun (pb, _goal_name) ->
        let ctxt = Frontend.init_all_used_context () in
-       let acc0 = SAT.empty (), `Unknown (SAT.empty ()), Explanation.empty in
-       let s = Stack.create () in
-       let _env, consistent, _ex =
-         List.fold_left
-           (fun acc d ->
-              FE.process_decl (fun _ _ -> ()) ctxt s acc d
-           ) acc0 pb
-       in
-       match consistent with
-       | `Sat _ | `Unknown _ ->
-         Format.printf "unknown"
+       let env = FE.init_env ctxt in
+       List.iter (FE.process_decl env) pb;
+       match env.res with
+       | `Sat | `Unknown ->
+         Format.printf "unknown@."
        | `Unsat ->
-         Format.printf "unsat"
-    )pbs
+         Format.printf "unsat@."
+    ) pbs

From b9ad2f99225cdd48e5c44bdb133ee6fc783ed420 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 19 Mar 2024 15:56:26 +0100
Subject: [PATCH 3/3] Add lib_usage in the package `alt-ergo-lib`

We add the executable `lib_usage` into the package `alt-ergo-lib`
but we don't install it.
---
 examples/dune | 1 +
 1 file changed, 1 insertion(+)

diff --git a/examples/dune b/examples/dune
index 52d46d10b..ccd2275e4 100644
--- a/examples/dune
+++ b/examples/dune
@@ -6,6 +6,7 @@
 
 (rule
  (alias runtest)
+ (package alt-ergo-lib)
  (action
   (ignore-stdout
    (ignore-stderr