simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 20:25:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

tmp: use dummy proof in pure sat solver

Browse source
This commit is contained in:
Simon Cruanes 2021-08-20 18:45:39 -04:00
parent 4cada7e7b6
commit 22638a0c0b
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/main/main.ml
View file

@ -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