From 769c2054cc14af50e70a38b0d2340ae6170863e0 Mon Sep 17 00:00:00 2001
From: QGarchery <QGarchery@users.noreply.github.com>
Date: Tue, 12 Feb 2019 10:32:49 +0100
Subject: equalities on array and bv types (#34)

---
 src/trace/smtAtom.ml     | 8 ++++----
 src/verit/veritSyntax.ml | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index a80e8b7..fd9f2bd 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -1202,12 +1202,12 @@ module Atom =
       and mk_bop_bveq = function
         | [s;a1;a2] when SL.mem LBitvectors known_logic ->
           let s' = mk_bvsize s in
-          mk_bop (BO_eq (TBV s')) [a1;a2]
+          mk_teq (TBV s') [a1;a2]
         (* We still want to interpret bv equality as uninterpreted
            smtlib2 equality if the solver doesn't support bitvectors *)
         | [s;a1;a2] ->
           let ty = SmtBtype.of_coq rt known_logic (mklApp cbitvector [|s|]) in
-          mk_bop (BO_eq ty) [a1;a2]
+          mk_teq ty [a1;a2]
         | _ -> assert false
 
       and mk_bop_select = function
@@ -1235,13 +1235,13 @@ module Atom =
         | [ti;te;_;_;_;_;_;a;b] when SL.mem LArrays known_logic ->
           let ti' = SmtBtype.of_coq rt known_logic ti in
           let te' = SmtBtype.of_coq rt known_logic te in
-          mk_bop (BO_eq (TFArray (ti', te'))) [a; b]
+          mk_teq (TFArray (ti', te')) [a; b]
         (* We still want to interpret array equality as uninterpreted
            smtlib2 equality if the solver doesn't support arrays *)
         | [ti;te;ord_ti;_;_;_;inh_te;a;b] ->
           let ty = SmtBtype.of_coq rt known_logic
               (mklApp cfarray [|ti; te; ord_ti; inh_te|]) in
-          mk_bop (BO_eq ty) [a;b]
+          mk_teq ty [a;b]
         | _ -> assert false
 
       and mk_unknown c args ty =
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"
-- 
cgit