Skip to content

GitLab

Commit d00dd702 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Yices: "nat" is built-in

parent 44a8424a
Show whitespace changes
Inline Side-by-side
src/printer/yices.ml
View file @ d00dd702
......@@ -40,7 +40,8 @@ let ident_printer =
(** for security *)
"bool";"unsat";"sat";"true";"false";
"true";"check";"assert";"TYPE";"SUBTYPE";
"scalar";"select";"update";"int";"real";"subtype";"subrange";"mk-bv";
"scalar";"select";"update";"int";"real";"nat";
"subtype";"subrange";"mk-bv";
"bv-concat";"bv-extract";"bv-shift-right0";"div";"mod";"bitvector";
"lambda";
]
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment