diff --git a/mcsolver/expr_intf.ml b/mcsolver/expr_intf.ml
index b18dfc13..25338cd7 100644
--- a/mcsolver/expr_intf.ml
+++ b/mcsolver/expr_intf.ml
@@ -47,8 +47,5 @@ module type S = sig
   (** Returns a 'normalized' form of the formula, possibly negated (in which case return true).
       [norm] must be so that [a] and [neg a] normalises to the same formula. *)
 
-  val iter_pure : (Term.t -> unit) -> Formula.t -> bool
-  (** An iterator over the pure subterms of a formula *)
-
 end
 
diff --git a/mcsolver/mcsolver.ml b/mcsolver/mcsolver.ml
index 34db799d..9c63fb20 100644
--- a/mcsolver/mcsolver.ml
+++ b/mcsolver/mcsolver.ml
@@ -11,10 +11,10 @@
 (**************************************************************************)
 
 module Make (E : Expr_intf.S)
-    (Th : Plugin_intf.S with type formula = E.Formula.t) = struct
+    (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) = struct
 
   module St = Mcsolver_types.Make(E)(Th)
-  module Proof = Res.Make(St)
+  (* module Proof = Res.Make(St) *)
 
   open St
 
@@ -30,6 +30,11 @@ module Make (E : Expr_intf.S)
     ul_learnt : int; (* number of learnt clauses *)
   }
 
+  (* Type for trail elements *)
+  type trail_elt =
+      | Semantic of semantic var
+      | Boolean of atom
+
   (* Singleton type containing the current state *)
   type env = {
 
@@ -51,7 +56,7 @@ module Make (E : Expr_intf.S)
     mutable var_inc : float;
     (* increment for variables' activity *)
 
-    trail : atom Vec.t;
+    trail : trail_elt Vec.t;
     (* decision stack + propagated atoms *)
 
     trail_lim : int Vec.t;
@@ -111,7 +116,6 @@ module Make (E : Expr_intf.S)
     mutable max_literals : int;
     mutable tot_literals : int;
     mutable nb_init_clauses : int;
-    mutable model : var Vec.t;
     mutable tenv_queue : Th.level Vec.t;
     mutable tatoms_qhead : int;
   }
@@ -123,7 +127,7 @@ module Make (E : Expr_intf.S)
     learnts = Vec.make 0 dummy_clause; (*updated during parsing*)
     clause_inc = 1.;
     var_inc = 1.;
-    trail = Vec.make 601 dummy_atom;
+    trail = Vec.make 601 (Boolean dummy_atom);
     trail_lim = Vec.make 601 (-1);
     user_levels = Vec.make 20 {ul_trail=0;ul_learnt=0;ul_clauses=0};
     qhead = 0;
@@ -149,7 +153,6 @@ module Make (E : Expr_intf.S)
     max_literals = 0;
     tot_literals = 0;
     nb_init_clauses = 0;
-    model = Vec.make 0 dummy_var;
     tenv_queue = Vec.make 100 Th.dummy;
     tatoms_qhead = 0;
   }
@@ -158,16 +161,32 @@ module Make (E : Expr_intf.S)
   let to_float i = float_of_int i
   let to_int f = int_of_float f
 
+  let get_elt_weight = function
+      | Term v -> v.weight
+      | Formula v -> v.weight
+
+  let set_elt_weight e w = match e with
+      | Term v -> v.weight <- w
+      | Formula v -> v.weight <- w
+
+  let get_elt_level = function
+      | Term v -> v.level
+      | Formula v -> v.level
+
   let f_weight i j =
-    (St.get_var j).weight < (St.get_var i).weight
+    get_elt_weight (St.get_var j) < get_elt_weight (St.get_var i)
 
   let f_filter i =
-    (St.get_var i).level < 0
-
+    get_elt_level (St.get_var i) < 0
 
   (* Var/clause activity *)
-  let insert_var_order v =
-    Iheap.insert f_weight env.order v.vid
+  let rec insert_var_order = function
+      | Term v ->
+              Iheap.insert f_weight env.order v.vid
+      | Formula v ->
+              Iheap.insert f_weight env.order v.vid;
+              Th.iter_assignable
+                (fun t -> insert_var_order (Term (St.add_term t))) v.tag.pa.lit
 
   let var_decay_activity () =
     env.var_inc <- env.var_inc *. env.var_decay
