From 619da6fbcbf917f1ab5ec6fde1a75c9b6b71bcfd Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 23 Jun 2023 20:44:01 -0400
Subject: [PATCH] fix warnings

---
 src/main/pure_sat_solver.ml | 11 +++++------
 src/smtlib/Driver.ml        |  4 ++--
 src/smtlib/build_model.mli  |  1 -
 3 files changed, 7 insertions(+), 9 deletions(-)

diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml
index a1ede58a..dd047d6a 100644
--- a/src/main/pure_sat_solver.ml
+++ b/src/main/pure_sat_solver.ml
@@ -104,7 +104,9 @@ let tracer ~(sink : Tr.Sink.t) () : SAT.Tracer.t =
           dict_of_list
             [
               "id", int id;
-              "c", list (lits |> Iter.map self#sat_encode_lit |> Iter.to_rev_list);
+              ( "c",
+                list (lits |> Iter.map self#sat_encode_lit |> Iter.to_rev_list)
+              );
             ])
       in
       Tr.Sink.emit sink ~tag:"AssCSat" v
@@ -147,8 +149,7 @@ let tracer ~(sink : Tr.Sink.t) () : SAT.Tracer.t =
 
 let start = Sys.time ()
 
-let solve ?(check = false) (solver : SAT.t) :
-    (unit, string) result =
+let solve ?check:(_ = false) (solver : SAT.t) : (unit, string) result =
   let res = Profile.with_ "solve" (fun () -> SAT.solve solver) in
   let t2 = Sys.time () in
   Printf.printf "\r";
@@ -158,9 +159,7 @@ let solve ?(check = false) (solver : SAT.t) :
     let t3 = Sys.time () in
     Format.printf "Sat (%.3f/%.3f)@." (t2 -. start) (t3 -. t2)
   | SAT.Unsat _ ->
-
-      (* TODO: extract proof from trace; use check_proof *)
-
+    (* TODO: extract proof from trace; use check_proof *)
     let t3 = Sys.time () in
     Format.printf "Unsat (%.3f/%.3f)@." (t2 -. start) (t3 -. t2));
   Ok ()
diff --git a/src/smtlib/Driver.ml b/src/smtlib/Driver.ml
index 9a572b91..fc3a1b60 100644
--- a/src/smtlib/Driver.ml
+++ b/src/smtlib/Driver.ml
@@ -120,10 +120,10 @@ let solve (self : t) ~assumptions () : Solver.res =
     *);
 
     (match self.proof_file with
-    | Some file ->
+    | Some _file ->
       (match unsat_proof () with
       | None -> ()
-      | Some step_id ->
+      | Some _step_id ->
         (* TODO: read trace; emit proof
               let proof = Solver.proof self.solver in
               let proof_quip =
diff --git a/src/smtlib/build_model.mli b/src/smtlib/build_model.mli
index 448d70e7..fb857e35 100644
--- a/src/smtlib/build_model.mli
+++ b/src/smtlib/build_model.mli
@@ -1,4 +1,3 @@
-open Common_
 open! Sidekick_base
 
 type t