diff options
| -rw-r--r-- | src/trace/smtAtom.ml | 8 | ||||
| -rw-r--r-- | src/verit/veritSyntax.ml | 2 | ||||
| -rw-r--r-- | unit-tests/Tests_lfsc.v | 20 |
3 files changed, 14 insertions, 16 deletions
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" diff --git a/unit-tests/Tests_lfsc.v b/unit-tests/Tests_lfsc.v index 48d2d2b..05a9fb4 100644 --- a/unit-tests/Tests_lfsc.v +++ b/unit-tests/Tests_lfsc.v @@ -46,12 +46,11 @@ Local Open Scope bv_scope. smt. Qed. - (* TODO: will be ok when symmetry of equality is back for verit *) - (* Goal forall (bv1 bv2: bitvector 4), *) - (* bv1 = bv2 <-> bv2 = bv1. *) - (* Proof. *) - (* smt. *) - (* Qed. *) + Goal forall (bv1 bv2: bitvector 4), + bv1 = bv2 <-> bv2 = bv1. + Proof. + smt. + Qed. End BV. @@ -689,11 +688,10 @@ Section A_BV_EUF_LIA_PR. smt. Qed. - (* TODO: will be ok when symmetry of equality is back for verit *) - (* Goal forall (a b: farray Z Z), a = b <-> b = a. *) - (* Proof. *) - (* smt. *) - (* Qed. *) + Goal forall (a b: farray Z Z), a = b <-> b = a. + Proof. + smt. + Qed. End A_BV_EUF_LIA_PR. |