From 296e3c78c2d56f0e08d654cb473f86f5b24375f4 Mon Sep 17 00:00:00 2001 From: QGarchery Date: Thu, 7 Feb 2019 19:30:58 +0100 Subject: Fix passing the goal strongly hashed (in ra' rf') instead of normal goal (hashed in ra rf) (#28) Fix flatten hashing in the wrong table veriT now has a happy ending added a debug_coq file --- src/verit/veritSyntax.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/verit/veritSyntax.ml') diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml index c4427b7..32e03f8 100644 --- a/src/verit/veritSyntax.ml +++ b/src/verit/veritSyntax.ml @@ -575,7 +575,7 @@ let init_index lsmt re_hash = let find = Hashtbl.find form_index_init_rank in let rec walk rank = function | [] -> () - | h::t -> add (Form.to_lit h) rank; + | h::t -> add (Form.to_lit (re_hash h)) rank; walk (rank+1) t in walk 1 lsmt; fun hf -> let re_hf = re_hash hf in @@ -584,7 +584,7 @@ let init_index lsmt re_hash = let oc = open_out "/tmp/input_not_found.log" in let fmt = Format.formatter_of_out_channel oc in List.iter (fun h -> Format.fprintf fmt "%a\n" hform_to_smt h) lsmt; - Format.fprintf fmt "\n%a\n" hform_to_smt re_hf; + Format.fprintf fmt "\n%a\n@." hform_to_smt re_hf; flush oc; close_out oc; failwith "not found: log available" -- cgit