diff --git a/src/core/BitField.ml b/src/core/BitField.ml
new file mode 100644
index 00000000..bbb1f632
--- /dev/null
+++ b/src/core/BitField.ml
@@ -0,0 +1,135 @@
+(* This file is free software, part of containers. See file "license" for more details. *)
+
+(** {1 Bit Field} *)
+
+exception TooManyFields
+exception Frozen
+
+let max_width = Sys.word_size - 2
+
+(*$R
+  let module B = CCBitField.Make(struct end) in
+  let x = B.mk_field () in
+  let y = B.mk_field () in
+  let z = B.mk_field () in
+
+  let f = B.empty |> B.set x true |> B.set y true in
+
+  assert_bool "z_false" (not (B.get z f)) ;
+
+  assert_bool "z_true" (f |> B.set z true |> B.get z);
+*)
+
+(*$R
+  let module B = CCBitField.Make(struct end) in
+  let _ = B.mk_field () in
+  B.freeze();
+  assert_bool "must raise"
+    (try ignore (B.mk_field()); false with Frozen -> true);
+
+*)
+
+(*$R
+  let module B = CCBitField.Make(struct end) in
+
+  let x = B.mk_field () in
+  let y = B.mk_field () in
+  let z = B.mk_field () in
+  let u = B.mk_field () in
+  B.freeze();
+
+  let f = B.empty
+    |> B.set y true
+    |> B.set z true
+  in
+
+  assert_equal ~printer:CCInt.to_string 6 (f :> int) ;
+
+  assert_equal false (B.get x f) ;
+  assert_equal true (B.get y f) ;
+  assert_equal true (B.get z f);
+
+  let f' = B.set u true f in
+
+  assert_equal false (B.get x f') ;
+  assert_equal true (B.get y f') ;
+  assert_equal true (B.get z f');
+  assert_equal true (B.get u f');
+
+  ()
+*)
+
+
+module type S = sig
+  type t = private int
+  (** Generative type of bitfields. Each instantiation of the functor
+      should create a new, incompatible type *)
+
+  val empty : t
+  (** Empty bitfields (all bits 0) *)
+
+  type field
+
+  val get : field -> t -> bool
+  (** Get the value of this field *)
+
+  val set : field -> bool -> t -> t
+  (** Set the value of this field *)
+
+  val mk_field : unit -> field
+  (** Make a new field *)
+
+  val freeze : unit -> unit
+  (** Prevent new fields from being added. From now on, creating
+      a field will raise Frozen *)
+
+  val total_width : unit -> int
+  (** Current width of the bitfield *)
+end
+
+(* all bits from 0 to w-1 set to true *)
+let rec all_bits_ acc w =
+  if w=0 then acc
+  else
+    let acc = acc lor (1 lsl w-1) in
+    all_bits_ acc (w-1)
+
+(*$T
+  all_bits_ 0 1 = 1
+  all_bits_ 0 2 = 3
+  all_bits_ 0 3 = 7
+  all_bits_ 0 4 = 15
+*)
+
+(* increment and return previous value *)
+let get_then_incr n =
+  let x = !n in
+  incr n;
+  x
+
+module Make(X : sig end) : S = struct
+  type t = int
+
+  let empty = 0
+
+  let width_ = ref 0
+  let frozen_ = ref false
+
+  type field = int (* a mask *)
+
+  let[@inline] get field x = (x land field) <> 0
+
+  let[@inline] set field b x =
+    if b then x lor field else x land (lnot field)
+
+  let mk_field () =
+    if !frozen_ then raise Frozen;
+    let n = get_then_incr width_ in
+    if n > max_width then raise TooManyFields;
+    let mask = 1 lsl n in
+    mask
+
+  let freeze () = frozen_ := true
+
+  let total_width () = !width_
+end
diff --git a/src/core/BitField.mli b/src/core/BitField.mli
new file mode 100644
index 00000000..6821855e
--- /dev/null
+++ b/src/core/BitField.mli
@@ -0,0 +1,69 @@
+(* This file is free software, part of containers. See file "license" for more details. *)
+
+(** {1 Bit Field}
+
+    This module defines efficient bitfields
+    up to 30 or 62 bits (depending on the architecture) in
+    a relatively type-safe way.
+
+    {[
+      module B = CCBitField.Make(struct end);;
+
+      #install_printer B.pp;;
+
+      let x = B.mk_field ()
+      let y = B.mk_field ()
+      let z = B.mk_field ()
+
+      let f = B.empty |> B.set x true |> B.set y true;;
+
+      assert (not (B.get z f)) ;;
+
+      assert (f |> B.set z true |> B.get z);;
+
+    ]}
+*)
+
+exception TooManyFields
+(** Raised when too many fields are packed into one bitfield *)
+
+exception Frozen
+(** Raised when a frozen bitfield is modified *)
+
+val max_width : int
+(** System-dependent maximum width for a bitfield, typically 30 or 62 *)
+
+(** {2 Bitfield Signature} *)
+module type S = sig
+  type t = private int
+  (** Generative type of bitfields. Each instantiation of the functor
+      should create a new, incompatible type *)
+
+  val empty : t
+  (** Empty bitfields (all bits 0) *)
+
+  type field
+
+  val get : field -> t -> bool
+  (** Get the value of this field *)
+
+  val set : field -> bool -> t -> t
+  (** Set the value of this field *)
+
+  val mk_field : unit -> field
+  (** Make a new field *)
+
+  val freeze : unit -> unit
+  (** Prevent new fields from being added. From now on, creating
+      a field will raise Frozen *)
+
+  val total_width : unit -> int
+  (** Current width of the bitfield *)
+end
+
+(** Create a new bitfield type *)
+module Make(X : sig end) : S
+
+(**/**)
+val all_bits_ : int -> int -> int
+(**/**)
diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index fde95666..aaeb604b 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -250,9 +250,6 @@ module Make
 
   let new_atom p =
     let a = atom p in
-    (* This is necessary to ensure that the var will not be dropped
-       during the next backtrack. *)
-    a.var.used <- a.var.used + 1;
     insert_var_order (E_var a.var)
 
   (* Rather than iterate over all the heap when we want to decrease all the
@@ -335,12 +332,11 @@ module Make
         if seen a then duplicates := a :: !duplicates
         else (mark a; res := a :: !res)
       ) clause.atoms;
-    List.iter (fun a ->
-        begin match a.var.seen with
-          | Both -> trivial := true
-          | _ -> ()
-        end;
-        clear a.var) !res;
+    List.iter
+      (fun a ->
+         if seen_both a.var then trivial := true;
+         clear a.var)
+      !res;
     if !trivial then
       raise Trivial
     else if !duplicates = [] then
@@ -417,7 +413,6 @@ module Make
   let attach_clause c =
     assert (not c.attached);
     Log.debugf debug (fun k -> k "Attaching %a" St.pp_clause c);
-    Array.iter (fun a -> a.var.used <- a.var.used + 1) c.atoms;
     Vec.push c.atoms.(0).neg.watched c;
     Vec.push c.atoms.(1).neg.watched c;
     c.attached <- true;
@@ -657,8 +652,9 @@ module Make
               | Some Bcp cl -> history := cl :: !history
               | _ -> assert false
             end;
-            if not (q.var.seen = Both) then begin
-              q.var.seen <- Both;
+            if not (seen_both q.var) then (
+              mark q;
+              mark q.neg;
               seen := q :: !seen;
               if q.var.v_level > 0 then begin
                 var_bump_activity q.var;
@@ -669,7 +665,7 @@ module Make
                   blevel := max !blevel q.var.v_level
                 end
               end
-            end
+            )
           done
       end;
 
@@ -679,7 +675,7 @@ module Make
         Log.debugf debug (fun k -> k "  looking at: %a" St.pp a);
         match a with
         | Atom q ->
-          (not (q.var.seen = Both)) ||
+          (not (seen_both q.var)) ||
           (q.var.v_level < conflict_level)
         | Lit _ -> true
       do
diff --git a/src/core/Solver_types.ml b/src/core/Solver_types.ml
index 1fd4b7b7..7d39f029 100644
--- a/src/core/Solver_types.ml
+++ b/src/core/Solver_types.ml
@@ -18,6 +18,12 @@ Copyright 2016 Simon Cruanes
 
 module type S = Solver_types_intf.S
 
+module Var_fields = Solver_types_intf.Var_fields
+
+let v_field_seen_neg = Var_fields.mk_field()
+let v_field_seen_pos = Var_fields.mk_field()
+let () = Var_fields.freeze()
+
 (* Solver types for McSat Solving *)
 (* ************************************************************************ *)
 
@@ -49,8 +55,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     vid : int;
     pa : atom;
     na : atom;
-    mutable used : int;
-    mutable seen : seen;
+    mutable v_fields : Var_fields.t;
     mutable v_level : int;
     mutable v_idx: int; (** position in heap *)
     mutable v_weight : float; (** Weight (for the heap), tracking activity *)
@@ -99,8 +104,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
     { vid = -101;
       pa = dummy_atom;
       na = dummy_atom;
-      used = 0;
-      seen = Nope;
+      v_fields = Var_fields.empty;
       v_level = -1;
       v_weight = -1.;
       v_idx= -1;
@@ -169,8 +173,7 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
           { vid = !cpt_mk_var;
             pa = pa;
             na = na;
-            used = 0;
-            seen = Nope;
+            v_fields = Var_fields.empty;
             v_level = -1;
             v_idx= -1;
             v_weight = 0.;
@@ -217,28 +220,21 @@ module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
   let empty_clause = make_clause "Empty" [] (History [])
 
   (* Marking helpers *)
-  let clear v = v.seen <- Nope
+  let clear v = v.v_fields <- Var_fields.empty
 
   let seen a =
     let pos = (a == a.var.pa) in
-    match a.var.seen, pos with
-    | Nope, _ -> false
-    | Both, _
-    | Positive, true
-    | Negative, false -> true
-    | Positive, false
-    | Negative, true -> false
+    let field = if pos then v_field_seen_pos else v_field_seen_neg in
+    Var_fields.get field a.var.v_fields
+
+  let seen_both v =
+    Var_fields.get v_field_seen_pos v.v_fields &&
+    Var_fields.get v_field_seen_neg v.v_fields
 
   let mark a =
     let pos = (a == a.var.pa) in
-    match a.var.seen with
-    | Both -> ()
-    | Nope ->
-      a.var.seen <- (if pos then Positive else Negative)
-    | Positive ->
-      if pos then () else a.var.seen <- Both
-    | Negative ->
-      if pos then a.var.seen <- Both else ()
+    let field = if pos then v_field_seen_pos else v_field_seen_neg in
+    a.var.v_fields <- Var_fields.set field true a.var.v_fields
 
   (* Decisions & propagations *)
   type t =
diff --git a/src/core/Solver_types.mli b/src/core/Solver_types.mli
index b9e76a7a..1892d53c 100644
--- a/src/core/Solver_types.mli
+++ b/src/core/Solver_types.mli
@@ -28,6 +28,8 @@ Copyright 2016 Simon Cruanes
 module type S = Solver_types_intf.S
 (** Interface for the internal types. *)
 
+module Var_fields = Solver_types_intf.Var_fields
+
 module McMake (E : Expr_intf.S)(Dummy : sig end):
     S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof
 (** Functor to instantiate the types of clauses for a solver. *)
diff --git a/src/core/Solver_types_intf.ml b/src/core/Solver_types_intf.ml
index 24022f7d..ee97b4fb 100644
--- a/src/core/Solver_types_intf.ml
+++ b/src/core/Solver_types_intf.ml
@@ -22,6 +22,8 @@ Copyright 2016 Simon Cruanes
     used in the core solver.
 *)
 
+module Var_fields = BitField.Make(struct end)
+
 module type S = sig
   (** The signatures of clauses used in the Solver. *)
 
@@ -41,6 +43,10 @@ module type S = sig
     | Positive
     | Negative
 
+  (* TODO: hide these types (from the outside of [Msat]);
+     instead, provide well defined modules [module Lit : sig type t val …]
+     that define their API in Msat itself (not here) *)
+
   type lit = {
     lid : int;                      (** Unique identifier *)
     term : term;                    (** Wrapped term *)
@@ -55,8 +61,7 @@ module type S = sig
     vid : int;  (** Unique identifier *)
     pa : atom;  (** Link for the positive atom *)
     na : atom;  (** Link for the negative atom *)
-    mutable used : int;         (** Number of attached clause that contain the var *)
-    mutable seen : seen;        (** Boolean used during propagation *)
+    mutable v_fields : Var_fields.t; (** bool fields *)
     mutable v_level : int;      (** Level of decision/propagation *)
     mutable v_idx: int;         (** rank in variable heap *)
     mutable v_weight : float;   (** Variable weight (for the heap) *)
@@ -178,8 +183,13 @@ module type S = sig
 
   val mark : atom -> unit
   (** Mark the atom as seen, using the 'seen' field in the variable. *)
+
   val seen : atom -> bool
   (** Returns wether the atom has been marked as seen. *)
+
+  val seen_both : var -> bool
+  (** both atoms have been seen? *)
+
   val clear : var -> unit
   (** Clear the 'seen' field of the variable. *)