Skip to content

Commit

Permalink
Remove needless output format check
Browse files Browse the repository at this point in the history
In cc97897 we introduced an extra check for smtlib printing of types
that is no longer needed after 7df3738 .  This patch removes that extra
check.
  • Loading branch information
bclement-ocp committed Sep 29, 2023
1 parent e9f5e61 commit b422593
Showing 1 changed file with 1 addition and 3 deletions.
4 changes: 1 addition & 3 deletions src/lib/structures/ty.ml
Original file line number Diff line number Diff line change
Expand Up @@ -107,9 +107,7 @@ let print_generic body_of =
| Treal -> fprintf fmt "real"
| Tbool -> fprintf fmt "bool"
| Tunit -> fprintf fmt "unit"
| Tbitv n ->
if Options.get_output_smtlib () then fprintf fmt "(_ BitVec %d)" n
else fprintf fmt "bitv[%d]" n
| Tbitv n -> fprintf fmt "bitv[%d]" n
| Tvar{v=v ; value = None} -> fprintf fmt "'a_%d" v
| Tvar{v=v ; value = Some (Trecord { args = l; name = n; _ } as t) } ->
if Hashtbl.mem h v then
Expand Down

0 comments on commit b422593

Please sign in to comment.