diff --git a/lib/check.ml b/lib/check.ml
index 9bf499d54..a188aeb53 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -391,7 +391,8 @@ let check_conv_int loc ~expect ct arg =
   let fail_unrepresentable () =
     let@ model = model () in
     fail (fun ctxt ->
-      { loc; msg = Int_unrepresentable { value = arg; ict = ct; ctxt; model } })
+      let report = Explain.trace ctxt model Explain.no_ex in
+      { loc; msg = Int_unrepresentable { value = arg; ict = ct; report } })
   in
   let bt = IT.get_bt arg in
   (* TODO: can we (later) optimise this? *)
@@ -434,7 +435,9 @@ let check_has_alloc_id loc ptr ub_unspec =
     | `False ->
       let@ model = model () in
       let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in
-      fail (fun ctxt -> { loc; msg = Needs_alloc_id { ptr; ub; ctxt; model } })
+      fail (fun ctxt ->
+        let report = Explain.trace ctxt model Explain.no_ex in
+        { loc; msg = Needs_alloc_id { ptr; ub; report } })
   else
     return ()
 
@@ -463,7 +466,9 @@ let check_both_eq_alloc loc arg1 arg2 ub =
   match provable @@ LC.T both_alloc with
   | `False ->
     let@ model = model () in
-    fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } })
+    fail (fun ctxt ->
+      let report = Explain.trace ctxt model Explain.no_ex in
+      { loc; msg = Undefined_behaviour { ub; report } })
   | `True -> return ()
 
 
@@ -485,7 +490,13 @@ let check_live_alloc_bounds ?(skip_live = false) reason loc ub ptrs =
       let@ model = model () in
       fail (fun ctxt ->
         let term = if List.length ptrs = 1 then List.hd ptrs else IT.tuple_ ptrs here in
-        { loc; msg = Alloc_out_of_bounds { constr; term; ub; ctxt; model } })
+        let report =
+          Explain.trace
+            ctxt
+            model
+            Explain.{ no_ex with unproven_constraint = Some (LC.T constr) }
+        in
+        { loc; msg = Alloc_out_of_bounds { constr; term; ub; report } })
   else
     return ()
 
@@ -660,7 +671,9 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m =
         | `False ->
           let@ model = model () in
           let ub = CF.Undefined.UB045a_division_by_zero in
-          fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } }))
+          fail (fun ctxt ->
+            let report = Explain.trace ctxt model Explain.no_ex in
+            { loc; msg = Undefined_behaviour { ub; report } }))
      | OpRem_t ->
        let@ () = WellTyped.ensure_base_type loc ~expect (Mu.bt_of_pexpr pe1) in
        let@ () = WellTyped.ensure_bits_type loc expect in
@@ -675,7 +688,9 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m =
         | `False ->
           let@ model = model () in
           let ub = CF.Undefined.UB045b_modulo_by_zero in
-          fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } }))
+          fail (fun ctxt ->
+            let report = Explain.trace ctxt model Explain.no_ex in
+            { loc; msg = Undefined_behaviour { ub; report } }))
      | OpEq ->
        let@ () = WellTyped.ensure_base_type loc ~expect Bool in
        let@ () =
@@ -882,7 +897,9 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m =
       | `False ->
         let@ model = model () in
         let ub = CF.Undefined.UB036_exceptional_condition in
-        fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } })
+        fail (fun ctxt ->
+          let report = Explain.trace ctxt model Explain.no_ex in
+          { loc; msg = Undefined_behaviour { ub; report } })
     in
     return direct_x
   | PEconv_int (ct_expr, pe) | PEconv_loaded_int (ct_expr, pe) ->
@@ -915,7 +932,9 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m =
      | `False ->
        let@ model = model () in
        let ub = CF.Undefined.UB036_exceptional_condition in
-       fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } }))
+       fail (fun ctxt ->
+         let report = Explain.trace ctxt model Explain.no_ex in
+         { loc; msg = Undefined_behaviour { ub; report } }))
   | PEis_representable_integer (pe, act) ->
     let@ () = WellTyped.check_ct act.loc act.ct in
     let@ () = WellTyped.ensure_base_type loc ~expect Bool in
@@ -972,7 +991,9 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m =
      | `True -> return (default_ expect loc)
      | `False ->
        let@ model = model () in
-       fail (fun ctxt -> { loc; msg = Undefined_behaviour { ub; ctxt; model } }))
+       fail (fun ctxt ->
+         let report = Explain.trace ctxt model Explain.no_ex in
+         { loc; msg = Undefined_behaviour { ub; report } }))
   | PEerror (err, _pe) ->
     let@ provable = provable loc in
     let here = Locations.other __LOC__ in
@@ -980,7 +1001,9 @@ let rec check_pexpr (pe : BT.t Mu.pexpr) : IT.t m =
      | `True -> return (default_ expect loc)
      | `False ->
        let@ model = model () in
-       fail (fun ctxt -> { loc; msg = StaticError { err; ctxt; model } }))
+       fail (fun ctxt ->
+         let report = Explain.trace ctxt model Explain.no_ex in
+         { loc; msg = StaticError { err; report } }))
 
 
 module Spine : sig
@@ -1137,8 +1160,8 @@ let all_empty loc _original_resources =
     let@ simp_ctxt = simp_ctxt () in
     RI.debug_constraint_failure_diagnostics 6 model simp_ctxt constr;
     fail (fun ctxt ->
-      (* let ctxt = { ctxt with resources = original_resources } in *)
-      { loc; msg = Unused_resource { resource; ctxt; model } })
+      let report = Explain.trace ctxt model Explain.no_ex in
+      { loc; msg = Unused_resource { resource; report } })
 
 
 let load loc pointer ct =
@@ -1421,7 +1444,8 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
              let@ model = model () in
              fail (fun ctxt ->
                let ict = act_to.ct in
-               { loc; msg = Int_unrepresentable { value = arg; ict; ctxt; model } })
+               let report = Explain.trace ctxt model Explain.no_ex in
+               { loc; msg = Int_unrepresentable { value = arg; ict; report } })
          in
          k actual_value)
      | PtrFromInt (act_from, act_to, pe) ->
@@ -1622,9 +1646,10 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
              | `False ->
                let@ model = model () in
                fail (fun ctxt ->
+                 let report = Explain.trace ctxt model Explain.no_ex in
                  let msg =
                    Write_value_unrepresentable
-                     { ct = act.ct; location = parg; value = varg; ctxt; model }
+                     { ct = act.ct; location = parg; value = varg; report }
                  in
                  { loc; msg })
            in
