From d6c6331d85f0cd93c4b76b2b6fd2d9e11468987b Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Thu, 28 Jul 2016 11:10:31 +0200
Subject: [PATCH] check proofs in `test_api`

---
 tests/test_api.ml | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/tests/test_api.ml b/tests/test_api.ml
index 4ecc4437..74f36e37 100644
--- a/tests/test_api.ml
+++ b/tests/test_api.ml
@@ -57,22 +57,32 @@ module type BASIC_SOLVER = sig
   val assume : ?tag:int -> F.t list list -> unit
 end
 
+exception Incorrect_model
+
 let mk_solver (s:solver): (module BASIC_SOLVER) =
   match s with
     | Smt ->
       let module S = struct
         include Smt.Make(struct end)
         let solve ?assumptions ()= match solve ?assumptions() with
-          | Sat _ -> R_sat
-          | Unsat _ -> R_unsat
+          | Sat _ ->
+            R_sat
+          | Unsat us ->
+            let p = us.Solver_intf.get_proof () in
+            Proof.check p;
+            R_unsat
       end
       in (module S)
     | Mcsat ->
       let module S = struct
         include Mcsat.Make(struct end)
         let solve ?assumptions ()= match solve ?assumptions() with
-          | Sat _ -> R_sat
-          | Unsat _ -> R_unsat
+          | Sat _ ->
+            R_sat
+          | Unsat us ->
+            let p = us.Solver_intf.get_proof () in
+            Proof.check p;
+            R_unsat
       end
       in (module S)