Skip to content
Snippets Groups Projects
Commit f7359a4f authored by Michele Alberti's avatar Michele Alberti
Browse files

[printers] declare-const must have Real type in VNN-LIB printer.

parent 54db081e
No related branches found
No related tags found
No related merge requests found
...@@ -477,11 +477,13 @@ let print_prop_decl info fmt prop_kind pr t = ...@@ -477,11 +477,13 @@ let print_prop_decl info fmt prop_kind pr t =
let print_param_decl info fmt ls = let print_param_decl info fmt ls =
match Term.Hls.find_opt info.variables ls with match Term.Hls.find_opt info.variables ls with
| None -> ()
| Some s -> | Some s ->
Fmt.pf fmt ";; %s@\n" s; Fmt.pf fmt ";; %s@\n" s;
Fmt.pf fmt "@[(declare-const %s %a)@]@\n@\n" s (print_type_value info) (* FIXME: The type should not be hardcoded as 'Real', but printed as: *)
ls.ls_value (* Fmt.pf fmt "@[(declare-const %s %a)@]@\n@\n" s (print_type_value info) *)
| _ -> () (* ls.ls_value *)
Fmt.pf fmt "@[(declare-const %s Real)@]@\n@\n" s
let print_decl info fmt d = let print_decl info fmt d =
match d.Decl.d_node with match d.Decl.d_node with
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment