diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index 83d49550..32267300 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -858,6 +858,13 @@ module Make (E : Expr_intf.S)
 
   let unsat_conflict () = env.unsat_conflict
 
+  let model () =
+    let opt = function Some a -> a | None -> assert false in
+    Vec.fold (fun acc e -> Either.destruct e
+      (fun v -> (v.tag.term, opt v.tag.assigned)  :: acc)
+      (fun _ -> acc)
+    ) [] env.trail
+
   (* Push/Pop *)
   type level = int
 
diff --git a/solver/mcsolver.mli b/solver/mcsolver.mli
index 120077f8..83a9e6b9 100644
--- a/solver/mcsolver.mli
+++ b/solver/mcsolver.mli
@@ -39,6 +39,9 @@ module Make (E : Expr_intf.S)
   (** Returns the unsat clause found at the toplevel, if it exists (i.e if
       [solve] has raised [Unsat]) *)
 
+  val model : unit -> (St.term * St.term) list
+  (** Returns the model found if the formula is satisfiable. *)
+
   type level
   (** Abstract notion of assumption level. *)