diff options
| author | QGarchery <QGarchery@users.noreply.github.com> | 2019-02-12 10:32:49 +0100 |
|---|---|---|
| committer | ckeller <ckeller@users.noreply.github.com> | 2019-02-12 10:32:49 +0100 |
| commit | 769c2054cc14af50e70a38b0d2340ae6170863e0 (patch) | |
| tree | d8ea9b89f915d195cbd0ddd4d73520df6c9706ea /src/verit/veritSyntax.ml | |
| parent | 9e1615b8bdd080f2331bce6b62f5f243950e43d7 (diff) | |
| download | smtcoq-769c2054cc14af50e70a38b0d2340ae6170863e0.tar.gz smtcoq-769c2054cc14af50e70a38b0d2340ae6170863e0.zip | |
equalities on array and bv types (#34)
Diffstat (limited to 'src/verit/veritSyntax.ml')
| -rw-r--r-- | src/verit/veritSyntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml index 32e03f8..e209fd2 100644 --- a/src/verit/veritSyntax.ml +++ b/src/verit/veritSyntax.ml @@ -583,7 +583,7 @@ let init_index lsmt re_hash = with Not_found -> 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; + List.iter (fun h -> Format.fprintf fmt "%a\n" hform_to_smt (re_hash h)) lsmt; Format.fprintf fmt "\n%a\n@." hform_to_smt re_hf; flush oc; close_out oc; failwith "not found: log available" |