From 22638a0c0b5b00abdd21e1d85c758806e960eeed Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 20 Aug 2021 18:45:39 -0400
Subject: [PATCH] tmp: use dummy proof in pure sat solver

---
 src/main/main.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/main/main.ml b/src/main/main.ml
index eaf0ac5d..f14fe697 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -143,9 +143,10 @@ let main_smt () : _ result =
 let main_cnf () : _ result =
   let module Proof = Pure_sat_solver.Proof in
   let module S = Pure_sat_solver in
-  let proof = Proof.create() in
+  (* TODO: switch proof depending on whether we need proofs or not *)
+  let proof = Proof.dummy in
 
-  (* FIXME: this should go in the proof module *)
+  (* FIXME: this should go in the proof module, or is already redundant? *)
   let close_proof_, on_learnt, on_gc =
     if !proof_file ="" then (
       (fun() -> ()), None, None