Commit c5f1bb89 authored by MARCHE Claude's avatar MARCHE Claude

SMTv2 printer: do not print declarations of algebraic datatypes when they are...

SMTv2 printer: do not print declarations of algebraic datatypes when they are given in the syntax map
parent 4eed53de
...@@ -560,9 +560,8 @@ let print_data_decl info fmt (ts,cl) = ...@@ -560,9 +560,8 @@ let print_data_decl info fmt (ts,cl) =
let print_decl cntexample args info fmt d = match d.d_node with let print_decl cntexample args info fmt d = match d.d_node with
| Dtype ts -> | Dtype ts ->
print_type_decl info fmt ts print_type_decl info fmt ts
| Ddata [(ts,_)] when query_syntax info.info_syn ts.ts_name <> None -> ()
| Ddata dl -> | Ddata dl ->
(*unsupportedDecl d
"smtv2 : algebraic type are not supported" *)
fprintf fmt "@[(declare-datatypes ()@ (%a))@]@\n" fprintf fmt "@[(declare-datatypes ()@ (%a))@]@\n"
(print_list space (print_data_decl info)) dl (print_list space (print_data_decl info)) dl
| Dparam ls -> | Dparam ls ->
......
...@@ -110,6 +110,20 @@ theory Map ...@@ -110,6 +110,20 @@ theory Map
end end
theory TestBool
use import bool.Bool
goal g : forall b:bool. b = b
(*
bin/why3prove tests/test-poly.why -D why3_smt -T TestBool -G g
*)
end
theory TestTuple theory TestTuple
......
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