From 24bbcb3fbb0655e5999fcaccf8f68167520c3e0a Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 15 Oct 2022 23:15:42 -0400 Subject: [PATCH] improve model printing so it's more smtlib2.6 compatible --- src/smtlib/model.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/smtlib/model.ml b/src/smtlib/model.ml index 141a8fa4..24142337 100644 --- a/src/smtlib/model.ml +++ b/src/smtlib/model.ml @@ -41,7 +41,7 @@ let rec eval t (self : t) : value option = let pp out (self : t) = if is_empty self then - Fmt.string out "(model)" + Fmt.string out "()" else ( let rec pp_entries out = function | [] -> () @@ -72,6 +72,5 @@ let pp out (self : t) = (List.mapi (fun i v -> i, Term.ty v) args) Term.pp (Term.ty v) pp_entries (TL_map.to_list entries) in - Fmt.fprintf out "(@[model@ %a@])" (Util.pp_iter pp_fun) - (TM.to_iter self.m) + Fmt.fprintf out "(@[%a@])" (Util.pp_iter pp_fun) (TM.to_iter self.m) )