@@ -179,7 +198,7 @@ module Make (E : Expr_intf.S)
     v.weight <- v.weight +. env.var_inc;
     if v.weight > 1e100 then begin
       for i = 0 to (St.nb_vars ()) - 1 do
-        (St.get_var i).weight <- (St.get_var i).weight *. 1e-100
+        set_elt_weight (St.get_var i) ((get_elt_weight (St.get_var i)) *. 1e-100)
       done;
       env.var_inc <- env.var_inc *. 1e-100;
     end;
@@ -244,13 +263,15 @@ module Make (E : Expr_intf.S)
       env.qhead <- Vec.get env.trail_lim lvl;
       env.tatoms_qhead <- env.qhead;
       for c = Vec.size env.trail - 1 downto env.qhead do
-        let a = Vec.get env.trail c in
-        a.is_true <- false;
-        a.neg.is_true <- false;
-        a.var.level <- -1;
-        a.var.reason <- None;
-        a.var.vpremise <- History [];
-        insert_var_order a.var
+        match Vec.get env.trail c with
+        | Boolean a ->
+          a.is_true <- false;
+          a.neg.is_true <- false;
+          a.var.level <- -1;
+          a.var.tag.reason <- Bcp None;
+          a.var.tag.vpremise <- History [];
+          insert_var_order (Formula a.var)
+        | Semantic a -> ()
       done;
       Th.backtrack (Vec.get env.tenv_queue lvl); (* recover the right tenv *)
       Vec.shrink env.trail ((Vec.size env.trail) - env.qhead);
@@ -265,17 +286,22 @@ module Make (E : Expr_intf.S)
     env.is_unsat <- true;
     raise Unsat
 
-  let enqueue a lvl reason =
-    assert (not a.is_true && not a.neg.is_true &&
-            a.var.level < 0 && a.var.reason = None && lvl >= 0);
+  let enqueue_bool a lvl reason =
+    assert (not a.is_true && not a.neg.is_true && a.var.level < 0
+            && a.var.tag.reason = Bcp None && lvl >= 0);
     assert (lvl = decision_level ());
     (* keep the reason for proof/unsat-core *)
     (*let reason = if lvl = 0 then None else reason in*)
     a.is_true <- true;
     a.var.level <- lvl;
-    a.var.reason <- reason;
+    a.var.tag.reason <- reason;
     Log.debug 8 "Enqueue: %a" pp_atom a;
-    Vec.push env.trail a
+    Vec.push env.trail (Boolean a)
+
+  let enqueue_assign v value lvl =
+    v.tag.assigned <- Some value;
+    v.level <- lvl;
+    Vec.push env.trail (Semantic v)
 
   (* conflict analysis *)
   let analyze c_clause =
@@ -296,9 +322,9 @@ module Make (E : Expr_intf.S)
         let q = Vec.get !c.atoms j in
         (*printf "I visit %a@." D1.atom q;*)
         assert (q.is_true || q.neg.is_true && q.var.level >= 0); (* Pas sur *)
-        if not q.var.seen && q.var.level > 0 then begin
+        if not q.var.tag.seen && q.var.level > 0 then begin
           var_bump_activity q.var;
-          q.var.seen <- true;
+          q.var.tag.seen <- true;
           seen := q :: !seen;
           if q.var.level >= decision_level () then begin
             incr pathC
@@ -330,12 +356,12 @@ module Make (E : Expr_intf.S)
       | [] -> assert false
       | [fuip] ->
         assert (blevel = 0);
-        fuip.var.vpremise <- history;
+        fuip.var.tag.vpremise <- history;
         let name = fresh_lname () in
         let uclause = make_clause name learnt size true history in
         Log.debug 2 "Unit clause learnt : %a" St.pp_clause uclause;
         Vec.push env.learnts uclause;
-        enqueue fuip 0 (Some uclause)
+        enqueue_bool fuip 0 (Bcp (Some uclause))
       | fuip :: _ ->
         let name = fresh_lname () in
         let lclause = make_clause name learnt size true history in
@@ -343,7 +369,7 @@ module Make (E : Expr_intf.S)
         Vec.push env.learnts lclause;
         attach_clause lclause;
         clause_bump_activity lclause;
-        enqueue fuip blevel (Some lclause)
+        enqueue_bool fuip blevel (Bcp (Some lclause))
     end;
     var_decay_activity ();
     clause_decay_activity ()
