some fixes to model printing

[zapashcanon]

this is breaking a lot of tests but this is because they seem to be calling Value.pp directly instead of calling something more high-level (like Model.pp I would say ?). Let me know what you think. :)

[filipeom]

this is breaking a lot of tests but this is because they seem to be calling Value.pp directly instead of calling something more high-level (like Model.pp I would say ?). Let me know what you think. :)

Ah thanks! I forgot to do the pp_no_type 😞 I should have tested the printing of the scfg models. Anyway, I think for the failing tests we can just promote.

I would only suggest the follwing patch:

diff --git a/src/solvers/model.ml b/src/solvers/model.ml
index 6a7f858..c783718 100644
--- a/src/solvers/model.ml
+++ b/src/solvers/model.ml
@@ -23,10 +23,10 @@ let pp_bindings fmt ?(no_values = false) model =
   Fmt.list
     ~sep:(fun fmt () -> Fmt.pf fmt "@\n")
     (fun fmt (key, data) ->
-      if not no_values then Fmt.pf fmt "(%a %a)" Symbol.pp key Value.pp data
-      else
-        let t = Symbol.type_of key in
-        Fmt.pf fmt "(%a %a)" Symbol.pp key Ty.pp t )
+      let t = Symbol.type_of key in
+      if not no_values then
+        Fmt.pf fmt "(%a %a %a)" Symbol.pp key Ty.pp t Value.pp data
+      else Fmt.pf fmt "(%a %a)" Symbol.pp key Ty.pp t )
     fmt (get_bindings model)

 let pp ?(no_values = false) fmt model =

[zapashcanon]

Thanks, I applied your patch. I'm getting some failures on the tests because I'm missing some pinned stuff. Do you think you could run+promote them for me ? My hard drive is completely full and I can't install more stuff right now... 😅

[filipeom]

Thanks, I applied your patch. I'm getting some failures on the tests because I'm missing some pinned stuff. Do you think you could run+promote them for me ? My hard drive is completely full and I can't install more stuff right now... 😅

Ah yes, sorry! I can finish it from here. Thank you very much! 😃