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/trace/smtAtom.ml | |
| parent | 9e1615b8bdd080f2331bce6b62f5f243950e43d7 (diff) | |
| download | smtcoq-769c2054cc14af50e70a38b0d2340ae6170863e0.tar.gz smtcoq-769c2054cc14af50e70a38b0d2340ae6170863e0.zip | |
equalities on array and bv types (#34)
Diffstat (limited to 'src/trace/smtAtom.ml')
| -rw-r--r-- | src/trace/smtAtom.ml | 8 |
1 files changed, 4 insertions, 4 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 = |