@@ -364,7 +390,7 @@ module Make (E : Expr_intf.S)
       let aux (atoms, init) a =
           if a.is_true then raise Trivial;
           if a.neg.is_true then
-              match a.var.vpremise with
+              match a.var.tag.vpremise with
               | History v -> atoms, [init0]
               | Lemma p -> assert false
           else
@@ -381,7 +407,7 @@ module Make (E : Expr_intf.S)
           if a.var.level = 0 then raise Trivial
           else (a::trues) @ unassigned @ falses @ r, init
         else if a.neg.is_true then
-          if a.var.level = 0 then match a.var.vpremise with
+          if a.var.level = 0 then match a.var.tag.vpremise with
           | History v ->
             partition_aux trues unassigned falses [init0] r
           | Lemma _ -> assert false
@@ -422,25 +448,15 @@ module Make (E : Expr_intf.S)
         end else if b.neg.is_true && not a.is_true && not a.neg.is_true then begin
           let lvl = List.fold_left (fun m a -> max m a.var.level) 0 atoms in
           cancel_until lvl;
-          enqueue a lvl (Some clause)
+          enqueue_bool a lvl (Bcp (Some clause))
         end
       | [a]   ->
         cancel_until 0;
-        a.var.vpremise <- history;
-        enqueue a 0 (match init with [init0] -> Some init0 | _ -> None)
+        a.var.tag.vpremise <- history;
+        enqueue_bool a 0 (Bcp (match init with [init0] -> Some init0 | _ -> None))
     with Trivial -> ()
 
 
-  (* Decide on a new litteral *)
-  let rec pick_branch_lit () =
-    let max = Iheap.remove_min f_weight env.order in
-    let v = St.get_var max in
-    if v.level>= 0 then  begin
-      assert (v.pa.is_true || v.na.is_true);
-      pick_branch_lit ()
-    end else
-      v
-
   let progress_estimate () =
     let prg = ref 0. in
     let nbv = to_float (nb_vars()) in
@@ -495,7 +511,7 @@ module Make (E : Expr_intf.S)
           Vec.set watched !new_sz c;
           incr new_sz;
           Log.debug 5 "Unit clause : %a" St.pp_clause c;
-          enqueue first (decision_level ()) (Some c)
+          enqueue_bool first (decision_level ()) (Bcp (Some c))
         end
       with Exit -> ()
 
