From 45b32648b9039d2b124d3cb07ce4251dcd867167 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@inria.fr>
Date: Thu, 30 Apr 2015 16:13:38 +0200
Subject: Generic program to run the extracted checkers (basic error messages)

---
 src/extraction/smtcoq.ml | 32 ++++++++++++++++++--------------
 1 file changed, 18 insertions(+), 14 deletions(-)

diff --git a/src/extraction/smtcoq.ml b/src/extraction/smtcoq.ml
index b88a280..f3bd6b1 100644
--- a/src/extraction/smtcoq.ml
+++ b/src/extraction/smtcoq.ml
@@ -24,21 +24,25 @@ let verifier_of_solver = function
 let run s pb trace =
   Printf.printf "Calling the %s verifier on %s and %s...\n" (string_of_solver s) pb trace;
   let v = verifier_of_solver s in
-  let t1 = Unix.time () in
-  let res = v pb trace in
-  let t2 = Unix.time () in
-  if res then
-    Printf.printf "The trace was correctly verified in %fs\n" (t2 -. t1)
-  else
-    Printf.printf "The verifier failed to check the trace :-(\n"
+  try
+    let t1 = Unix.time () in
+    let res = v pb trace in
+    let t2 = Unix.time () in
+    if res then
+      Printf.printf "The trace was correctly verified in %fs\n" (t2 -. t1)
+    else
+      failwith "Error"
+  with | _ -> Printf.printf "The verifier failed to check the trace :-(\n"
 
 
 
 let _ =
-  try
-    let s = if Sys.argv.(1) = "-verit" then Verit else Zchaff in
-    let pb = Sys.argv.((Array.length Sys.argv)-2) in
-    let trace = Sys.argv.((Array.length Sys.argv)-1) in
-    run s pb trace
-  with
-    | _ -> Printf.printf "%s" usage; exit 0
+  let (s,pb,trace) =
+    try
+      let s = if Sys.argv.(1) = "-verit" then Verit else Zchaff in
+      let pb = Sys.argv.((Array.length Sys.argv)-2) in
+      let trace = Sys.argv.((Array.length Sys.argv)-1) in
+      (s,pb,trace)
+    with
+      | _ -> Printf.printf "%s" usage; exit 0 in
+  run s pb trace
-- 
cgit