From 58e6b924a846e0c953f8f6e79d9989b5714cf7ec Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 7 Dec 2016 13:21:12 +0100
Subject: [PATCH] Added full_slice function in Internal

---
 src/core/internal.mli | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/core/internal.mli b/src/core/internal.mli
index c00b5d29..30fb1836 100644
--- a/src/core/internal.mli
+++ b/src/core/internal.mli
@@ -69,6 +69,10 @@ module Make
   val model : unit -> (St.term * St.term) list
   (** Returns the model found if the formula is satisfiable. *)
 
+  val full_slice : unit -> (St.term, St.formula, St.proof) Plugin_intf.slice
+  (** View the current state of the trail as a slice. Mainly useful when the
+      solver has reached a SAT conclusion. *)
+
   val check : unit -> bool
   (** Check the satisfiability of the current model. Only has meaning
       if the solver finished proof search and has returned [Sat]. *)