diff --git a/doc/guide.md b/doc/guide.md
index 6514550c..12caf666 100644
--- a/doc/guide.md
+++ b/doc/guide.md
@@ -209,12 +209,8 @@ We start with `p = q`.
 # Solver.solve ~assumptions:[] solver;;
 - : Solver.res =
 Sidekick_smt_solver.Solver.Sat
- (model
-  (p := true)
-  (q := true)
-  (true := true)
-  (false := false)
-  ([[ (= p q) ]] := true))
+ {Sidekick_smt_solver.Solver.get_value = <fun>; iter_classes = <fun>;
+  eval_lit = <fun>; iter_true_lits = <fun>}
 ```
 
 It is satisfiable, and we got a model where "p" and "q" are both false.
@@ -246,12 +242,8 @@ Note that this doesn't affect satisfiability without assumptions:
 # Solver.solve ~assumptions:[] solver;;
 - : Solver.res =
 Sidekick_smt_solver.Solver.Sat
- (model
-  (p := true)
-  (q := true)
-  (true := true)
-  (false := false)
-  ([[ (= p q) ]] := true))
+ {Sidekick_smt_solver.Solver.get_value = <fun>; iter_classes = <fun>;
+  eval_lit = <fun>; iter_true_lits = <fun>}
 ```
 
 We can therefore add more formulas and see where it leads us.
@@ -264,14 +256,8 @@ We can therefore add more formulas and see where it leads us.
 # Solver.solve ~assumptions:[] solver;;
 - : Solver.res =
 Sidekick_smt_solver.Solver.Sat
- (model
-  (p := true)
-  (q := true)
-  (r := true)
-  (true := true)
-  (false := false)
-  ([[ (= p q) ]] := true)
-  ([[ (or r (not p) false) ]] := true))
+ {Sidekick_smt_solver.Solver.get_value = <fun>; iter_classes = <fun>;
+  eval_lit = <fun>; iter_true_lits = <fun>}
 ```
 
 Still satisfiable, but now we see `r` in the model, too. And now:
@@ -331,13 +317,8 @@ We can play with assertions now:
 # Solver.solve ~assumptions:[] solver;;
 - : Solver.res =
 Sidekick_smt_solver.Solver.Sat
- (model
-  (true := true)
-  (false := false)
-  (a := 0)
-  (b := 0)
-  ([[ (<= (+ a ((* -1) b)) 0) ]] := true)
-  ($_le_comb[0] := 0))
+ {Sidekick_smt_solver.Solver.get_value = <fun>; iter_classes = <fun>;
+  eval_lit = <fun>; iter_true_lits = <fun>}
 
 
 # let a_geq_1 = LRA_term.geq tstore a (LRA_term.const tstore (Q.of_int 1));;
diff --git a/src/smt/model.ml b/src/smt/model.ml
index 259d9c53..dc93a338 100644
--- a/src/smt/model.ml
+++ b/src/smt/model.ml
@@ -9,5 +9,18 @@ open Sigs
 
 type t = { eval: Term.t -> value option; map: value Term.Map.t }
 
+let is_empty self = Term.Map.is_empty self.map
+
 let eval (self : t) (t : Term.t) : value option =
   try Some (Term.Map.find t self.map) with Not_found -> self.eval t
+
+let pp out (self : t) =
+  if is_empty self then
+    Fmt.string out "(model)"
+  else (
+    let pp_pair out (t, v) =
+      Fmt.fprintf out "(@[<1>%a@ := %a@])" Term.pp t Term.pp v
+    in
+    Fmt.fprintf out "(@[<hv>model@ %a@])" (Util.pp_iter pp_pair)
+      (Term.Map.to_iter self.map)
+  )
diff --git a/src/smtlib/build_model.ml b/src/smtlib/build_model.ml
index 67f6c953..13c09dc9 100644
--- a/src/smtlib/build_model.ml
+++ b/src/smtlib/build_model.ml
@@ -1,4 +1,3 @@
-open Common_
 open! Sidekick_base
 
 type t = { fun_symbols: unit Term.Tbl.t; ty_symbols: unit Term.Tbl.t }