@@ -520,12 +536,16 @@ module Make (E : Expr_intf.S)
 
   (* Propagation (boolean and theory *)
   let _th_cnumber = ref 0
-  let slice_get i = (Vec.get env.trail i).lit
+  let slice_get i = match (Vec.get env.trail i) with
+    | Boolean a -> Th.Lit a.lit
+    | Semantic {tag={term; assigned = Some v}} -> Th.Assign (term, v)
+    | _ -> assert false
+
   let slice_push l lemma =
     decr _th_cnumber;
     let atoms = List.rev_map (fun x -> add_atom x) l in
     Iheap.grow_to_by_double env.order (St.nb_vars ());
-    List.iter (fun a -> insert_var_order a.var) atoms;
+    List.iter (fun a -> insert_var_order (Formula a.var)) atoms;
     add_clause ~cnumber:!_th_cnumber atoms (Lemma lemma)
 
   let current_slice () = Th.({
@@ -553,10 +573,12 @@ module Make (E : Expr_intf.S)
       let num_props = ref 0 in
       let res = ref None in
       while env.qhead < Vec.size env.trail do
-        let a = Vec.get env.trail env.qhead in
-        env.qhead <- env.qhead + 1;
-        incr num_props;
-        propagate_atom a res;
+        match Vec.get env.trail env.qhead with
+        | Boolean a ->
+          env.qhead <- env.qhead + 1;
+          incr num_props;
+          propagate_atom a res
+        | Semantic a -> ()
       done;
       env.propagations <- env.propagations + !num_props;
       env.simpDB_props <- env.simpDB_props - !num_props;
@@ -637,6 +659,34 @@ module Make (E : Expr_intf.S)
       env.simpDB_props <- env.clauses_literals + env.learnts_literals;
     end
 
+  (* Decide on a new litteral *)
+  let rec pick_branch_lit () =
+    let max = Iheap.remove_min f_weight env.order in
+    match St.get_var max with
+    | Term v ->
+        let value = Th.assign v.tag.term in
+        env.decisions <- env.decisions + 1;
+        new_decision_level();
+        let current_level = decision_level () in
+        assert (v.level < 0);
+(*         Log.debug 5 "Assigning %a to %a" St.pp_atom v.tag.pa; *)
+        enqueue_assign v value current_level
+    | Formula v ->
+      if v.level>= 0 then begin
+          assert (v.tag.pa.is_true || v.tag.na.is_true);
+          pick_branch_lit ()
+      end else match Th.eval v.tag.pa.lit with
+        | Th.Unknown ->
+          env.decisions <- env.decisions + 1;
+          new_decision_level();
+          let current_level = decision_level () in
+          assert (v.level < 0);
+          Log.debug 5 "Deciding on %a" St.pp_atom v.tag.pa;
+          enqueue_bool v.tag.pa current_level (Bcp None)
+        | Th.Bool b ->
+          let a = if b then v.tag.pa else v.tag.na in
+          enqueue_bool a (decision_level ()) (Bcp None)
+
   let search n_of_conflicts n_of_learnts =
     let conflictC = ref 0 in
     env.starts <- env.starts + 1;
@@ -660,14 +710,7 @@ module Make (E : Expr_intf.S)
            Vec.size env.learnts - nb_assigns() >= n_of_learnts then
           reduce_db();
 
-        env.decisions <- env.decisions + 1;
-
-        new_decision_level();
-        let next = pick_branch_lit () in
-        let current_level = decision_level () in
-        assert (next.level < 0);
-        Log.debug 5 "Deciding on %a" St.pp_atom next.pa;
-        enqueue next.pa current_level None
+        pick_branch_lit ()
     done
 
   let check_clause c =
@@ -682,11 +725,6 @@ module Make (E : Expr_intf.S)
   let check_vec vec =
     for i = 0 to Vec.size vec - 1 do check_clause (Vec.get vec i) done
 
-  (*
-  let check_model () =
-    check_vec env.clauses;
-    check_vec env.learnts
-  *)
 
   (* fixpoint of propagation and decisions until a model is found, or a
      conflict is reached *)
@@ -720,7 +758,6 @@ module Make (E : Expr_intf.S)
     Iheap.grow_to_by_double env.order nbv;
     (* List.iter (List.iter (fun a -> insert_var_order a.var)) cnf; *)
     St.iter_vars insert_var_order;
-    Vec.grow_to_by_double env.model nbv;
     Vec.grow_to_by_double env.clauses nbc;
     Vec.grow_to_by_double env.learnts nbc;
     env.nb_init_clauses <- nbc;
@@ -732,9 +769,9 @@ module Make (E : Expr_intf.S)
     init_solver cnf ~cnumber
 
   let eval lit =
-    let var, negated = make_var lit in
-    assert (var.pa.is_true || var.na.is_true);
-    let truth = var.pa.is_true in
+    let var, negated = make_boolean_var lit in
+    assert (var.tag.pa.is_true || var.tag.na.is_true);
+    let truth = var.tag.pa.is_true in
     if negated then not truth else truth
 
   let history () = env.learnts
diff --git a/mcsolver/mcsolver.mli b/mcsolver/mcsolver.mli
index 4d841daf..e13584d7 100644
--- a/mcsolver/mcsolver.mli
+++ b/mcsolver/mcsolver.mli
@@ -12,19 +12,20 @@
 (**************************************************************************)
 
 module Make (E : Expr_intf.S)
-    (Th : Theory_intf.S with type formula = E.Formula.t) : sig
-  (** Functor to create a SMT Solver parametrised by the atomic
-      formulas and a theory. *)
+    (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) : sig
+  (** Functor to create a  McSolver parametrised by the atomic formulas and a theory. *)
 
   exception Unsat
 
   module St : Mcsolver_types.S
     with type formula = E.Formula.t
 
+  (*
   module Proof : Res.S
     with type atom = St.atom
      and type clause = St.clause
      and type lemma = Th.proof
+  *)
 
   val solve : unit -> unit
   (** Try and solves the current set of assumptions.
diff --git a/mcsolver/mcsolver_types.ml b/mcsolver/mcsolver_types.ml
index 9fede52c..46d14b02 100644
--- a/mcsolver/mcsolver_types.ml
+++ b/mcsolver/mcsolver_types.ml
@@ -15,23 +15,34 @@ open Printf
 
 module type S = Mcsolver_types_intf.S
 
-module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
+module Make (E : Expr_intf.S)(Th : Plugin_intf.S) = struct
 
+  (* Types declarations *)
+
+  type term = E.Term.t
   type formula = E.Formula.t
   type proof = Th.proof
 
-  type var =
-    {  vid : int;
-       pa : atom;
-       na : atom;
-       mutable weight : float;
-       mutable seen : bool;
-       mutable level : int;
-       mutable reason: reason;
-       mutable vpremise : premise}
+  type 'a var =
+    { vid : int;
+      tag : 'a;
+      mutable weight : float;
+      mutable level : int; }
+
+  type semantic =
+    { term : term;
+      mutable assigned : term option; }
+
+  type boolean = {
+    pa : atom;
+    na : atom;
+    mutable seen : bool;
+    mutable reason : reason;
+    mutable vpremise : premise
+  }
 
   and atom =
-    { var : var;
+    { var : boolean var;
       lit : formula;
       neg : atom;
       mutable watched : clause Vec.t;
@@ -46,23 +57,53 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
       learnt : bool;
       cpremise : premise }
 
-  and reason = clause option
+  and reason =
+      | Semantic of int
+      | Bcp of clause option
 
   and premise =
       | History of clause list
       | Lemma of proof
 
+  type elt =
+      | Term of semantic var
+      | Formula of boolean var
+
+  (* Accessors for variables *)
+  let get_elt_id = function
+      | Term v -> v.vid
+      | Formula v -> v.vid
+
+  let get_elt_weight = function
+      | Term v -> v.weight
+      | Formula v -> v.weight
+
+  let get_elt_level = function
+      | Term v -> v.level
+      | Formula v -> v.level
+
+  let set_elt_weight e w = match e with
+      | Term v -> v.weight <- w
+      | Formula v -> v.weight <- w
+
+  let set_elt_level e l = match e with
+      | Term v -> v.level <- l
+      | Formula v -> v.level <- l
+
+  (* Dummy values *)
   let dummy_lit = E.dummy
 
   let rec dummy_var =
     { vid = -101;
-      pa = dummy_atom;
-      na = dummy_atom;
       level = -1;
-      reason = None;
       weight = -1.;
-      seen = false;
-      vpremise = History [] }
+      tag = {
+        pa = dummy_atom;
+        na = dummy_atom;
+        reason = None;
+        seen = false;
+        vpremise = History []; };
+    }
   and dummy_atom =
     { var = dummy_var;
       lit = dummy_lit;
@@ -72,7 +113,6 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
       neg = dummy_atom;
       is_true = false;
       aid = -102 }
-
   let dummy_clause =
     { name = "";
       atoms = Vec.make_empty dummy_atom;
@@ -84,33 +124,36 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
   let () =
     dummy_atom.watched <- Vec.make_empty dummy_clause
 
-  module MA = Map.Make(E.Formula)
+  (* Constructors *)
+  module MF = Map.Make(E.Formula)
+  module MT = Map.Make(E.Term)
 
-  let normal_form = E.norm
-
-  let ma = ref MA.empty
-  let vars = Vec.make 107 dummy_var
+  let f_map = ref MF.empty
+  let t_map = ref MT.empty
 
+  let vars = Vec.make 107 (Formula dummy_var)
   let nb_vars () = Vec.size vars
   let get_var i = Vec.get vars i
   let iter_vars f = Vec.iter f vars
 
   let cpt_mk_var = ref 0
-  let make_var =
+
+  let make_boolean_var =
     fun lit ->
-      let lit, negated = normal_form lit in
-      try MA.find lit !ma, negated
+      let lit, negated = E.norm lit in
+      try MF.find lit !f_map, negated
       with Not_found ->
         let cpt_fois_2 = !cpt_mk_var lsl 1 in
         let rec var  =
           { vid = !cpt_mk_var;
-            pa = pa;
-            na = na;
             level = -1;
-            reason = None;
             weight = 0.;
-            seen = false;
-            vpremise = History [];
+            tag = {
+              pa = pa;
+              na = na;
+              reason = Bcp None;
+              seen = false;
+              vpremise = History [];};
           }
         and pa =
           { var = var;
@@ -126,15 +169,32 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
             neg = pa;
             is_true = false;
             aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in
-        ma := MA.add lit var !ma;
+        f_map := MF.add lit var !f_map;
         incr cpt_mk_var;
-        Vec.push vars var;
-        assert (Vec.get vars var.vid == var && !cpt_mk_var = Vec.size vars);
+        Vec.push vars (Formula var);
         var, negated
 
+  let make_semantic_var t =
+      try MT.find t !t_map
+      with Not_found ->
+        let res = {
+          vid = !cpt_mk_var;
+          weight = 0.;
+          level = -1;
+          tag = {
+            term = t;
+            assigned = None; };
+        } in
+        incr cpt_mk_var;
+        t_map := MT.add t res !t_map;
+        Vec.push vars (Term res);
+        res
+
+  let add_term t = make_semantic_var t
+
   let add_atom lit =
-    let var, negated = make_var lit in
-    if negated then var.na else var.pa
+    let var, negated = make_boolean_var lit in
+    if negated then var.tag.na else var.tag.pa
 
   let make_clause name ali sz_ali is_learnt premise =
     let atoms = Vec.from_list ali sz_ali dummy_atom in
@@ -147,6 +207,7 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
 
   let empty_clause = make_clause "Empty" [] 0 false (History [])
 
+  (* Name generation *)
   let fresh_lname =
     let cpt = ref 0 in
     fun () -> incr cpt; "L" ^ (string_of_int !cpt)
@@ -159,10 +220,6 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
     let cpt = ref 0 in
     fun () -> incr cpt; "C" ^ (string_of_int !cpt)
 
-  let clear () =
-    cpt_mk_var := 0;
-    ma := MA.empty
-
   (* Pretty printing for atoms and clauses *)
   let print_atom fmt a = E.Formula.print fmt a.lit
 
@@ -178,15 +235,16 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
     Format.fprintf fmt "%s : %a" c.name print_atoms c.atoms
 
   (* Complete debug printing *)
-  let sign a = if a==a.var.pa then "" else "-"
+  let sign a = if a==a.var.tag.pa then "" else "-"
 
   let level a =
-    match a.var.level, a.var.reason with
+    match a.var.level, a.var.tag.reason with
     | n, _ when n < 0 -> assert false
-    | 0, Some c -> sprintf "->0/%s" c.name
-    | 0, None   -> "@0"
-    | n, Some c -> sprintf "->%d/%s" n c.name
-    | n, None   -> sprintf "@@%d" n
+    | 0, Bcp (Some c) -> sprintf "->0/%s" c.name
+    | 0, Bcp None   -> "@0"
+    | n, Bcp (Some c) -> sprintf "->%d/%s" n c.name
+    | n, Bcp None   -> sprintf "@@%d" n
+    | _ -> assert false
 
   let value a =
     if a.is_true then sprintf "[T%s]" (level a)
@@ -200,7 +258,7 @@ module Make (E : Expr_intf.S)(Th : Theory_intf.S) = struct
   let pp_atom b a =
     bprintf b "%s%d%s [lit:%s] vpremise={{%a}}"
       (sign a) (a.var.vid+1) (value a) (Log.on_fmt E.Formula.print a.lit)
-      pp_premise a.var.vpremise
+      pp_premise a.var.tag.vpremise
 
   let pp_atoms_vec b vec =
     for i = 0 to Vec.size vec - 1 do
diff --git a/mcsolver/mcsolver_types.mli b/mcsolver/mcsolver_types.mli
index 02170f85..42cfda42 100644
--- a/mcsolver/mcsolver_types.mli
+++ b/mcsolver/mcsolver_types.mli
@@ -11,8 +11,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module type S = Solver_types_intf.S
+module type S = Mcsolver_types_intf.S
 
-module Make : functor (E : Expr_intf.S)(Th : Theory_intf.S)
-  -> S with type formula = E.Formula.t and type proof = Th.proof
+module Make : functor (E : Expr_intf.S)(Th : Plugin_intf.S)
+  -> S with type term= E.Term.t and type formula = E.Formula.t and type proof = Th.proof
 (** Functor to instantiate the types of clauses for the Solver. *)
diff --git a/mcsolver/mcsolver_types_intf.ml b/mcsolver/mcsolver_types_intf.ml
index 724bc3f3..c7bc10f9 100644
--- a/mcsolver/mcsolver_types_intf.ml
+++ b/mcsolver/mcsolver_types_intf.ml
@@ -14,22 +14,31 @@
 module type S = sig
   (** The signatures of clauses used in the Solver. *)
 
+  type term
   type formula
   type proof
 
-  type var = {
-    vid : int;
+
+  type 'a var =
+    { vid : int;
+      tag : 'a;
+      mutable weight : float;
+      mutable level : int; }
+
+  type semantic =
+    { term : term;
+      mutable assigned : term option; }
+
+  type boolean = {
     pa : atom;
     na : atom;
-    mutable weight : float;
     mutable seen : bool;
-    mutable level : int;
     mutable reason : reason;
     mutable vpremise : premise
   }
 
   and atom = {
-    var : var;
+    var : boolean var;
     lit : formula;
     neg : atom;
     mutable watched : clause Vec.t;
@@ -46,43 +55,46 @@ module type S = sig
     cpremise : premise
   }
 
-  and reason = clause option
+  and reason =
+      | Semantic of int
+      | Bcp of clause option
   and premise =
       | History of clause list
       | Lemma of proof
+
+  type elt =
+      | Term of semantic var
+      | Formula of boolean var
   (** Recursive types for literals (atoms) and clauses *)
 
-  val dummy_var : var
+  val dummy_var : boolean var
   val dummy_atom : atom
   val dummy_clause : clause
   (** Dummy values for use in vector dummys *)
 
-  val empty_clause : clause
-  (** The empty clause *)
+  val nb_vars : unit -> int
+  val get_var : int -> elt
+  val iter_vars : (elt -> unit) -> unit
+  (** Read access to the vector of variables created *)
 
   val add_atom : formula -> atom
   (** Returns the atom associated with the given formula *)
-
-  val make_var : formula -> var * bool
+  val add_term : term -> semantic var
+  (** Returns the variable associated with the term *)
+  val make_boolean_var : formula -> boolean var * bool
   (** Returns the variable linked with the given formula, and wether the atom associated with the formula
       is [var.pa] or [var.na] *)
 
+  val empty_clause : clause
+  (** The empty clause *)
   val make_clause : string -> atom list -> int -> bool -> premise -> clause
   (** [make_clause name atoms size learnt premise] creates a clause with the given attributes. *)
 
-  val nb_vars : unit -> int
-  val get_var : int -> var
-  val iter_vars : (var -> unit) -> unit
-  (** Read access to the vector of variables created *)
-
   val fresh_name : unit -> string
   val fresh_lname : unit -> string
   val fresh_dname : unit -> string
   (** Fresh names for clauses *)
 
-  val clear : unit -> unit
-  (** Forget all variables cretaed *)
-
   val print_atom : Format.formatter -> atom -> unit
   val print_clause : Format.formatter -> clause -> unit
   (** Pretty printing functions for atoms and clauses *)
diff --git a/mcsolver/plugin_intf.ml b/mcsolver/plugin_intf.ml
index 8358f3e7..6c267d6b 100644
--- a/mcsolver/plugin_intf.ml
+++ b/mcsolver/plugin_intf.ml
@@ -15,16 +15,23 @@
 module type S = sig
   (** Singature for theories to be given to the Solver. *)
 
+  type term
+  (** The type of terms. Should be compatible with Expr_intf.Term.t*)
+
   type formula
-  (** The type of formulas. Should be compatble with Formula_intf.S *)
+  (** The type of formulas. Should be compatble with Expr_intf.Formula.t *)
 
   type proof
   (** A custom type for the proofs of lemmas produced by the theory. *)
 
+  type assumption =
+    | Lit of formula
+    | Assign of term * term (* Assign(x, alpha) *)
+
   type slice = {
     start : int;
     length : int;
-    get : int -> formula;
+    get : int -> assumption;
     push : formula list -> proof -> unit;
   }
   (** The type for a slice of litterals to assume/propagate in the theory.
@@ -42,6 +49,10 @@ module type S = sig
     | Sat of level
     | Unsat of formula list * proof
 
+  type eval_res =
+    | Bool of bool
+    | Unknown
+
   val dummy : level
   (** A dummy level. *)
 
@@ -57,5 +68,14 @@ module type S = sig
   (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the
       same state as when it returned the value [l], *)
 
+  val assign : term -> term
+  (** Returns an assignment value for the given term. *)
+
+  val iter_assignable : (term -> unit) -> formula -> unit
+  (** An iterator over the subterms of a formula that should be assigned a value (usually the poure subterms) *)
+
+  val eval : formula -> eval_res
+  (** Returns the evaluation of the formula in the current assignment *)
+
 end