From cf578d186839f2312bcbf88952e1504c22c51b51 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Tue, 13 Jan 2015 17:36:13 +0100
Subject: [PATCH] Removed useless level in plugin_intf

---
 smt/mcsat.ml          | 4 ++--
 solver/mcsolver.ml    | 2 +-
 solver/plugin_intf.ml | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/smt/mcsat.ml b/smt/mcsat.ml
index a996f852..ecafbaef 100644
--- a/smt/mcsat.ml
+++ b/smt/mcsat.ml
@@ -35,7 +35,7 @@ module Tsmt = struct
   }
 
   type res =
-    | Sat of level
+    | Sat
     | Unsat of formula list * proof
 
   type eval_res =
@@ -74,7 +74,7 @@ module Tsmt = struct
                 | Fsmt.Distinct (i, j) ->
                   env := { !env with cc = CC.add_neq !env.cc i j }
           done;
-          Sat (current_level ())
+          Sat
       with CC.Unsat x ->
         Log.debug 8 "Making explanation clause...";
         Unsat (to_clause x, ())
diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index 83d49550..d8e32d88 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -635,7 +635,7 @@ module Make (E : Expr_intf.S)
   let rec theory_propagate () =
     let head = Vec.size env.trail in
     match Th.assume (current_slice ()) with
-    | Th.Sat _ ->
+    | Th.Sat ->
       env.tatoms_qhead <- head;
       propagate ()
     | Th.Unsat (l, p) ->
diff --git a/solver/plugin_intf.ml b/solver/plugin_intf.ml
index fe819219..3a4ba650 100644
--- a/solver/plugin_intf.ml
+++ b/solver/plugin_intf.ml
@@ -47,7 +47,7 @@ module type S = sig
       Formulas in the unsat clause must come from the current set of assumptions, i.e
       must have been encountered in a slice. *)
   type res =
-    | Sat of level
+    | Sat
     | Unsat of formula list * proof
 
   type eval_res =