verit also works when it doesn't use the conclusion (#24)

Fixes issue #20

1 files changed, 3 insertions, 28 deletions

diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 8eb1b60..16968cc 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -38,31 +38,6 @@ exception Import_trace of int
 let get_val = function
     Some a -> a
   | None -> assert false
-
-(* For debugging certif processing : <add_scertif> <select> <occur> <alloc> *)
-let print_certif c where=
-  let r = ref c in
-  let out_channel = open_out where in
-  let fmt = Format.formatter_of_out_channel out_channel in
-  let continue = ref true in
-  while !continue do
-    let kind = to_string (!r.kind) in
-    let id = !r.id in
-    let pos = match !r.pos with
-      | None -> "None"
-      | Some p -> string_of_int p in
-    let used = !r.used in
-    Format.fprintf fmt "id:%i kind:%s pos:%s used:%i value:" id kind pos used;
-    begin match !r.value with
-    | None -> Format.fprintf fmt "None"
-    | Some l -> List.iter (fun f -> Form.to_smt Atom.to_string fmt f;
-                                    Format.fprintf fmt " ") l end;
-    Format.fprintf fmt "\n";
-    match !r.next with
-    | None -> continue := false
-    | Some n -> r := n 
-  done;
-  Format.fprintf fmt "@."; close_out out_channel
                             
 let import_trace ra' rf' filename first lsmt =
   let chan = open_in filename in
@@ -91,13 +66,13 @@ let import_trace ra' rf' filename first lsmt =
        begin match first with
        | None -> ()
        | Some _ ->
-          let cf, lr = order_roots (VeritSyntax.init_index lsmt re_hash)
-                         !cfirst in
+          let init_index = VeritSyntax.init_index lsmt re_hash in
+          let cf, lr = order_roots init_index !cfirst in
           cfirst := cf;
           let to_add = VeritSyntax.qf_to_add (List.tl lr) in
           let to_add =
             (match first, !cfirst.value with
-             | Some (root, l), Some [fl] when not (Form.equal l (re_hash fl)) ->
+             | Some (root, l), Some [fl] when init_index fl = 1 && not (Form.equal l (re_hash fl)) ->
                 let cfirst_value = !cfirst.value in
                 !cfirst.value <- root.value;
                 [Other (ImmFlatten (root, fl)), cfirst_value, !cfirst]