From f7359a4fb90ecd992335d0c69fec5220c7500b27 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 24 May 2023 15:36:02 +0200
Subject: [PATCH] [printers] declare-const must have Real type in VNN-LIB
printer.
---
src/printers/vnnlib.ml | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/src/printers/vnnlib.ml b/src/printers/vnnlib.ml
index 29758ee..45680a9 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
--
GitLab