diff --git a/src/printers/vnnlib.ml b/src/printers/vnnlib.ml index 29758ee6ce16a920db6930c6c3e6fd5092e28258..45680a9b0371b9e94c53afb0ce8be590a607762d 100644 --- a/src/printers/vnnlib.ml +++ b/src/printers/vnnlib.ml @@ -477,11 +477,13 @@ let print_prop_decl info fmt prop_kind pr t = let print_param_decl info fmt ls = match Term.Hls.find_opt info.variables ls with + | None -> () | Some s -> Fmt.pf fmt ";; %s@\n" s; - Fmt.pf fmt "@[(declare-const %s %a)@]@\n@\n" s (print_type_value info) - ls.ls_value - | _ -> () + (* FIXME: The type should not be hardcoded as 'Real', but printed as: *) + (* 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 = match d.Decl.d_node with