@@ -1964,10 +1989,16 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
            RI.debug_constraint_failure_diagnostics 6 model simp_ctxt lc;
            let@ () = Diagnostics.investigate model lc in
            fail (fun ctxt ->
+             let report =
+               Explain.trace
+                 ctxt
+                 model
+                 Explain.{ no_ex with unproven_constraint = Some lc }
+             in
              { loc;
                msg =
                  Unproven_constraint
-                   { constr = lc; info = (loc, None); requests = []; ctxt; model }
+                   { constr = lc; info = (loc, None); requests = []; report }
              }))
       | Inline _nms -> return ()
       | Print it ->
diff --git a/lib/explain.ml b/lib/explain.ml
index 475e4e8be..1a2f5ff55 100644
--- a/lib/explain.ml
+++ b/lib/explain.ml
@@ -331,46 +331,51 @@ let state (ctxt : C.t) log model_with_q extras =
       (Rp.add_labeled Rp.lab_uninteresting uninteresting Rp.labeled_empty)
   in
   let invalid_resources =
-    let g = ctxt.global in
-    let defs = g.resource_predicates in
-    let check (rt, o) =
-      match (rt, o) with
-      | Req.Q _, _ -> None
-      | Req.P { name = Owned _; pointer = _; iargs = _ }, _ -> None
-      | Req.P { name = PName s; pointer = _; iargs }, Resource.O it ->
-        (match (Sym.Map.find_opt s defs, evaluate it) with
-         | Some def, Some cand ->
-           let here = Locations.other __LOC__ in
-           let ptr_val = Req.get_pointer rt in
-           let ptr_def = (IT.sym_ (def.pointer, IT.get_bt ptr_val, here), ptr_val) in
-           Some (CP.check_pred s def cand ctxt iargs (ptr_def :: vals), rt, it)
-         | Some _, None ->
-           Some
-             ( CP.Result.error (!^"Could not locate definition of variable" ^^^ IT.pp it),
-               rt,
-               it )
-         | None, _ ->
-           Some
-             ( CP.Result.error (!^"Could not locate definition of predicate" ^^^ Sym.pp s),
-               rt,
-               it ))
-    in
-    let checked = List.filter_map check (C.get_rs ctxt) in
-    let nos, _ = List.partition (fun (r, _, _) -> CP.Result.is_no r) checked in
-    (* let yeses, unknown = List.partition (fun (r, _, _) -> is_yes r) rest in *)
-    (* Issue #900 *)
-    let pp_checked_res (p, req, cand) =
-      let _ = p in
-      let rslt = Req.pp req ^^^ !^"(" ^^^ IT.pp cand ^^^ !^")" in
-      Rp.
-        { original = rslt;
-          (* !^"Full predicate check output: "
+    (* temporarily disable these checks *)
+    if true then
+      Rp.labeled_empty
+    else (
+      let g = ctxt.global in
+      let defs = g.resource_predicates in
+      let check (rt, o) =
+        match (rt, o) with
+        | Req.Q _, _ -> None
+        | Req.P { name = Owned _; pointer = _; iargs = _ }, _ -> None
+        | Req.P { name = PName s; pointer = _; iargs }, Resource.O it ->
+          (match (Sym.Map.find_opt s defs, evaluate it) with
+           | Some def, Some cand ->
+             let here = Locations.other __LOC__ in
+             let ptr_val = Req.get_pointer rt in
+             let ptr_def = (IT.sym_ (def.pointer, IT.get_bt ptr_val, here), ptr_val) in
+             Some (CP.check_pred s def cand ctxt iargs (ptr_def :: vals), rt, it)
+           | Some _, None ->
+             Some
+               ( CP.Result.error (!^"Could not locate definition of variable" ^^^ IT.pp it),
+                 rt,
+                 it )
+           | None, _ ->
+             Some
+               ( CP.Result.error
+                   (!^"Could not locate definition of predicate" ^^^ Sym.pp s),
+                 rt,
+                 it ))
+      in
+      let checked = List.filter_map check (C.get_rs ctxt) in
+      let nos, _ = List.partition (fun (r, _, _) -> CP.Result.is_no r) checked in
+      (* let yeses, unknown = List.partition (fun (r, _, _) -> is_yes r) rest in *)
+      (* Issue #900 *)
+      let pp_checked_res (p, req, cand) =
+        let _ = p in
+        let rslt = Req.pp req ^^^ !^"(" ^^^ IT.pp cand ^^^ !^")" in
+        Rp.
+          { original = rslt;
+            (* !^"Full predicate check output: "
             ^^^ CP.Result.pp (Pp.list LC.pp) (fun x -> x) p; *)
-          (* Issue #900 *)
-          simplified = [ rslt ]
-        }
-    in
-    Rp.add_labeled Rp.lab_invalid (List.map pp_checked_res nos) Rp.labeled_empty
+            (* Issue #900 *)
+            simplified = [ rslt ]
+          }
+      in
+      Rp.add_labeled Rp.lab_invalid (List.map pp_checked_res nos) Rp.labeled_empty)
     (* Currently only displays invalid predicates : Issue #900 *)
     (* (Rp.add_labeled
        Rp.lab_unknown
diff --git a/lib/resourceInference.ml b/lib/resourceInference.ml
index ced0b4295..a92ca6729 100644
--- a/lib/resourceInference.ml
+++ b/lib/resourceInference.ml
@@ -79,7 +79,15 @@ module General = struct
          | `False ->
            let@ model = model () in
            let msg ctxt =
-             TypeErrors.Merging_multiple_arrays { requests; situation; ctxt; model }
+             let orequest =
+               Option.map
+                 (fun r -> r.TypeErrors.RequestChain.resource)
+                 (List.nth_opt (List.rev requests) 0)
+             in
+             let report =
+               Explain.trace ctxt model Explain.{ no_ex with request = orequest }
+             in
+             TypeErrors.Merging_multiple_arrays { requests; situation; report }
            in
            fail (fun ctxt -> { loc; msg = msg ctxt })
          | `True -> return default)
@@ -120,10 +128,17 @@ module General = struct
           | `False ->
             let@ model = model () in
             fail (fun ctxt ->
-              (* let ctxt = { ctxt with resources = original_resources } in *)
+              let orequest =
+                Option.map
+                  TypeErrors.RequestChain.(fun (r : elem) -> r.resource)
+                  (List.nth_opt (List.rev request_chain) 0)
+              in
+              let report =
+                Explain.trace ctxt model Explain.{ no_ex with request = orequest }
+              in
               let msg =
                 TypeErrors.Missing_resource
-                  { requests = request_chain; situation; model; ctxt }
+                  { requests = request_chain; situation; report }
               in
               { loc; msg })
           | `True -> assert false)
@@ -142,16 +157,16 @@ module General = struct
        | `True -> return (ftyp, [])
        | `False ->
          let@ model = model () in
-         let@ all_cs = get_cs () in
-         let () = assert (not (LC.Set.mem c all_cs)) in
          debug_constraint_failure_diagnostics 6 model simp_ctxt c;
          let@ () = Diagnostics.investigate model c in
          fail (fun ctxt ->
-           (* let ctxt = { ctxt with resources = original_resources } in *)
+           let report =
+             Explain.trace ctxt model Explain.{ no_ex with unproven_constraint = Some c }
+           in
            { loc;
              msg =
                TypeErrors.Unproven_constraint
-                 { constr = c; info; requests = snd uiinfo; ctxt; model }
+                 { constr = c; info; requests = snd uiinfo; report }
            }))
     | I _rt -> return (ftyp, [])
 
@@ -477,7 +492,13 @@ module Special = struct
     | `False ->
       let@ model = model () in
       fail (fun ctxt ->
-        let msg = TypeErrors.Missing_resource { requests; situation; model; ctxt } in
+        let orequest =
+          Option.map
+            TypeErrors.RequestChain.(fun (r : elem) -> r.resource)
+            (List.nth_opt (List.rev requests) 0)
+        in
+        let report = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in
+        let msg = TypeErrors.Missing_resource { requests; situation; report } in
         { loc; msg })
     | `True -> assert false
 
@@ -555,16 +576,23 @@ module Special = struct
     match found with
     | Ans.Found -> return ()
     | No_res ->
-      fail (fun ctxt ->
+      fail (fun _ctxt ->
         let msg =
-          TypeErrors.Allocation_not_live { reason; ptr; model_constr = None; ctxt }
+          (* probably we want Report.report to work also if no model is
+             available *)
+          TypeErrors.Allocation_not_live { reason; ptr; maybe_report = None }
         in
         { loc; msg })
     | Model (model, constr) ->
       fail (fun ctxt ->
+        let report =
+          Explain.trace
+            ctxt
+            model
+            Explain.{ no_ex with unproven_constraint = Some (LC.T constr) }
+        in
         let msg =
-          TypeErrors.Allocation_not_live
-            { reason; ptr; model_constr = Some (model, constr); ctxt }
+          TypeErrors.Allocation_not_live { reason; ptr; maybe_report = Some report }
         in
         { loc; msg })
 
diff --git a/lib/simple_smt.ml b/lib/simple_smt.ml
index 66391d842..c770f9d40 100644
--- a/lib/simple_smt.ml
+++ b/lib/simple_smt.ml
@@ -544,6 +544,16 @@ let check s =
   | ans -> raise (UnexpectedSolverResponse ans)
 
 
+(** Check if the current set of assumptions, plus the argument, are consistent.
+    Throws {!UnexpectedSolverResponse}. *)
+let check_assuming s lcs =
+  match s.command (list [ atom "check-sat-assuming"; list lcs ]) with
+  | Sexp.Atom "unsat" -> Unsat
+  | Sexp.Atom "sat" -> Sat
+  | Sexp.Atom "unknown" -> Unknown
+  | ans -> raise (UnexpectedSolverResponse ans)
+
+
 (** {2 Decoding Results} *)
 
 (** Get all definitions currently in scope. Only valid after a [Sat] result.
@@ -901,7 +911,7 @@ let cvc5 : solver_config =
   { exe = "cvc5";
     (* opts = [ "--incremental"; "--sets-ext"; "--force-logic=QF_AUFBVDTLIA" ]; *)
     (* NOTE cvc5 1.2.1 renamed --sets-ext to --sets-exp *)
-    opts = [ "--incremental"; "--sets-ext"; "--force-logic=QF_ALL" ];
+    opts = [ "--incremental"; "--sets-exp"; "--force-logic=QF_ALL" ];
     setup = [];
     exts = CVC5;
     log = quiet_log
diff --git a/lib/solver.ml b/lib/solver.ml
index 75632a2f8..1f5b36ca2 100644
--- a/lib/solver.ml
+++ b/lib/solver.ml
@@ -81,7 +81,7 @@ let empty_solver_frame () =
   }
 
 
-let copy_solver_frame f = { f with commands = f.commands }
+let _copy_solver_frame f = { f with commands = f.commands }
 
 type solver =
   { smt_solver : SMT.solver; (** The SMT solver connection. *)
@@ -94,6 +94,24 @@ type solver =
     globals : Global.t
   }
 
+(* ---------------------------------------------------------------------------*)
+(* GLOBAL STATE: Models *)
+(* ---------------------------------------------------------------------------*)
+
+type model = IT.t -> IT.t option
+
+type quantifiers = (Sym.t * BaseTypes.t) list
+
+type model_with_q = model * quantifiers
+
+type model_state =
+  | No_model
+  | Model of solver * quantifiers (* the solver that produced the model *)
+
+let model_state = ref No_model
+
+let have_model () = match !model_state with No_model -> false | Model _ -> true
+
 module Debug = struct
   let dump_frame (f : solver_frame) =
     let to_string = Sexplib.Sexp.to_string_hum in
@@ -155,6 +173,7 @@ let debug_ack_command s cmd =
 
 (** Start a new scope. *)
 let push s =
+  model_state := No_model;
   debug_ack_command s (SMT.push 1);
   s.prev_frames := !(s.cur_frame) :: !(s.prev_frames);
   s.cur_frame := empty_solver_frame ()
@@ -162,6 +181,7 @@ let push s =
 
 (** Return to the previous scope.  Assumes that there is a previous scope. *)
 let pop s n =
+  model_state := No_model;
   if n = 0 then
     ()
   else (
@@ -1091,8 +1111,25 @@ let rec translate_term s iterm =
      | _ -> assert false)
 
 
+let model () =
+  match !model_state with
+  | No_model -> assert false
+  | Model (solver, qs) ->
+    let _defs = SMT.get_model solver.smt_solver in
+    let eval =
+      fun it ->
+      assert (have_model ());
+      let sexp = translate_term solver it in
+      let res = SMT.get_expr solver.smt_solver sexp in
+      let ctys = get_ctype_table solver in
+      Some (get_ivalue solver.globals ctys (get_bt it) (SMT.no_let res))
+    in
+    (eval, qs)
+
+
 (** Add an assertion.  Quantified predicates are ignored. *)
 let add_assumption solver global lc =
+  model_state := No_model;
   let s1 = { solver with globals = global } in
   match lc with
   | LC.T it -> ack_command solver (SMT.assume (translate_term s1 it))
@@ -1289,101 +1326,72 @@ let make globals =
   s
 
 
-(* ---------------------------------------------------------------------------*)
-(* GLOBAL STATE: Models *)
-(* ---------------------------------------------------------------------------*)
-
-type model = int
-
-type model_fn = IT.t -> IT.t option
-
-type model_with_q = model * (Sym.t * BaseTypes.t) list
-
-type model_table = (model, model_fn) Hashtbl.t
-
-let models_tbl : model_table = Hashtbl.create 1
-
-let empty_model =
-  let model = Option.some in
-  Hashtbl.add models_tbl 0 model;
-  0
-
-
-type model_state =
-  | Model of model_with_q
-  | No_model
-
-let model_state = ref No_model
-
-let model () = match !model_state with No_model -> assert false | Model mo -> mo
-
-(** Evaluate terms in the context of a model computed by the solver. *)
-let model_evaluator, reset_model_evaluator_state =
-  (* internal state for the model evaluator, reuses the solver across consecutive calls for efficiency *)
-  let model_evaluator_solver : Simple_smt.solver option ref = ref None in
-  let currently_loaded_model = ref 0 in
-  let model_id = ref 0 in
-  let new_model_id () =
-    (* Start with 1, as 0 is the id of the empty model *)
-    model_id := !model_id + 1;
-    !model_id
-  in
-  let reset_model_evaluator_state () =
-    currently_loaded_model := 0;
-    model_evaluator_solver := None;
-    model_id := 0
-  in
-  let model_evaluator solver mo =
-    match SMT.to_list mo with
-    | None -> failwith "model is an atom"
-    | Some defs ->
-      let scfg = solver.smt_solver.config in
-      let cfg = { scfg with log = Logger.make "model" } in
-      let smt_solver, new_solver =
-        match !model_evaluator_solver with
-        | Some smt_solver -> (smt_solver, false)
-        | None ->
-          let s = SMT.new_solver cfg in
-          model_evaluator_solver := Some s;
-          (s, true)
-      in
-      let model_id = new_model_id () in
-      let gs = solver.globals in
-      let evaluator =
-        { smt_solver;
-          cur_frame = ref (empty_solver_frame ());
-          prev_frames =
-            ref
-              (List.map copy_solver_frame (!(solver.cur_frame) :: !(solver.prev_frames)))
-            (* We keep the prev_frames because things that were declared, would now be
-               defined by the model. Also, we need the infromation about the C type
-               mapping. *);
-          name_seed = solver.name_seed;
-          globals = gs
-        }
-      in
-      if new_solver then (
-        declare_solver_basics evaluator;
-        push evaluator);
-      let model_fn e =
-        if not (!currently_loaded_model = model_id) then (
-          currently_loaded_model := model_id;
-          pop evaluator 1;
-          push evaluator;
-          List.iter (debug_ack_command evaluator) defs);
-        let inp = translate_term evaluator e in
-        match SMT.check smt_solver with
-        | SMT.Sat ->
-          let res = SMT.get_expr smt_solver inp in
-          let ctys = get_ctype_table evaluator in
-          Some (get_ivalue gs ctys (get_bt e) (SMT.no_let res))
-        | _ -> None
-      in
-      Hashtbl.add models_tbl model_id model_fn;
-      model_id
-  in
-  (model_evaluator, reset_model_evaluator_state)
-
+(* (\** Evaluate terms in the context of a model computed by the solver. *\) *)
+(* let model_evaluator, reset_model_evaluator_state = *)
+(*   (\* internal state for the model evaluator, reuses the solver across consecutive calls for efficiency *\) *)
+(*   let model_evaluator_solver : Simple_smt.solver option ref = ref None in *)
+(*   let currently_loaded_model = ref 0 in *)
+(*   let model_id = ref 0 in *)
+(*   let new_model_id () = *)
+(*     (\* Start with 1, as 0 is the id of the empty model *\) *)
+(*     model_id := !model_id + 1; *)
+(*     !model_id *)
+(*   in *)
+(*   let reset_model_evaluator_state () = *)
+(*     currently_loaded_model := 0; *)
+(*     model_evaluator_solver := None; *)
+(*     model_id := 0 *)
+(*   in *)
+(*   let model_evaluator solver mo = *)
+(*     match SMT.to_list mo with *)
+(*     | None -> failwith "model is an atom" *)
+(*     | Some defs -> *)
+(*       let scfg = solver.smt_solver.config in *)
+(*       let cfg = { scfg with log = Logger.make "model" } in *)
+(*       let smt_solver, new_solver = *)
+(*         match !model_evaluator_solver with *)
+(*         | Some smt_solver -> (smt_solver, false) *)
+(*         | None -> *)
+(*           let s = SMT.new_solver cfg in *)
+(*           model_evaluator_solver := Some s; *)
+(*           (s, true) *)
+(*       in *)
+(*       let model_id = new_model_id () in *)
+(*       let gs = solver.globals in *)
+(*       let evaluator = *)
+(*         { smt_solver; *)
+(*           cur_frame = ref (empty_solver_frame ()); *)
+(*           prev_frames = *)
+(*             ref *)
+(*               (List.map copy_solver_frame (!(solver.cur_frame) :: !(solver.prev_frames))) *)
+(*             (\* We keep the prev_frames because things that were declared, would now be *)
+(*                defined by the model. Also, we need the infromation about the C type *)
+(*                mapping. *\); *)
+(*           name_seed = solver.name_seed; *)
+(*           globals = gs *)
+(*         } *)
+(*       in *)
+(*       if new_solver then ( *)
+(*         declare_solver_basics evaluator; *)
+(*         push evaluator); *)
+(*       let model_fn e = *)
+(*         if not (!currently_loaded_model = model_id) then ( *)
+(*           currently_loaded_model := model_id; *)
+(*           pop evaluator 1; *)
+(*           push evaluator; *)
+(*           List.iter (debug_ack_command evaluator) defs); *)
+(*         let inp = translate_term evaluator e in *)
+(*         match SMT.check smt_solver with *)
+(*         | SMT.Sat -> *)
+(*           let res = SMT.get_expr smt_solver inp in *)
+(*           let ctys = get_ctype_table evaluator in *)
+(*           Some (get_ivalue gs ctys (get_bt e) (SMT.no_let res)) *)
+(*         | _ -> None *)
+(*       in *)
+(*       Hashtbl.add models_tbl model_id model_fn; *)
+(*       model_id *)
+(*   in *)
+(*   (model_evaluator, reset_model_evaluator_state) *)
 
 (* ---------------------------------------------------------------------------*)
 
@@ -1443,11 +1451,7 @@ let try_hard = ref false
 
 let provableWithUnknown ~loc ~solver ~assumptions ~simp_ctxt lc =
   let _ = loc in
-  let set_model smt_solver qs =
-    let defs = SMT.get_model smt_solver in
-    let model = model_evaluator solver defs in
-    model_state := Model (model, qs)
-  in
+  let set_model (s : solver) qs = model_state := Model (s, qs) in
   match shortcut simp_ctxt lc with
   | `True ->
     model_state := No_model;
@@ -1455,47 +1459,36 @@ let provableWithUnknown ~loc ~solver ~assumptions ~simp_ctxt lc =
   | `No_shortcut lc ->
     let { expr; qs; extra } = translate_goal solver assumptions lc in
     let nexpr = SMT.bool_not expr in
-    let inc = solver.smt_solver in
-    debug_ack_command solver (SMT.push 1);
-    debug_ack_command solver (SMT.assume (SMT.bool_ands (nexpr :: extra)));
-    (match SMT.check inc with
+    (match SMT.check_assuming solver.smt_solver (nexpr :: extra) with
      | SMT.Unsat ->
-       debug_ack_command solver (SMT.pop 1);
        model_state := No_model;
        `True
-     | SMT.Sat when !try_hard ->
-       debug_ack_command solver (SMT.pop 1);
-       let assumptions = LC.Set.elements assumptions in
-       let foralls = TryHard.translate_foralls solver assumptions in
-       let functions = TryHard.translate_functions solver in
-       debug_ack_command solver (SMT.push 1);
-       debug_ack_command
-         solver
-         (SMT.assume (SMT.bool_ands ((nexpr :: foralls) @ functions)));
-       Pp.(debug 3 (lazy !^"***** try-hard *****"));
-       (match SMT.check inc with
-        | SMT.Unsat ->
-          debug_ack_command solver (SMT.pop 1);
-          model_state := No_model;
-          Pp.(debug 3 (lazy !^"***** try-hard: provable *****"));
-          `True
-        | SMT.Sat ->
-          set_model inc qs;
-          debug_ack_command solver (SMT.pop 1);
-          Pp.(debug 3 (lazy !^"***** try-hard: unprovable *****"));
-          `Unknown (*TODO CHT*)
-        | SMT.Unknown ->
-          set_model inc qs;
-          debug_ack_command solver (SMT.pop 1);
-          Pp.(debug 3 (lazy !^"***** try-hard: unknown *****"));
-          `False)
      | SMT.Sat ->
-       set_model inc qs;
-       debug_ack_command solver (SMT.pop 1);
-       `False
-     | SMT.Unknown ->
-       debug_ack_command solver (SMT.pop 1);
-       failwith "Unknown")
+       (match !try_hard with
+        | true ->
+          let assumptions = LC.Set.elements assumptions in
+          let foralls = TryHard.translate_foralls solver assumptions in
+          let functions = TryHard.translate_functions solver in
+          Pp.(debug 3 (lazy !^"***** try-hard *****"));
+          (match
+             SMT.check_assuming solver.smt_solver ((nexpr :: foralls) @ functions)
+           with
+           | SMT.Unsat ->
+             model_state := No_model;
+             Pp.(debug 3 (lazy !^"***** try-hard: provable *****"));
+             `True
+           | SMT.Sat ->
+             set_model solver qs;
+             Pp.(debug 3 (lazy !^"***** try-hard: unprovable *****"));
+             `False
+           | SMT.Unknown ->
+             set_model solver qs;
+             Pp.(debug 3 (lazy !^"***** try-hard: unknown *****"));
+             `Unknown)
+        | false ->
+          set_model solver qs;
+          `False)
+     | SMT.Unknown -> failwith "Unknown")
 
 
 (** The main way to query the solver. *)
@@ -1511,7 +1504,5 @@ let provable ~loc ~solver ~assumptions ~simp_ctxt ?(purpose = "") lc =
   result
 
 
-(* ISD: Could these globs be different from the saved ones? *)
-let eval mo t =
-  let model_fn = Hashtbl.find models_tbl mo in
-  model_fn t
+(* TODO: remove this *)
+let eval model t = model t
diff --git a/lib/solver.mli b/lib/solver.mli
index 6f284ce67..05c7372ce 100644
--- a/lib/solver.mli
+++ b/lib/solver.mli
@@ -6,8 +6,6 @@ type model
 (** Model with quantifier instantiations *)
 type model_with_q = model * (Sym.t * BaseTypes.t) list
 
-val empty_model : model
-
 module Logger : sig
   val to_file : bool ref
 
@@ -35,9 +33,6 @@ val pop : solver -> int -> unit
     but may be unnecessary https://github.com/rems-project/cerberus/issues/752 *)
 val num_scopes : solver -> int
 
-(* Resets internal state for the model evaluator *)
-val reset_model_evaluator_state : unit -> unit
-
 (* Run the solver. Note that we pass the assumptions explicitly even though they are also
    available in the solver context, because CN is going some simplification on its own. *)
 val provableWithUnknown
diff --git a/lib/typeErrors.ml b/lib/typeErrors.ml
index f939401c3..a469826d3 100644
--- a/lib/typeErrors.ml
+++ b/lib/typeErrors.ml
@@ -94,19 +94,22 @@ type message =
   | Missing_resource of
       { requests : RequestChain.t;
         situation : situation;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Merging_multiple_arrays of
       { requests : RequestChain.t;
         situation : situation;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Unused_resource of
       { resource : Res.t;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Illtyped_binary_it of
       { left : IT.Surface.t;
@@ -119,60 +122,68 @@ type message =
       { ct : Sctypes.t;
         location : IT.t;
         value : IT.t;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Int_unrepresentable of
       { value : IT.t;
         ict : Sctypes.t;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Unproven_constraint of
       { constr : LC.t;
         requests : RequestChain.t;
         info : Locations.info;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Undefined_behaviour of
       { ub : CF.Undefined.undefined_behaviour;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Needs_alloc_id of
       { ptr : IT.t;
         ub : CF.Undefined.undefined_behaviour;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Alloc_out_of_bounds of
       { term : IT.t;
         constr : IT.t;
         ub : CF.Undefined.undefined_behaviour;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Allocation_not_live of
       { reason :
           [ `Copy_alloc_id | `Ptr_cmp | `Ptr_diff | `ISO_array_shift | `ISO_member_shift ];
         ptr : IT.t;
-        ctxt : Context.t * Explain.log;
-        model_constr : (Solver.model_with_q * IT.t) option
+        (* ctxt : Context.t * Explain.log; *)
+        maybe_report : Report.report option
       }
   (* | Implementation_defined_behaviour of document * state_report *)
   | Unspecified of CF.Ctype.ctype
   | StaticError of
       { err : string;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Generic of Pp.document [@deprecated "Please add a specific constructor"]
   (** TODO delete this *)
   | Generic_with_model of
       { err : document;
-        model : Solver.model_with_q;
-        ctxt : Context.t * Explain.log
+        (* model : Solver.model_with_q; *)
+        (* ctxt : Context.t * Explain.log *)
+        report : Report.report
       } [@deprecated "Please add a specific constructor"]
   | Unsupported of document
   | Empty_provenance
@@ -445,17 +456,17 @@ let pp_message = function
   | Compile msg -> pp_compile msg
   | Builtins msg -> pp_builtins msg
   | Parse msg -> pp_parse msg
-  | Missing_resource { requests; situation; ctxt; model } ->
+  | Missing_resource { requests; situation; report } ->
     let short = !^"Missing resource" ^^^ for_situation situation in
     let descr = RequestChain.pp requests in
-    let orequest =
-      Option.map
-        (fun (r : RequestChain.elem) -> r.RequestChain.resource)
-        (List.nth_opt (List.rev requests) 0)
-    in
-    let state = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in
-    { short; descr; state = Some state }
-  | Merging_multiple_arrays { requests; situation; ctxt; model } ->
+    (* let orequest = *)
+    (*   Option.map *)
+    (*     (fun (r : RequestChain.elem) -> r.RequestChain.resource) *)
+    (*     (List.nth_opt (List.rev requests) 0) *)
+    (* in *)
+    (* let state = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in *)
+    { short; descr; state = Some report }
+  | Merging_multiple_arrays { requests; situation; report } ->
     let short =
       !^"Cannot satisfy request for resource"
       ^^^ for_situation situation
@@ -463,16 +474,12 @@ let pp_message = function
       ^^^ !^"It requires merging multiple arrays."
     in
     let descr = RequestChain.pp requests in
-    let orequest =
-      Option.map (fun r -> r.RequestChain.resource) (List.nth_opt (List.rev requests) 0)
-    in
-    let state = Explain.trace ctxt model Explain.{ no_ex with request = orequest } in
-    { short; descr; state = Some state }
-  | Unused_resource { resource; ctxt; model } ->
+    { short; descr; state = Some report }
+  | Unused_resource { resource; report } ->
     let resource = Res.pp resource in
     let short = !^"Left-over unused resource" ^^^ squotes resource in
-    let state = Explain.trace ctxt model Explain.no_ex in
-    { short; descr = None; state = Some state }
+    (* let state = Explain.trace ctxt model Explain.no_ex in *)
+    { short; descr = None; state = Some report }
   | TooBigExponent { it } ->
     let it = IT.pp it in
     let short = !^"Exponent too big" in
@@ -499,26 +506,25 @@ let pp_message = function
       ^^^ !^"Exponent must be non-negative"
     in
     { short; descr = Some descr; state = None }
-  | Write_value_unrepresentable { ct; location; value; ctxt; model } ->
+  | Write_value_unrepresentable { ct; location; value; report } ->
     let short = !^"Write value not representable at type" ^^^ Sctypes.pp ct in
     let location = IT.pp location in
     let value = IT.pp value in
-    let state = Explain.trace ctxt model Explain.no_ex in
+    (* let state = Explain.trace ctxt model Explain.no_ex in *)
     let descr =
       !^"Location" ^^ colon ^^^ location ^^ comma ^^^ !^"value" ^^ colon ^^^ value ^^ dot
     in
-    { short; descr = Some descr; state = Some state }
-  | Int_unrepresentable { value; ict; ctxt; model } ->
+    { short; descr = Some descr; state = Some report }
+  | Int_unrepresentable { value; ict; report } ->
     let short = !^"integer value not representable at type" ^^^ Sctypes.pp ict in
     let value = IT.pp value in
     let descr = !^"Value" ^^ colon ^^^ value in
-    let state = Explain.trace ctxt model Explain.no_ex in
-    { short; descr = Some descr; state = Some state }
-  | Unproven_constraint { constr; requests; info; ctxt; model } ->
+    { short; descr = Some descr; state = Some report }
+  | Unproven_constraint { constr = _; requests; info; report } ->
     let short = !^"Unprovable constraint" in
-    let state =
-      Explain.trace ctxt model Explain.{ no_ex with unproven_constraint = Some constr }
-    in
+    (* let state = *)
+    (*   Explain.trace ctxt model Explain.{ no_ex with unproven_constraint = Some constr } *)
+    (* in *)
     let descr =
       let spec_loc, odescr = info in
       let head, pos = Locations.head_pos_of_location spec_loc in
@@ -531,40 +537,40 @@ let pp_message = function
       | Some doc2 -> doc ^^ hardline ^^ doc2
       | None -> doc
     in
-    { short; descr = Some descr; state = Some state }
-  | Undefined_behaviour { ub; ctxt; model } ->
+    { short; descr = Some descr; state = Some report }
+  | Undefined_behaviour { ub; report } ->
     let short = !^"Undefined behaviour" in
-    let state = Explain.trace ctxt model Explain.no_ex in
+    (* let state = Explain.trace ctxt model Explain.no_ex in *)
     let descr =
       match CF.Undefined.std_of_undefined_behaviour ub with
       | Some stdref -> !^(CF.Undefined.ub_short_string ub) ^^^ parens !^stdref
       | None -> !^(CF.Undefined.ub_short_string ub)
     in
-    { short; descr = Some descr; state = Some state }
-  | Needs_alloc_id { ptr; ub; ctxt; model } ->
+    { short; descr = Some descr; state = Some report }
+  | Needs_alloc_id { ptr; ub; report } ->
     let short = !^"Pointer " ^^ bquotes (IT.pp ptr) ^^ !^" needs allocation ID" in
-    let state = Explain.trace ctxt model Explain.no_ex in
+    (* let state = Explain.trace ctxt model Explain.no_ex in *)
     let descr =
       match CF.Undefined.std_of_undefined_behaviour ub with
       | Some stdref -> !^(CF.Undefined.ub_short_string ub) ^^^ parens !^stdref
       | None -> !^(CF.Undefined.ub_short_string ub)
     in
-    { short; descr = Some descr; state = Some state }
-  | Alloc_out_of_bounds { constr; term; ub; ctxt; model } ->
+    { short; descr = Some descr; state = Some report }
+  | Alloc_out_of_bounds { constr = _; term; ub; report } ->
     let short = bquotes (IT.pp term) ^^ !^" out of bounds" in
-    let state =
-      Explain.trace
-        ctxt
-        model
-        Explain.{ no_ex with unproven_constraint = Some (LC.T constr) }
-    in
+    (* let state = *)
+    (*   Explain.trace *)
+    (*     ctxt *)
+    (*     model *)
+    (*     Explain.{ no_ex with unproven_constraint = Some (LC.T constr) } *)
+    (* in *)
     let descr =
       match CF.Undefined.std_of_undefined_behaviour ub with
       | Some stdref -> !^(CF.Undefined.ub_short_string ub) ^^^ parens !^stdref
       | None -> !^(CF.Undefined.ub_short_string ub)
     in
-    { short; descr = Some descr; state = Some state }
-  | Allocation_not_live { reason; ptr; ctxt; model_constr } ->
+    { short; descr = Some descr; state = Some report }
+  | Allocation_not_live { reason; ptr; maybe_report } ->
     let adjust = function
       | IT.IT (CopyAllocId { loc; _ }, _, _) -> loc
       | IT.IT (ArrayShift { base; _ }, _, _) -> base
@@ -582,17 +588,17 @@ let pp_message = function
     let short =
       !^"Pointer " ^^ bquotes (IT.pp ptr) ^^^ !^"needs to be live for" ^^^ !^reason
     in
-    let state =
-      Option.map
-        (fun (model, constr) ->
-           Explain.trace
-             ctxt
-             model
-             Explain.{ no_ex with unproven_constraint = Some (LC.T constr) })
-        model_constr
-    in
+    (* let state = *)
+    (*   Option.map *)
+    (*     (fun (model, constr) -> *)
+    (*        Explain.trace *)
+    (*          ctxt *)
+    (*          model *)
+    (*          Explain.{ no_ex with unproven_constraint = Some (LC.T constr) }) *)
+    (*     model_constr *)
+    (* in *)
     let descr = !^"Need an Alloc or RW in context with same allocation id" in
-    { short; descr = Some descr; state }
+    { short; descr = Some descr; state = maybe_report }
   (* | Implementation_defined_behaviour (impl, state) -> *)
   (*    let short = !^"Implementation defined behaviour" in *)
   (*    let descr = impl in *)
@@ -600,18 +606,18 @@ let pp_message = function
   | Unspecified ctype ->
     let short = !^"Unspecified value of C-type" ^^^ CF.Pp_core_ctype.pp_ctype ctype in
     { short; descr = None; state = None }
-  | StaticError { err; ctxt; model } ->
+  | StaticError { err; report } ->
     let short = !^"Static error" in
-    let state = Explain.trace ctxt model Explain.no_ex in
+    (* let state = Explain.trace ctxt model Explain.no_ex in *)
     let descr = !^err in
-    { short; descr = Some descr; state = Some state }
+    { short; descr = Some descr; state = Some report }
   | ((Generic err) [@alert "-deprecated"]) ->
     let short = err in
     { short; descr = None; state = None }
-  | ((Generic_with_model { err; model; ctxt }) [@alert "-deprecated"]) ->
+  | ((Generic_with_model { err; report }) [@alert "-deprecated"]) ->
     let short = err in
-    let state = Explain.trace ctxt model Explain.no_ex in
-    { short; descr = None; state = Some state }
+    (* let state = Explain.trace ctxt model Explain.no_ex in *)
+    { short; descr = None; state = Some report }
   | Unsupported err ->
     let short = err in
     { short; descr = None; state = None }
@@ -619,10 +625,9 @@ let pp_message = function
     let short = !^"Empty provenance" in
     { short; descr = None; state = None }
   | Illtyped_binary_it { left; right; binop } -> pp_illtyped_binary_it ~left ~right binop
-  | Inconsistent_assumptions (kind, ctxt_log) ->
+  | Inconsistent_assumptions (kind, _ctxt_log) ->
     let short = !^kind ^^ !^" makes inconsistent assumptions" in
-    let state = Some (Explain.trace ctxt_log (Solver.empty_model, []) Explain.no_ex) in
-    { short; descr = None; state }
+    { short; descr = None; state = None }
   | Byte_conv_needs_owned ->
     let short = !^"byte conversion only supports W/RW" in
     { short; descr = None; state = None }
diff --git a/lib/typeErrors.mli b/lib/typeErrors.mli
index 527659d98..1247a7c6c 100644
--- a/lib/typeErrors.mli
+++ b/lib/typeErrors.mli
@@ -37,19 +37,22 @@ type message =
   | Missing_resource of
       { requests : RequestChain.t;
         situation : Error_common.situation;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Merging_multiple_arrays of
       { requests : RequestChain.t;
         situation : Error_common.situation;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Unused_resource of
       { resource : Resource.t;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Illtyped_binary_it of
       { left : IndexTerms.Surface.t;
@@ -62,59 +65,68 @@ type message =
       { ct : Sctypes.t;
         location : IndexTerms.t;
         value : IndexTerms.t;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Int_unrepresentable of
       { value : IndexTerms.t;
         ict : Sctypes.t;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Unproven_constraint of
       { constr : LogicalConstraints.t;
         requests : RequestChain.t;
         info : Locations.info;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Undefined_behaviour of
       { ub : Cerb_frontend.Undefined.undefined_behaviour;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Needs_alloc_id of
       { ptr : IndexTerms.t;
         ub : Cerb_frontend.Undefined.undefined_behaviour;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Alloc_out_of_bounds of
       { term : IndexTerms.t;
         constr : IndexTerms.t;
         ub : Cerb_frontend.Undefined.undefined_behaviour;
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Allocation_not_live of
       { reason :
           [ `Copy_alloc_id | `ISO_array_shift | `ISO_member_shift | `Ptr_cmp | `Ptr_diff ];
         ptr : IndexTerms.t;
-        ctxt : Context.t * Explain.log;
-        model_constr : (Solver.model_with_q * IndexTerms.t) option
+        (* ctxt : Context.t * Explain.log; *)
+        (* model_constr : (Solver.model_with_q * IndexTerms.t) option *)
+        maybe_report : Report.report option
       }
   | Unspecified of Cerb_frontend.Ctype.ctype
   | StaticError of
       { err : string; (** TODO replace with an actual type *)
-        ctxt : Context.t * Explain.log;
-        model : Solver.model_with_q
+        (* ctxt : Context.t * Explain.log; *)
+        (* model : Solver.model_with_q *)
+        report : Report.report
       }
   | Generic of Pp.document [@deprecated "Please add a specific constructor"]
   (** TODO delete this *)
   | Generic_with_model of
       { err : Pp.document;
-        model : Solver.model_with_q;
-        ctxt : Context.t * Explain.log
+        (* model : Solver.model_with_q; *)
+        (* ctxt : Context.t * Explain.log *)
+        report : Report.report
       } [@deprecated "Please add a specific constructor"] (** TODO delete this too *)
   | Unsupported of Pp.document (** TODO add source location *)
   | Empty_provenance
diff --git a/tests/cn/reverse.error.c.verify b/tests/cn/reverse.error.c.verify
index 132f40521..297292326 100644
--- a/tests/cn/reverse.error.c.verify
+++ b/tests/cn/reverse.error.c.verify
@@ -13,5 +13,5 @@ tests/cn/reverse.error.c:124:3: error: Missing resource for de-allocating
   ^~~~~~~~~ 
 Resource needed: W<struct node>(&n3)
   which requires: W<signed int>(&&n3->head)
-      other location (File "lib/resourceInference.ml", line 205, characters 31-38)  (arg head)
+      other location (File "lib/resourceInference.ml", line 220, characters 31-38)  (arg head)
 State file: file:///tmp/state__reverse.error.c__main.html