diff --git a/Makefile b/Makefile
index 189c9ccd2ae5a7015e2ca4f96d4a1e60e9c87541..015815ef7d6b7b1c9f2b0d12d0e1faa62a78ef57 100644
--- a/Makefile
+++ b/Makefile
@@ -19,7 +19,7 @@ promote:
 	dune promote --root=$$(pwd)
 
 check:
-	why3 prove --L src/lib  src/lib/cp.mlw
+	why3 prove --type-only -L src/lib  src/lib/*.mlw src/lib/constraints/*.mlw
 
 replay:
 	why3 replay -L src/lib  src/lib/cp
diff --git a/src/lib/all.mlw b/src/lib/all.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..57e93b6b3b6c782916a750f08c91dc491c796929
--- /dev/null
+++ b/src/lib/all.mlw
@@ -0,0 +1,1053 @@
+module All
+
+   use cp.DomI as Dom2I
+   use cp.DomB as Dom2B
+   use constraints.simple.Simple as Constraint2
+
+   clone cp.Engine with
+
+         type DomI.t = Dom2I.t,
+         type DomI.value = Dom2I.value,
+         predicate DomI.is_true_in = Dom2I.is_true_in,
+         predicate DomI.is_singleton = Dom2I.is_singleton,
+         val DomI.get_singleton = Dom2I.get_singleton,
+         val DomI.is_singleton = Dom2I.is_singleton,
+         val DomI.mk_singleton = Dom2I.mk_singleton,
+         val DomI.default_value = Dom2I.default_value,
+         function DomI.size = Dom2I.size,
+
+         type DomB.t = Dom2B.t,
+         type DomB.value = Dom2B.value,
+         predicate DomB.is_true_in = Dom2B.is_true_in,
+         predicate DomB.is_singleton = Dom2B.is_singleton,
+         val DomB.get_singleton = Dom2B.get_singleton,
+         val DomB.is_singleton = Dom2B.is_singleton,
+         val DomB.mk_singleton = Dom2B.mk_singleton,
+         val DomB.default_value = Dom2B.default_value,
+         function DomB.size = Dom2B.size,
+
+         type Constraint.t = Constraint2.t,
+         function Constraint.is_true_in = Constraint2.constraint_is_true_in,
+         function Constraint.vars = Constraint2.vars,
+         val propagate = Constraint2.propagate,
+         val check_model = Constraint2.check_model,
+         function size = Constraint2.size,
+         val Constraint.compute_vars_ti = Constraint2.compute_vars_ti,
+         val Constraint.compute_vars_tb = Constraint2.compute_vars_tb
+
+
+   use list.List
+   use cp.Type
+   use mach.int.Int
+
+   let start' (p:Prob.t) (minint:int) (maxint:int) : (model int bool)
+         ensures { forall v. S.mem v (defined_model result).Var.si -> minint <= get_mod_int result v <= maxint }
+         ensures { forall m:(interp int bool). is_model_of m result -> Prob.is_true_in m p }
+         raises { Unsat -> forall m:(interp int bool). (forall v. S.mem v (Prob.vars p).Var.si -> minint <= m.i v <= maxint) -> not (Prob.is_true_in m p) }
+         ensures { Var.equal_set (Prob.vars p) (defined_model result) }
+       =
+       let topbool = Dom2B.Top in
+       let topint = {Dom2I.min=minint; Dom2I.max=maxint} in
+       start p topbool topint
+
+end
+
+module API
+
+       use mach.int.Int
+       use bool.Bool
+       use list.List
+       use list.Mem as ListMem
+       use cp.Var as Var
+       use mach.int.Int63
+       use mach.peano.Peano as Peano
+       use mach.peano.Int63 as PeanoInt63
+       use constraints.simple.Simple as Constraint
+       use cp.ConstraintCst as ConstraintCst
+       use cp.ConstraintIsTrue as ConstraintIsTrue
+       use cp.ConstraintAdd as ConstraintAdd
+       use cp.ConstraintOr as ConstraintOr
+       use cp.ConstraintEquiv as ConstraintEquiv
+       use cp.ConstraintNot as ConstraintNot
+       use cp.ConstraintLe as ConstraintLe
+       use cp.ConstraintBoolPresent as ConstraintBoolPresent
+       use All
+       use set.Fset as S
+       use cp.Type as Type
+       use int.Int
+       use int.MinMax
+
+       type ti = Var.ti
+       type tb = Var.tb
+
+
+       type interp = Type.interp int bool
+
+       function i (m:interp) : ti -> int = m.Type.i
+
+       function b (m:interp) : tb -> bool = m.Type.b
+
+       let function true_ : tb = { Var.vb = 1 }
+       let function zero_ : ti = { Var.vi = 1 }
+
+       type context = {
+            mutable intmin : int;
+            mutable intmax : int;
+            mutable ghost sti: S.fset ti;
+            mutable nexti: Peano.t;
+            mutable ghost stb: S.fset tb;
+            mutable nextb: Peano.t;
+            mutable prob: list Constraint.t;
+       }
+       invariant { forall v. S.mem v sti <-> 1 <= v.Var.vi < nexti }
+       invariant { forall v. S.mem v stb <-> 1 <= v.Var.vb < nextb }
+       invariant { S.mem true_ stb }
+       invariant { S.mem zero_ sti }
+       invariant { 2 <= nexti }
+       invariant { 2 <= nextb }
+       invariant { forall m. All.Engine.Prob.is_true_in m prob -> m.Type.b true_ }
+       invariant { forall m. All.Engine.Prob.is_true_in m prob -> m.Type.i zero_ = 0 }
+       invariant { forall m. All.Engine.Prob.is_true_in m prob ->
+                                       forall vi. S.mem vi sti ->
+                                                 intmin <= m.Type.i vi <= intmax }
+       invariant { (S.(==) (All.Engine.Prob.vars prob).Var.si sti) } 
+       invariant { (S.(==) (All.Engine.Prob.vars prob).Var.sb stb) } 
+       by {
+        intmin = 0;
+        intmax = 0;
+        sti = S.add zero_ S.empty;
+        stb = S.add true_ S.empty;
+        nexti = Peano.succ Peano.one;
+        nextb = Peano.succ Peano.one;
+        prob =
+             Cons (Constraint.Cst { ConstraintCst.v = zero_; ConstraintCst.i = 0; ConstraintCst.b = true_ })
+             (Cons (Constraint.IsTrue { ConstraintIsTrue.b = true_ })
+              Nil);
+       }
+
+       predicate is_true_in (m:interp) (c:context) =
+            All.Engine.Prob.is_true_in m c.prob
+
+       let create_vari (c:context) (min_:int) (max_:int) : ti
+           ensures { not (S.mem result (old c.sti)) }
+           ensures { c.sti = S.add result (old c.sti) }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ min_ <= m.i result <= max_ ) }
+         =
+          c.nexti <- Peano.succ c.nexti;
+          let r = { Var.vi = PeanoInt63.to_int63 c.nexti - 1 } in
+          c.sti <- S.add r c.sti;
+          c.intmin <- min c.intmin min_;
+          c.intmax <- max c.intmax max_;
+          let ctr1 = { ConstraintLe.v1 = r; ConstraintLe.v2 = zero_;
+                                   ConstraintLe.i = max_; ConstraintLe.b = true_ } in
+          let ctr2 = { ConstraintLe.v1 = zero_; ConstraintLe.v2 = r;
+                                  ConstraintLe.i = - min_; ConstraintLe.b = true_ } in
+          c.prob <- Cons (Constraint.Le ctr1) (Cons (Constraint.Le ctr2) c.prob);
+          assert { ListMem.mem (Constraint.Le ctr1) c.prob };
+          assert { ListMem.mem (Constraint.Le ctr2) c.prob };
+          assert { forall ctr. ListMem.mem ctr (old c.prob) -> ListMem.mem ctr c.prob };
+          assert { forall m. All.Engine.Prob.is_true_in m c.prob -> ConstraintLe.constraint_is_true_in m ctr1 };
+          assert { forall m. All.Engine.Prob.is_true_in m c.prob -> ConstraintLe.constraint_is_true_in m ctr2 };
+          assert { forall v. S.mem v (All.Engine.Prob.vars c.prob).Var.si -> (v = r \/ v = zero_ \/ old (S.mem v (All.Engine.Prob.vars c.prob).Var.si)) };
+          r
+
+       let create_varb (c:context) : tb
+           ensures { not (S.mem result (old c.stb)) }
+           ensures { c.stb = S.add result (old c.stb) }
+           ensures { result.Var.vb <> true_.Var.vb }
+         =
+          if PeanoInt63.to_int63 c.nextb = true_.Var.vb then c.nextb <- Peano.succ c.nextb;
+          c.nextb <- Peano.succ c.nextb;
+          let r = { Var.vb = PeanoInt63.to_int63 c.nextb - 1 } in
+          let _ = PeanoInt63.to_int63 c.nextb in
+          c.stb <- S.add r c.stb;
+          c.prob <- Cons (Constraint.BoolPresent { ConstraintBoolPresent.b1 = r }) c.prob;
+          r
+
+       let create_context ()
+           ensures { forall m. is_true_in m result <-> (m.b true_ /\ m.i zero_ = 0) }
+       =
+         let c = {
+           intmin = 0;
+           intmax = 0;
+           sti = S.add zero_ S.empty;
+           nexti = Peano.succ Peano.one;
+           stb = S.add true_ S.empty;
+           nextb = Peano.succ Peano.one;
+           prob =
+             Cons (Constraint.Cst { ConstraintCst.v = zero_; ConstraintCst.i = 0; ConstraintCst.b = true_ })
+             (Cons (Constraint.IsTrue { ConstraintIsTrue.b = true_ })
+              Nil);
+         } in
+         c
+
+       lemma true_is_true: forall c:context. forall m. is_true_in m c -> m.b true_
+       lemma zero_is_zero: forall c:context. forall m. is_true_in m c -> m.i zero_ = 0
+
+       let is_cst_reif (c:context) (v:ti) (iv:int) (r:tb)
+           requires { S.mem v c.sti }
+           requires { S.mem r c.stb }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v = iv) ) }
+       =
+       c.prob <- Cons ((Constraint.Cst {
+              ConstraintCst.v = v;
+              ConstraintCst.i = iv;
+              ConstraintCst.b = r })) c.prob
+
+       let is_cst (c:context) (v:ti) (iv:int)
+           requires { S.mem v c.sti }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v = iv ) }
+       =
+        is_cst_reif c v iv true_
+
+       let add_reif (c:context) (v1:ti) (v2:ti) (v3:ti) (r:tb)
+           requires { S.mem v1 c.sti }
+           requires { S.mem v2 c.sti }
+           requires { S.mem v3 c.sti }
+           requires { S.mem r c.stb }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v1 + m.i v2 = m.i v3) ) }
+       =
+       c.prob <- Cons ((Constraint.Add {
+              ConstraintAdd.v1 = v1;
+              ConstraintAdd.v2 = v2;
+              ConstraintAdd.v3 = v3;
+              ConstraintAdd.b = r })) c.prob
+
+       let add (c:context) (v1:ti) (v2:ti) (v3:ti)
+           requires { S.mem v1 c.sti }
+           requires { S.mem v2 c.sti }
+           requires { S.mem v3 c.sti }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v1 + m.i v2 = m.i v3 ) }
+       =
+        add_reif c v1 v2 v3 true_
+
+       let le_reif (c:context) (v1:ti) (v2:ti) (cst:int) (r:tb)
+           requires { S.mem v1 c.sti }
+           requires { S.mem v2 c.sti }
+           requires { S.mem r c.stb }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v1 <= m.i v2 + cst) ) }
+       =
+       c.prob <- Cons ((Constraint.Le {
+              ConstraintLe.v1 = v1;
+              ConstraintLe.v2 = v2;
+              ConstraintLe.i = cst;
+              ConstraintLe.b = r })) c.prob
+
+       let le (c:context) (v1:ti) (v2:ti) (cst:int)
+           requires { S.mem v1 c.sti }
+           requires { S.mem v2 c.sti }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v1 <= m.i v2 + cst ) }
+       =
+        le_reif c v1 v2 cst true_
+
+
+       let or (c:context) (b1:tb) (b2:tb) (b3:tb)
+           requires { S.mem b1 c.stb }
+           requires { S.mem b2 c.stb }
+           requires { S.mem b3 c.stb }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b b3 <-> (m.b b1) \/ (m.b b2))) }
+       =
+       c.prob <- Cons ((Constraint.Or {
+              ConstraintOr.b1 = b1;
+              ConstraintOr.b2 = b2;
+              ConstraintOr.b3 = b3;
+              })) c.prob
+
+       let equiv (c:context) (b1:tb) (b2:tb) (b3:tb)
+           requires { S.mem b1 c.stb }
+           requires { S.mem b2 c.stb }
+           requires { S.mem b3 c.stb }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b b3 <-> ((m.b b1) <-> (m.b b2)))) }
+       =
+       c.prob <- Cons ((Constraint.Equiv {
+              ConstraintEquiv.b1 = b1;
+              ConstraintEquiv.b2 = b2;
+              ConstraintEquiv.b3 = b3;
+              })) c.prob
+
+       let not_ (c:context) (b1:tb) (b2:tb)
+           requires { S.mem b1 c.stb }
+           requires { S.mem b2 c.stb }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b b2 <-> not (m.b b1))) }
+       =
+       c.prob <- Cons ((Constraint.Not {
+              ConstraintNot.b1 = b1;
+              ConstraintNot.b2 = b2;
+              })) c.prob
+
+       let is_true (c:context) (b1:tb)
+           requires { S.mem b1 c.stb }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.b b1) }
+       =
+       c.prob <- Cons (Constraint.IsTrue { ConstraintIsTrue.b = b1 })
+                 c.prob
+
+
+      let solve (c:context) : Type.model int bool
+          ensures { is_true_in (All.Engine.interp_of_model result) c }
+          ensures { Var.equal_set (All.Engine.Prob.vars c.prob) (Type.defined_model result) }
+          raises { Type.Unsat -> forall m. not (is_true_in m c) } =
+          All.start' c.prob c.intmin c.intmax
+
+end
+
+module APIDefensive
+
+       use mach.int.Int
+       use bool.Bool
+       use list.List
+       use list.Mem as ListMem
+       use cp.Var as Var
+       use mach.int.Int63
+       use mach.peano.Peano as Peano
+       use mach.peano.Int63 as PeanoInt63
+       use constraints.simple.Simple as Constraint
+       use cp.ConstraintCst as ConstraintCst
+       use cp.ConstraintIsTrue as ConstraintIsTrue
+       use cp.ConstraintAdd as ConstraintAdd
+       use cp.ConstraintOr as ConstraintOr
+       use cp.ConstraintNot as ConstraintNot
+       use cp.ConstraintLe as ConstraintLe
+       use All
+       use set.Fset as S
+       use cp.Type as Type
+       use int.Int
+       use int.MinMax
+       use import API as API
+
+       type ti = Var.ti
+       type tb = Var.tb
+
+
+       type interp = Type.interp int bool
+
+       function i (m:interp) : ti -> int = m.Type.i
+
+       function b (m:interp) : tb -> bool = m.Type.b
+
+       let function true_ : tb = API.true_
+       let function zero_ : ti = API.zero_
+
+       type context = API.context
+       predicate is_true_in (m:interp) (c:context) = API.is_true_in m c
+
+       let create_vari (c:context) (min_:int) (max_:int) : ti
+           ensures { not (S.mem result (old c.sti)) }
+           ensures { c.sti = S.add result (old c.sti) }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ min_ <= m.i result <= max_ ) }
+         =
+          API.create_vari c min_ max_
+
+       let create_varb (c:context) : tb
+           ensures { not (S.mem result (old c.stb)) }
+           ensures { c.stb = S.add result (old c.stb) }
+           ensures { result.Var.vb <> true_.Var.vb }
+         =
+          API.create_varb c
+
+       let create_context ()
+           ensures { forall m. is_true_in m result <-> (m.b true_ /\ m.i zero_ = 0) }
+       =
+        API.create_context ()
+
+       lemma true_is_true: forall c:context. forall m. is_true_in m c -> m.b true_
+       lemma zero_is_zero: forall c:context. forall m. is_true_in m c -> m.i zero_ = 0
+
+       exception UnknownVariable
+
+       let check_ti (c:context) (v:ti) : unit
+           raises { UnknownVariable -> not (S.mem v c.sti) }
+           ensures { S.mem v c.sti } =
+            if 1 <= v.Var.vi < (PeanoInt63.to_int63 c.nexti) then ()
+            else raise UnknownVariable
+
+       let check_tb (c:context) (v:tb) : unit
+           raises { UnknownVariable -> not (S.mem v c.stb) }
+           ensures { S.mem v c.stb } =
+            if 1 <= v.Var.vb < (PeanoInt63.to_int63 c.nextb) then ()
+            else raise UnknownVariable
+
+       let is_cst_reif (c:context) (v:ti) (iv:int) (r:tb)
+           raises { UnknownVariable -> not (S.mem v c.sti) \/ not (S.mem r c.stb) }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v = iv) ) }
+       =
+        check_ti c v;
+        check_tb c r;
+        API.is_cst_reif c v iv r
+
+       let is_cst (c:context) (v:ti) (iv:int)
+           raises { UnknownVariable -> not (S.mem v c.sti) }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v = iv ) }
+       =
+        check_ti c v;
+        API.is_cst c v iv
+
+       let add_reif (c:context) (v1:ti) (v2:ti) (v3:ti) (r:tb)
+           raises { UnknownVariable -> not (S.mem v1 c.sti) \/ not (S.mem v2 c.sti) \/ not (S.mem v3 c.sti) \/ not (S.mem r c.stb) }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v1 + m.i v2 = m.i v3) ) }
+       =
+        check_ti c v1;
+        check_ti c v2;
+        check_ti c v3;
+        check_tb c r;
+        API.add_reif c v1 v2 v3 r
+
+       let add (c:context) (v1:ti) (v2:ti) (v3:ti)
+           raises { UnknownVariable -> not (S.mem v1 c.sti) \/ not (S.mem v2 c.sti) \/ not (S.mem v3 c.sti) }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v1 + m.i v2 = m.i v3 ) }
+       =
+        check_ti c v1;
+        check_ti c v2;
+        check_ti c v3;
+        API.add c v1 v2 v3
+
+       let le_reif (c:context) (v1:ti) (v2:ti) (cst:int) (r:tb)
+           raises { UnknownVariable -> not (S.mem v1 c.sti) \/ not (S.mem v2 c.sti) \/ not (S.mem r c.stb) }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v1 <= m.i v2 + cst) ) }
+       =
+        check_ti c v1;
+        check_ti c v2;
+        check_tb c r;
+        API.le_reif c v1 v2 cst r
+
+       let le (c:context) (v1:ti) (v2:ti) (cst:int)
+           raises { UnknownVariable -> not (S.mem v1 c.sti) \/ not (S.mem v2 c.sti) }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v1 <= m.i v2 + cst ) }
+       =
+        check_ti c v1;
+        check_ti c v2;
+        API.le c v1 v2 cst
+
+       let or (c:context) (b1:tb) (b2:tb) (b3:tb)
+           raises { UnknownVariable -> not (S.mem b1 c.stb) \/ not (S.mem b2 c.stb) \/ not (S.mem b3 c.stb) }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b b3 <-> (m.b b1) \/ (m.b b2))) }
+       =
+        check_tb c b1;
+        check_tb c b2;
+        check_tb c b3;
+        API.or c b1 b2 b3
+
+       let equiv (c:context) (b1:tb) (b2:tb) (b3:tb)
+           raises { UnknownVariable -> not (S.mem b1 c.stb) \/ not (S.mem b2 c.stb) \/ not (S.mem b3 c.stb) }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b b3 <-> ((m.b b1) <-> (m.b b2)))) }
+       =
+        check_tb c b1;
+        check_tb c b2;
+        check_tb c b3;
+        API.equiv c b1 b2 b3
+
+       let not_ (c:context) (b1:tb) (b2:tb)
+           raises { UnknownVariable -> not (S.mem b1 c.stb) \/ not (S.mem b2 c.stb) }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b b2 <-> not (m.b b1))) }
+       =
+        check_tb c b1;
+        check_tb c b2;
+        API.not_ c b1 b2
+
+       let is_true (c:context) (b1:tb)
+           raises { UnknownVariable -> not (S.mem b1 c.stb) }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b b1)) }
+       =
+        check_tb c b1;
+        API.is_true c b1
+
+      type model = {
+           mod : Type.model int bool;
+           lasti: int63;
+           lastb: int63;
+        }
+       invariant { forall v. 1 <= v.Var.vi <= lasti <-> S.mem v (Type.defined_model mod).Var.si  }
+       invariant { forall v. 1 <= v.Var.vb <= lastb <-> S.mem v (Type.defined_model mod).Var.sb  }
+       by { mod =
+            (let hi = Var.Hi.create (-1) (0:int) S.empty in
+             let hb = Var.Hb.create (-1) true S.empty in
+             { Type.modi = Var.Hi.copy_lock hi; Type.modb = Var.Hb.copy_lock hb });
+           lasti = 0; lastb = 0; }
+
+      let solve (c:context) : model
+          ensures { is_true_in (All.Engine.interp_of_model result.mod) c }
+          raises { Type.Unsat -> forall m. not (is_true_in m c) } =
+          {
+              mod = API.solve c;
+            lasti = PeanoInt63.to_int63 (Peano.pred c.nexti);
+            lastb = PeanoInt63.to_int63 (Peano.pred c.nextb);
+          }
+
+      let get_model_i (m:model) (v:ti): int
+          raises { UnknownVariable -> not (S.mem v (Type.defined_model m.mod).Var.si) }
+          ensures { Type.get_mod_int m.mod v = result } =
+          if 1 <= v.Var.vi <= m.lasti then ()
+          else raise UnknownVariable;
+          m.mod.Type.modi.Var.Hi.Lock.find v
+
+      let get_model_b (m:model) (v:tb): bool
+          raises { UnknownVariable -> not ( S.mem v (Type.defined_model m.mod).Var.sb) }
+          ensures { Type.get_mod_bool m.mod v = result } =
+          if 1 <= v.Var.vb <= m.lastb then ()
+          else raise UnknownVariable;
+          m.mod.Type.modb.Var.Hb.Lock.find v
+
+end
+
+
+
+(*
+module APIIntf
+(** commentaires *)
+       use mach.int.Int
+       use bool.Bool
+       use set.Fset as S
+       use list.List
+       use list.Mem as ListMem
+       use map.Map as Map
+
+       type int_var
+       type bool_var
+
+       type finite_mapping 'a 'b = abstract {
+            mapping: 'a -> 'b;
+            defined: S.fset 'a;
+       }
+
+       predicate extended (fm1:finite_mapping 'a 'b) (fm2:finite_mapping 'a 'b) (k:'a) (v:'b) =
+                 fm2.mapping = Map.set fm1.mapping k v /\
+                 fm2.defined = S.add k fm2.defined
+
+       type interp = abstract {
+            fm_int: finite_mapping int_var int;
+            fm_bool: finite_mapping bool_var bool;
+       }
+
+       function i (m:interp) : int_var -> int = m.fm_int.mapping
+       function b (m:interp) : bool_var -> bool = m.fm_bool.mapping
+
+       val function empty_interp: interp
+
+       axiom def_empty_interp:
+             empty_interp.fm_int.defined = S.empty /\
+             empty_interp.fm_bool.defined = S.empty
+
+
+       (** Inteprétation, une valuation, assigment *)
+
+       type interp_set = abstract { (** rename interp_set, infinite *)
+            mutable int_vars: S.fset int_var; (** finite set of usable integer variable *)
+            mutable bool_vars: S.fset bool_var; (** finite set of usable boolean variable *)
+            mutable interps: S.fset interp;
+       }
+       invariant { forall m. S.mem m interps -> int_vars = m.fm_int.defined }
+       invariant { forall m. S.mem m interps -> bool_vars = m.fm_bool.defined }
+       by {
+        interps = S.empty;
+        int_vars = S.empty;
+        bool_vars = S.empty;
+       }
+
+       (** tells if an interpretation is in the set of interpretion *)
+       predicate mem (m:interp) (c:interp_set) =
+                 S.mem m c.interps
+
+       (** start with all possible interpreatation *)
+       val create_interp_set () : interp_set
+           ensures { result.int_vars = S.empty }
+           ensures { result.bool_vars = S.empty }
+           ensures { S.cardinal result.interps = 1 }
+
+       val partial create_int_var (c:interp_set) (intmin:int) (intmax:int) : int_var
+           ensures { not (S.mem result (old c.int_vars)) }
+           ensures { c.int_vars = S.add result (old c.int_vars) }
+
+           ensures { forall m:interp. (old mem m c) -> forall i. intmin <= i <= intmax ->
+                        exists m'. mem m' c /\ extended m.fm_int m'.fm_int result i }
+           ensures { forall m':interp. (mem m' c) ->
+                        intmin <= m'.i result <= intmax /\
+                        exists m. (old mem m c) /\ extended m.fm_int m'.fm_int result (m'.i result) }
+
+           writes { c.int_vars }
+
+       val partial create_bool_var (c:interp_set) : bool_var
+           ensures { not (S.mem result (old c.bool_vars)) }
+           ensures { c.bool_vars = S.add result (old c.bool_vars) }
+
+           ensures { forall m:interp. (old mem m c) -> forall i.
+                        exists m'. mem m' c /\ extended m.fm_bool m'.fm_bool result i }
+           ensures { forall m':interp. (mem m' c) ->
+                        exists m. (old mem m c) /\ extended m.fm_bool m'.fm_bool result (m'.b result) }
+
+           writes { c.bool_vars }
+
+       (** We keep only from the set of interpretation the interpetation where [r] is true *)
+       val is_true (c:interp_set) (r:bool_var) : unit
+           requires { S.mem r c.bool_vars }
+           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r) ) }
+
+       (** Remove from the set of interpretation the interpetation where [r1] and [r2] are not opposite *)
+       val not_ (c:interp_set) (r1:bool_var) (r2:bool_var) : unit
+           requires { S.mem r1 c.bool_vars }
+           requires { S.mem r2 c.bool_vars }
+           ensures { forall m. mem m c <-> ((old mem m c) /\ notb (m.b r1) = m.b r2 ) }
+
+       (** Remove from the set of interpretation the interpetation where we don't have r = (v = iv) *)
+       val is_cst_reif (c:interp_set) (v:int_var) (iv:int) (r:bool_var) : unit
+           requires { S.mem v c.int_vars }
+           requires { S.mem r c.bool_vars }
+           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r <-> m.i v = iv) ) }
+           writes { c }
+
+       val add_reif (c:interp_set) (v1:int_var) (v2:int_var) (v3:int_var) (r:bool_var) : unit
+           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r <-> m.i v1 + m.i v2 = m.i v3) ) }
+           writes { c }
+
+       (** Remove from the set of interpretation the interpetation where [r1] and [r2] are not opposite *)
+       val le_reif (c:interp_set) (v1:int_var) (cst:int) (v2:int_var) (r:bool_var) : unit
+           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r <-> m.i v1 <= cst + m.i v2) ) }
+           writes { c }
+
+       exception Unsat
+
+       (** Create a model that belongs to the set of interpretation, if one exists. Otherwise raise Unsat *)
+       val partial solve (c:interp_set) : interp
+           (** The model is mem *)
+           ensures { mem result c }
+           raises { Unsat -> forall m. not (mem m c) } (** is_empty c *)
+
+       (** Create a model that belongs to the set of interpretation, if one exists. Otherwise raise Unsat *)
+       val partial solve_all (c:interp_set) : list interp
+           (** The model is mem *)
+           ensures { forall m. mem m c -> ListMem.mem m result }
+           raises { Unsat -> forall m. not (mem m c) } (** is_empty c *)
+
+       val get_int (m:interp) (v:int_var) : int
+           requires { S.mem v m.fm_int.defined }
+           ensures { result = m.i v }
+
+       val get_bool (m:interp) (v:bool_var) : bool
+           requires { S.mem v m.fm_bool.defined }
+           ensures { result = m.b v }
+
+end
+
+(**
+
+       let () =
+         let cxt = create_context () in
+         let a = create_vari cxt 0 10 in
+         let b = create_vari cxt 0 10 in
+         let c = create_vari cxt 0 10 in
+         add cxt a b c;
+         add cxt a c b;
+         let m = solve cxt in
+         let vc = get_int m c in
+         ....
+
+*)
+
+
+module API
+
+       use mach.int.Int
+       use bool.Bool
+       use list.List
+       use Var as Var
+       use mach.int.Int63
+       use mach.peano.Peano as Peano
+       use mach.peano.Int63 as PeanoInt63
+       use ConstraintSimple as Constraint
+       use ConstraintCst as ConstraintCst
+       use ConstraintIsTrue as ConstraintIsTrue
+       use ConstraintAdd as ConstraintAdd
+       use ConstraintLe as ConstraintLe
+       use ConstraintOr as ConstraintOr
+       use ConstraintNot as ConstraintNot
+       use All
+       use set.Fset as S
+       use map.Map as Map
+       use Type as Type
+       use list.Mem as ListMem
+
+
+       type int_var = Var.ti
+       type bool_var = Var.tb
+
+       type finite_mapping 'a 'b = {
+            mapping: 'a -> 'b;
+            defined: S.fset 'a;
+       }
+
+       predicate extended (fm1:finite_mapping 'a 'b) (fm2:finite_mapping 'a 'b) (k:'a) (v:'b) =
+                 fm2.mapping = Map.set fm1.mapping k v /\
+                 fm2.defined = S.add k fm2.defined
+
+       type interp = {
+            fm_int: finite_mapping int_var int;
+            fm_bool: finite_mapping bool_var bool;
+            model: Type.model int bool;
+       }
+       invariant { fm_int.mapping = model.Type.modi.Var.Hi.Lock.contents }
+       invariant { fm_int.defined = model.Type.modi.Var.Hi.Lock.defined }
+       invariant { fm_bool.mapping = model.Type.modb.Var.Hb.Lock.contents }
+       invariant { fm_bool.defined = model.Type.modb.Var.Hb.Lock.defined }
+
+       function i (m:interp) : int_var -> int = m.fm_int.mapping
+       function b (m:interp) : bool_var -> bool = m.fm_bool.mapping
+
+       (** Inteprétation, une valuation, assigment *)
+
+       let function true_ : bool_var = { Var.vb = 1 }
+       let function zero_ : int_var  = { Var.vi = 1 }
+
+       let ghost mk_interp (m:Type.model int bool) : interp =
+          {
+                fm_int = {
+                       mapping = m.Type.modi.Var.Hi.Lock.contents;
+                       defined = m.Type.modi.Var.Hi.Lock.defined;
+                };
+                fm_bool = {
+                       mapping = m.Type.modb.Var.Hb.Lock.contents;
+                       defined = m.Type.modb.Var.Hb.Lock.defined;
+                };
+                model = m;
+           }
+
+       let ghost base_interp () : interp
+           ensures { result.fm_int.defined = S.add zero_ S.empty }
+           ensures { result.fm_bool.defined = S.add true_ S.empty }
+           ensures { result.fm_int.mapping zero_ = 0 }
+           ensures { result.fm_bool.mapping true_ = true }
+       =
+           let modi = Var.Hi.create 2 0 (S.add zero_ S.empty) in
+           let modb = Var.Hb.create 2 true (S.add true_ S.empty) in
+           Var.Hi.set modi zero_ 0;
+           Var.Hb.set modb true_ true;
+           let p = mk_interp {
+               Type.modi = Var.Hi.copy_lock modi;
+               Type.modb = Var.Hb.copy_lock modb;
+           }
+           in
+           p
+
+       type interp_set = {
+            ghost mutable int_vars: S.fset int_var;
+            ghost mutable bool_vars: S.fset bool_var;
+            ghost mutable interps: S.fset interp;
+            mutable intmin : int;
+            mutable intmax : int;
+            mutable nexti: Peano.t;
+            mutable nextb: Peano.t;
+            mutable prob: list Constraint.t;
+       }
+       invariant { forall m. S.mem m interps -> int_vars = m.fm_int.defined }
+       invariant { forall m. S.mem m interps -> bool_vars = m.fm_bool.defined }
+       invariant { forall v. S.mem v int_vars -> 1 <= v.Var.vi < nexti }
+       invariant { forall v. S.mem v bool_vars -> 1 <= v.Var.vb < nextb }
+       invariant { let s = All.Engine.Prob.vars prob in
+                   (int_vars = s.Var.si)
+                /\ (bool_vars = s.Var.sb) }
+       invariant { 2 <= nexti }
+       invariant { 2 <= nextb }
+       invariant { S.mem true_ bool_vars }
+       invariant { forall m. All.Engine.Prob.is_true_in m prob -> m.Type.b true_ }
+       invariant { forall m. All.Engine.Prob.is_true_in m prob -> m.Type.i zero_ = 0 }
+       invariant { forall m. All.Engine.Prob.is_true_in m prob ->
+                   forall v. S.mem v int_vars -> intmin <= m.Type.i v <= intmax }
+       by {
+        interps = S.add (base_interp ()) S.empty;
+        intmin = 0;
+        intmax = 0;
+        int_vars = S.add zero_ S.empty;
+        bool_vars = S.add true_ S.empty;
+        nexti = Peano.succ Peano.one;
+        nextb = Peano.succ Peano.one;
+        prob =
+             (Cons (Constraint.Cst { ConstraintCst.v = zero_; ConstraintCst.i = 0; ConstraintCst.b = true_ })
+             (Cons (Constraint.IsTrue { ConstraintIsTrue.b = true_ })
+              Nil));
+       }
+
+       (** tells if an interpretation is in the set of interpretion *)
+       predicate mem (m:interp) (c:interp_set) =
+            m.fm_int.defined = c.int_vars /\ m.fm_bool.defined = c.bool_vars /\
+            All.Engine.Prob.is_true_in (All.Engine.interp_of_model m.model) c.prob
+
+
+       axiom only_defined_int: forall m c. mem m c -> c.int_vars = m.fm_int.defined
+       axiom only_defined_bool: forall m c. mem m c -> c.bool_vars = m.fm_bool.defined
+
+       (** start with all possible interpreatation *)
+       let create_interp_set () : interp_set
+           ensures { S.cardinal result.interps = 1 }
+       =
+         let c = {
+           interps = S.add (base_interp ()) S.empty;
+           intmin = 0;
+           intmax = 0;
+           int_vars = S.add zero_ S.empty;
+           nexti = Peano.succ Peano.one;
+           bool_vars = S.add true_ S.empty;
+           nextb = Peano.succ Peano.one;
+           prob =
+             (Cons (Constraint.Cst { ConstraintCst.v = zero_; ConstraintCst.i = 0; ConstraintCst.b = true_ })
+             (Cons (Constraint.IsTrue { ConstraintIsTrue.b = true_ })
+              Nil));
+         } in
+         c
+
+       type iter_fset 'a = {
+            mutable iter_fset_todo: S.fset 'a;
+            mutable iter_fset_done: S.fset 'a;
+            iter_fset_all: S.fset 'a;
+       }
+       invariant { S.(==) iter_fset_all (S.union iter_fset_done iter_fset_todo) }
+       invariant { S.(inter iter_fset_done iter_fset_todo == S.empty) }
+       by {
+         iter_fset_todo = S.empty;
+         iter_fset_done = S.empty;
+         iter_fset_all = S.empty;
+       }
+
+       let ghost create_iter_fset (s:S.fset 'a) : iter_fset 'a =
+        {
+         iter_fset_todo = s;
+         iter_fset_done = S.empty;
+         iter_fset_all = s
+        }
+
+       let ghost is_empty_iter_fset (s:iter_fset 'a) : bool
+          ensures { result = (S.is_empty s.iter_fset_todo) }
+         =
+           S.is_empty s.iter_fset_todo
+
+       let ghost next_iter_fset (s:iter_fset 'a) : 'a
+          requires { not (S.is_empty s.iter_fset_todo) }
+          ensures { S.mem result (old s.iter_fset_todo) }
+          ensures { s.iter_fset_todo = S.remove result (old s.iter_fset_todo) }
+          ensures { s.iter_fset_done = S.add result (old s.iter_fset_done) }
+         =
+           let e = S.pick s.iter_fset_todo in
+           s.iter_fset_todo <- S.remove e s.iter_fset_todo;
+           s.iter_fset_done <- S.add e s.iter_fset_done;
+           e
+
+       function variant_iter_fset (s:iter_fset 'a) : int
+           = S.cardinal s.iter_fset_todo
+
+       use ref.Ref
+
+       let partial create_int_var (c:interp_set) (intmin:int) (intmax:int) : int_var
+           ensures { not (S.mem result (old c.int_vars)) }
+           ensures { c.int_vars = S.add result (old c.int_vars) }
+
+           ensures { forall m:interp. (old mem m c) -> forall i. intmin <= i <= intmax ->
+                        exists m'. mem m' c /\ extended m.fm_int m'.fm_int result i }
+           ensures { forall m':interp. (mem m' c) ->
+                        intmin <= m'.i result <= intmax /\
+                        exists m. (old mem m c) /\ extended m.fm_int m'.fm_int result (m'.i result) }
+         =
+          c.nexti <- Peano.succ c.nexti;
+          let r = { Var.vi = (PeanoInt63.to_int63 c.nexti) - 1 } in
+          c.int_vars <- S.add r c.int_vars;
+          let constraint_min =
+              Constraint.Le { ConstraintLe.v1 = zero_; ConstraintLe.v2 = r;
+                              ConstraintLe.i = - intmin; ConstraintLe.b = true_}
+          in
+          let constraint_max =
+              Constraint.Le { ConstraintLe.v1 = r; ConstraintLe.v2 = zero_;
+                              ConstraintLe.i = intmax; ConstraintLe.b = true_}
+          in
+          c.prob <- Cons constraint_min (Cons constraint_max c.prob);
+          let ghost ref interps' = S.empty in
+          let ghost () =
+           if intmin <= intmax then
+             let iter = create_iter_fset c.interps in
+             while not (is_empty_iter_fset iter); do
+               variant { variant_iter_fset iter }
+               invariant { forall m:interp. S.mem m iter.iter_fset_done -> forall i. intmin <= i <= intmax ->
+                           exists m'. S.mem m' interps' /\ extended m.fm_int m'.fm_int r i }
+               invariant { forall m':interp. S.mem m' interps' ->
+                        intmin <= m'.i r <= intmax /\
+                        exists m. S.mem m iter.iter_fset_done /\ extended m.fm_int m'.fm_int r (m'.i r) }
+               let m = (next_iter_fset iter) in
+               let ref j = intmin in
+               let ghost ref interps'' = S.empty in
+               while j <= intmax do
+                 variant { intmax - j }
+                 invariant { intmin <= j <= intmax + 1 }
+                 invariant { forall i. intmin <= i < j ->
+                             exists m'. S.mem m' interps'' /\ extended m.fm_int m'.fm_int r i }
+                 invariant { forall m':interp. S.mem m' interps'' ->
+                          intmin <= m'.i r < j /\
+                          exists m. S.mem m iter.iter_fset_done /\ extended m.fm_int m'.fm_int r (m'.i r) }
+                 let m_modi = Var.Hi.copy_unlock m.model.Type.modi in
+                 Var.Hi.set m_modi r j;
+                 let m = mk_interp
+                     {
+                      Type.modi = Var.Hi.copy_lock m_modi;
+                      Type.modb = m.model.Type.modb
+                 } in
+                 interps'' <- S.add m interps'';
+                 j <- j+1;
+               done;
+               interps' <- S.union interps' interps'';
+             done;
+          in
+          c.interps <- interps';
+          r
+
+       let partial create_bool_var (c:interp_set) : bool_var
+           ensures { not (S.mem result (old c.bool_vars)) }
+           ensures { c.bool_vars = S.add result (old c.bool_vars) }
+
+           ensures { forall m:interp. (old mem m c) -> forall i.
+                        exists m'. mem m' c /\ extended m.fm_bool m'.fm_bool result i }
+           ensures { forall m':interp. (mem m' c) ->
+                        exists m. (old mem m c) /\ extended m.fm_bool m'.fm_bool result (m'.b result) }
+         =
+          c.nextb <- Peano.succ c.nextb;
+          let r = { Var.vb = PeanoInt63.to_int63 c.nextb - 1 } in
+          let _ = PeanoInt63.to_int63 c.nextb in
+          c.bool_vars <- S.add r c.bool_vars;
+          r
+
+       (** We keep only from the set of interpretation the interpetation where [r] is true *)
+       val is_true (c:interp_set) (r:bool_var) : unit
+           requires { S.mem r c.bool_vars }
+           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r) ) }
+
+       (** Remove from the set of interpretation the interpetation where [r1] and [r2] are not opposite *)
+       val not_ (c:interp_set) (r1:bool_var) (r2:bool_var) : unit
+           requires { S.mem r1 c.bool_vars }
+           requires { S.mem r2 c.bool_vars }
+           ensures { forall m. mem m c <-> ((old mem m c) /\ notb (m.b r1) = m.b r2 ) }
+
+       (** Remove from the set of interpretation the interpetation where we don't have r = (v = iv) *)
+       val is_cst_reif (c:interp_set) (v:int_var) (iv:int) (r:bool_var) : unit
+           requires { S.mem v c.int_vars }
+           requires { S.mem r c.bool_vars }
+           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r <-> m.i v = iv) ) }
+           writes { c }
+
+       val add_reif (c:interp_set) (v1:int_var) (v2:int_var) (v3:int_var) (r:bool_var) : unit
+           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r <-> m.i v1 + m.i v2 = m.i v3) ) }
+           writes { c }
+
+       (** Remove from the set of interpretation the interpetation where [r1] and [r2] are not opposite *)
+       val le_reif (c:interp_set) (v1:int_var) (cst:int) (v2:int_var) (r:bool_var) : unit
+           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r <-> m.i v1 <= cst + m.i v2) ) }
+           writes { c }
+
+       exception Unsat
+
+       (** Create a model that belongs to the set of interpretation, if one exists. Otherwise raise Unsat *)
+       val partial solve (c:interp_set) : interp
+           (** The model is mem *)
+           ensures { mem result c }
+           raises { Unsat -> forall m. not (mem m c) } (** is_empty c *)
+
+       (** Create a model that belongs to the set of interpretation, if one exists. Otherwise raise Unsat *)
+       val partial solve_all (c:interp_set) : list interp
+           (** The model is mem *)
+           ensures { forall m. mem m c -> ListMem.mem m result }
+           raises { Unsat -> forall m. not (mem m c) } (** is_empty c *)
+
+       val get_int (m:interp) (v:int_var) : int
+           requires { S.mem v m.fm_int.defined }
+           ensures { result = m.i v }
+
+       val get_bool (m:interp) (v:bool_var) : bool
+           requires { S.mem v m.fm_bool.defined }
+           ensures { result = m.b v }
+(*
+       lemma true_is_true: forall c:context. forall m. is_true_in m c -> m.b true_
+
+       let is_cst_reif (c:context) (v:ti) (iv:int) (r:tb)
+           requires { S.mem v c.int_vars }
+           requires { S.mem r c.bool_vars }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v = iv) ) }
+       =
+       c.prob <- Cons ((Constraint.Cst {
+              ConstraintCst.v = v;
+              ConstraintCst.i = iv;
+              ConstraintCst.b = r })) c.prob
+
+       let is_cst (c:context) (v:ti) (iv:int)
+           requires { S.mem v c.int_vars }
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v = iv ) }
+       =
+        is_cst_reif c v iv true_
+
+       let add_reif (c:context) (v1:ti) (v2:ti) (v3:ti) (r:tb)
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v1 + m.i v2 = m.i v3) ) }
+       =
+       c.prob <- Cons ((Constraint.Add {
+              ConstraintAdd.v1 = v1;
+              ConstraintAdd.v2 = v2;
+              ConstraintAdd.v3 = v3;
+              ConstraintAdd.b = r })) c.prob
+
+       let add (c:context) (v1:ti) (v2:ti) (v3:ti)
+           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v1 + m.i v2 = m.i v3 ) }
+       =
+        add_reif c v1 v2 v3 true_
+
+       type model = Type.model int bool
+
+       function is_defined_ti (m:model) (v:ti) : bool =
+           S.mem v (Type.defined_model m).Var.si
+       function is_defined_tb (m:model) (v:tb) : bool =
+           S.mem v (Type.defined_model m).Var.sb
+
+       function interp_of_model (m:model) : interp = All.Engine.interp_of_model m
+
+       let solve' (c:context) : model
+           ensures { is_true_in (interp_of_model result) c }
+           ensures { forall v. S.mem v c.int_vars <-> is_defined_ti result v }
+           ensures { forall v. S.mem v c.bool_vars <-> is_defined_tb result v }
+           raises { Type.Unsat -> forall m. not (is_true_in m c) }
+           writes { } =
+           All.start' c.prob c.intmin c.intmax
+
+
+       let solve (c:context) : model
+           ensures { is_true_in (interp_of_model result) c }
+           ensures { forall v. S.mem v c.int_vars <-> is_defined_ti result v }
+           ensures { forall v. S.mem v c.bool_vars <-> is_defined_tb result v }
+           raises { Type.Unsat -> forall m. not (is_true_in m c) }
+           writes { } =
+           let _ = solve' c in absurd; raise Type.Unsat
+
+       let get_int (m:model) (v:ti) : int
+           requires { is_defined_ti m v }
+           ensures { result = (interp_of_model m).i v } =
+           Type.get_mod_int m v
+*)
+
+(*
+        clone APIIntf with
+              type ti = ti,
+              type tb = tb,
+              type interp = interp,
+              val mk_interp = mk_interp,
+              function i = i,
+              function b = b,
+              type context = context,
+              val true_ = true_,
+              predicate is_true_in = is_true_in,
+              val create_vari = create_vari,
+              val create_varb = create_varb,
+              val create_context = create_context,
+              val is_cst_reif = is_cst_reif,
+              val is_cst = is_cst,
+              val add_reif = add_reif,
+              val add = add,
+              lemma true_is_true,
+              exception Unsat = Type.Unsat,
+              type model = model,
+              function is_defined_ti = is_defined_ti,
+              function is_defined_tb = is_defined_tb,
+              function interp_of_model = interp_of_model,
+              val solve = solve,
+              val get_int = get_int
+*)
+end
+
+*)
diff --git a/src/lib/colibrics.ml b/src/lib/colibrics.ml
index de4866072d105a823113bb3b2c01e644aa696fbd..a963a274ff4031451d6e96f1c53db70db5022f0b 100644
--- a/src/lib/colibrics.ml
+++ b/src/lib/colibrics.ml
@@ -10,42 +10,42 @@
 (**************************************************************************)
 
 exception Unsat = Cp__Type.Unsat
-exception UnknownVariable = Cp__APIDefensive.UnknownVariable
+exception UnknownVariable = All__APIDefensive.UnknownVariable
 
 module Model = struct
-  type t = Cp__APIDefensive.model
+  type t = All__APIDefensive.model
 end
 
 module Context = struct
-  type t = Cp__APIDefensive.context
-  let create = Cp__APIDefensive.create_context
-  let solve = Cp__APIDefensive.solve
+  type t = All__APIDefensive.context
+  let create = All__APIDefensive.create_context
+  let solve = All__APIDefensive.solve
 end
 
 module Var = struct
    module I = struct
-     type t = Cp__APIDefensive.ti
-     let mk ~min ~max c = Cp__APIDefensive.create_vari c min max
-     let get m i = Cp__APIDefensive.get_model_i m i
-     let zero = Cp__APIDefensive.zero_
+     type t = All__APIDefensive.ti
+     let mk ~min ~max c = All__APIDefensive.create_vari c min max
+     let get m i = All__APIDefensive.get_model_i m i
+     let zero = All__APIDefensive.zero_
    end
    module B = struct
-     type t = Cp__APIDefensive.tb
-     let mk c = Cp__APIDefensive.create_varb c
-     let get m i = Cp__APIDefensive.get_model_b m i
-     let true_ = Cp__APIDefensive.true_
+     type t = All__APIDefensive.tb
+     let mk c = All__APIDefensive.create_varb c
+     let get m i = All__APIDefensive.get_model_b m i
+     let true_ = All__APIDefensive.true_
    end
 end
 
 module Constraint = struct
-  let is_cst_reif = Cp__APIDefensive.is_cst_reif
-  let is_cst = Cp__APIDefensive.is_cst
-  let add_reif = Cp__APIDefensive.add_reif
-  let add = Cp__APIDefensive.add
-  let le_reif = Cp__APIDefensive.le_reif
-  let le = Cp__APIDefensive.le
-  let or_ = Cp__APIDefensive.or1
-  let not_ = Cp__APIDefensive.not_
-  let is_true = Cp__APIDefensive.is_true
-  let equiv = Cp__APIDefensive.equiv
+  let is_cst_reif = All__APIDefensive.is_cst_reif
+  let is_cst = All__APIDefensive.is_cst
+  let add_reif = All__APIDefensive.add_reif
+  let add = All__APIDefensive.add
+  let le_reif = All__APIDefensive.le_reif
+  let le = All__APIDefensive.le
+  let or_ = All__APIDefensive.or1
+  let not_ = All__APIDefensive.not_
+  let is_true = All__APIDefensive.is_true
+  let equiv = All__APIDefensive.equiv
 end
diff --git a/src/lib/constraints/simple.mlw b/src/lib/constraints/simple.mlw
new file mode 100644
index 0000000000000000000000000000000000000000..b357d53ee0ee875a8669b056ffe1980b25371791
--- /dev/null
+++ b/src/lib/constraints/simple.mlw
@@ -0,0 +1,135 @@
+module Simple
+
+   use cp.Type
+   use cp.Var as Var
+   use mach.int.Int
+   use Bool
+   use set.Fset as S
+   use cp.DomI
+   use cp.DomB
+   use seq.Seq as Seq
+   use cp.Int63 as Int63
+
+   use export cp.ConstraintHelpers
+   use cp.ConstraintCst as ConstraintCst
+   use cp.ConstraintIsTrue as ConstraintIsTrue
+   use cp.ConstraintAdd as ConstraintAdd
+   use cp.ConstraintLe as ConstraintLe
+   use cp.ConstraintOr as ConstraintOr
+   use cp.ConstraintEquiv as ConstraintEquiv
+   use cp.ConstraintNot as ConstraintNot
+   use cp.ConstraintBoolPresent as ConstraintBoolPresent
+
+   type t =
+   | Cst ConstraintCst.t
+   | Add ConstraintAdd.t
+   | Le ConstraintLe.t
+   | Or  ConstraintOr.t
+   | Equiv  ConstraintEquiv.t
+   | IsTrue ConstraintIsTrue.t
+   | Not ConstraintNot.t
+   | BoolPresent ConstraintBoolPresent.t
+
+   function constraint_is_true_in (m:interp) (c:t) : bool =
+     match c with
+     | Cst c -> ConstraintCst.constraint_is_true_in m c
+     | IsTrue c -> ConstraintIsTrue.constraint_is_true_in m c
+     | Not c -> ConstraintNot.constraint_is_true_in m c
+     | Add c -> ConstraintAdd.constraint_is_true_in m c
+     | Le c -> ConstraintLe.constraint_is_true_in m c
+     | Or c -> ConstraintOr.constraint_is_true_in m c
+     | Equiv c -> ConstraintEquiv.constraint_is_true_in m c
+     | BoolPresent c -> ConstraintBoolPresent.constraint_is_true_in m c
+     end
+
+   let ghost function vars (c:t) : Var.vars =
+     match c with
+     | Cst c -> ConstraintCst.vars c
+     | IsTrue c -> ConstraintIsTrue.vars c
+     | Not c -> ConstraintNot.vars c
+     | Add c -> ConstraintAdd.vars c
+     | Le c -> ConstraintLe.vars c
+     | Or c -> ConstraintOr.vars c
+     | Equiv c -> ConstraintEquiv.vars c
+     | BoolPresent c -> ConstraintBoolPresent.vars c
+     end
+
+   let compute_vars_ti (c:t) (si:Var.Si.t) : unit
+       ensures { S.(==) si.Var.Si.elts (S.union (old si.Var.Si.elts) (vars c).Var.si) }
+       writes { si } =
+       match c with
+       | Cst c -> ConstraintCst.compute_vars_ti c si
+       | IsTrue c -> ConstraintIsTrue.compute_vars_ti c si
+       | Not c -> ConstraintNot.compute_vars_ti c si
+       | Add c -> ConstraintAdd.compute_vars_ti c si
+       | Le c -> ConstraintLe.compute_vars_ti c si
+       | Or c -> ConstraintOr.compute_vars_ti c si
+       | Equiv c -> ConstraintEquiv.compute_vars_ti c si
+       | BoolPresent c -> ConstraintBoolPresent.compute_vars_ti c si
+      end
+
+
+   let compute_vars_tb (c:t) (sb:Var.Sb.t) : unit
+       ensures { S.(==) sb.Var.Sb.elts (S.union (old sb.Var.Sb.elts) (vars c).Var.sb) }
+       writes { sb } =
+       match c with
+       | Cst c -> ConstraintCst.compute_vars_tb c sb
+       | IsTrue c -> ConstraintIsTrue.compute_vars_tb c sb
+       | Not c -> ConstraintNot.compute_vars_tb c sb
+       | Add c -> ConstraintAdd.compute_vars_tb c sb
+       | Le c -> ConstraintLe.compute_vars_tb c sb
+       | Or c -> ConstraintOr.compute_vars_tb c sb
+       | Equiv c -> ConstraintEquiv.compute_vars_tb c sb
+       | BoolPresent c -> ConstraintBoolPresent.compute_vars_tb c sb
+      end
+
+   let propagate (e:env) (c:t) : unit
+       requires { Var.subset (vars c) (defined e) }
+       ensures { forall m:interp.
+                    old (is_true_in m e) ->
+                    constraint_is_true_in m c ->
+                    is_true_in m e
+               }
+       ensures { forall m:interp. is_true_in m e -> old (is_true_in m e) }
+       (* ensures { Var.equal_set (defined (old e)) (defined e) } *)
+       ensures { not (old e.dirty) -> e.dirty -> size e < size (old e) }
+       ensures { 0 <= size e <= size (old e) }
+       raises { Unsat -> forall m:interp. old (is_true_in m e) -> not (constraint_is_true_in m c) }
+       writes { e.domi.Var.Hbi.contents,
+                e.domb.Var.Hbb.contents,
+                e.dirty
+              }
+     =
+      match c with
+      | Cst c -> ConstraintCst.propagate e c
+      | IsTrue c -> ConstraintIsTrue.propagate e c
+      | Not c -> ConstraintNot.propagate e c
+      | Add c -> ConstraintAdd.propagate e c
+      | Le c -> ConstraintLe.propagate e c
+      | Or c -> ConstraintOr.propagate e c
+      | Equiv c -> ConstraintEquiv.propagate e c
+      | BoolPresent c -> ConstraintBoolPresent.propagate e c
+      end
+
+
+
+   let check_model (mo:model) (c:t) : bool
+       requires { Var.subset (vars c) (defined_model mo) }
+       ensures {
+        if result
+        then forall m:interp. is_model_of m mo -> constraint_is_true_in m c
+        else forall m:interp. is_model_of m mo -> not (constraint_is_true_in m c)
+       }
+       =
+     match c with
+      | Cst c -> ConstraintCst.check_model mo c
+      | IsTrue c -> ConstraintIsTrue.check_model mo c
+      | Not c -> ConstraintNot.check_model mo c
+      | Add c -> ConstraintAdd.check_model mo c
+      | Le c -> ConstraintLe.check_model mo c
+      | Or c -> ConstraintOr.check_model mo c
+      | Equiv c -> ConstraintEquiv.check_model mo c
+      | BoolPresent c -> ConstraintBoolPresent.check_model mo c
+      end
+
+end
diff --git a/src/lib/cp.mlw b/src/lib/cp.mlw
index 627eb3eb3d276d099580b0074769e821dd76f33d..18223145b0945f0a94ac062dcc1205b959abb5e5 100644
--- a/src/lib/cp.mlw
+++ b/src/lib/cp.mlw
@@ -2416,1193 +2416,3 @@ module ConstraintBoolPresent
          = true
 
 end
-
-module ConstraintSimple
-
-     use Type
-     use Var as Var
-     use mach.int.Int
-     use Bool
-     use set.Fset as S
-     use DomI
-     use DomB
-     use seq.Seq as Seq
-     use Int63 as Int63
-
-     use export ConstraintHelpers
-     use ConstraintCst as ConstraintCst
-     use ConstraintIsTrue as ConstraintIsTrue
-     use ConstraintAdd as ConstraintAdd
-     use ConstraintLe as ConstraintLe
-     use ConstraintOr as ConstraintOr
-     use ConstraintEquiv as ConstraintEquiv
-     use ConstraintNot as ConstraintNot
-     use ConstraintBoolPresent as ConstraintBoolPresent
-
-     type t =
-     | Cst ConstraintCst.t
-     | Add ConstraintAdd.t
-     | Le ConstraintLe.t
-     | Or  ConstraintOr.t
-     | Equiv  ConstraintEquiv.t
-     | IsTrue ConstraintIsTrue.t
-     | Not ConstraintNot.t
-     | BoolPresent ConstraintBoolPresent.t
-
-     function constraint_is_true_in (m:interp) (c:t) : bool =
-       match c with
-       | Cst c -> ConstraintCst.constraint_is_true_in m c
-       | IsTrue c -> ConstraintIsTrue.constraint_is_true_in m c
-       | Not c -> ConstraintNot.constraint_is_true_in m c
-       | Add c -> ConstraintAdd.constraint_is_true_in m c
-       | Le c -> ConstraintLe.constraint_is_true_in m c
-       | Or c -> ConstraintOr.constraint_is_true_in m c
-       | Equiv c -> ConstraintEquiv.constraint_is_true_in m c
-       | BoolPresent c -> ConstraintBoolPresent.constraint_is_true_in m c
-       end
-
-     let ghost function vars (c:t) : Var.vars =
-       match c with
-       | Cst c -> ConstraintCst.vars c
-       | IsTrue c -> ConstraintIsTrue.vars c
-       | Not c -> ConstraintNot.vars c
-       | Add c -> ConstraintAdd.vars c
-       | Le c -> ConstraintLe.vars c
-       | Or c -> ConstraintOr.vars c
-       | Equiv c -> ConstraintEquiv.vars c
-       | BoolPresent c -> ConstraintBoolPresent.vars c
-       end
-
-     let compute_vars_ti (c:t) (si:Var.Si.t) : unit
-         ensures { S.(==) si.Var.Si.elts (S.union (old si.Var.Si.elts) (vars c).Var.si) }
-         writes { si } =
-         match c with
-         | Cst c -> ConstraintCst.compute_vars_ti c si
-         | IsTrue c -> ConstraintIsTrue.compute_vars_ti c si
-         | Not c -> ConstraintNot.compute_vars_ti c si
-         | Add c -> ConstraintAdd.compute_vars_ti c si
-         | Le c -> ConstraintLe.compute_vars_ti c si
-         | Or c -> ConstraintOr.compute_vars_ti c si
-         | Equiv c -> ConstraintEquiv.compute_vars_ti c si
-         | BoolPresent c -> ConstraintBoolPresent.compute_vars_ti c si
-        end
-
-
-     let compute_vars_tb (c:t) (sb:Var.Sb.t) : unit
-         ensures { S.(==) sb.Var.Sb.elts (S.union (old sb.Var.Sb.elts) (vars c).Var.sb) }
-         writes { sb } =
-         match c with
-         | Cst c -> ConstraintCst.compute_vars_tb c sb
-         | IsTrue c -> ConstraintIsTrue.compute_vars_tb c sb
-         | Not c -> ConstraintNot.compute_vars_tb c sb
-         | Add c -> ConstraintAdd.compute_vars_tb c sb
-         | Le c -> ConstraintLe.compute_vars_tb c sb
-         | Or c -> ConstraintOr.compute_vars_tb c sb
-         | Equiv c -> ConstraintEquiv.compute_vars_tb c sb
-         | BoolPresent c -> ConstraintBoolPresent.compute_vars_tb c sb
-        end
-
-     let propagate (e:env) (c:t) : unit
-         requires { Var.subset (vars c) (defined e) }
-         ensures { forall m:interp.
-                      old (is_true_in m e) ->
-                      constraint_is_true_in m c ->
-                      is_true_in m e
-                 }
-         ensures { forall m:interp. is_true_in m e -> old (is_true_in m e) }
-         (* ensures { Var.equal_set (defined (old e)) (defined e) } *)
-         ensures { not (old e.dirty) -> e.dirty -> size e < size (old e) }
-         ensures { 0 <= size e <= size (old e) }
-         raises { Unsat -> forall m:interp. old (is_true_in m e) -> not (constraint_is_true_in m c) }
-         writes { e.domi.Var.Hbi.contents,
-                  e.domb.Var.Hbb.contents,
-                  e.dirty
-                }
-       =
-        match c with
-        | Cst c -> ConstraintCst.propagate e c
-        | IsTrue c -> ConstraintIsTrue.propagate e c
-        | Not c -> ConstraintNot.propagate e c
-        | Add c -> ConstraintAdd.propagate e c
-        | Le c -> ConstraintLe.propagate e c
-        | Or c -> ConstraintOr.propagate e c
-        | Equiv c -> ConstraintEquiv.propagate e c
-        | BoolPresent c -> ConstraintBoolPresent.propagate e c
-        end
-
-
-
-     let check_model (mo:model) (c:t) : bool
-         requires { Var.subset (vars c) (defined_model mo) }
-         ensures {
-          if result
-          then forall m:interp. is_model_of m mo -> constraint_is_true_in m c
-          else forall m:interp. is_model_of m mo -> not (constraint_is_true_in m c)
-         }
-         =
-       match c with
-        | Cst c -> ConstraintCst.check_model mo c
-        | IsTrue c -> ConstraintIsTrue.check_model mo c
-        | Not c -> ConstraintNot.check_model mo c
-        | Add c -> ConstraintAdd.check_model mo c
-        | Le c -> ConstraintLe.check_model mo c
-        | Or c -> ConstraintOr.check_model mo c
-        | Equiv c -> ConstraintEquiv.check_model mo c
-        | BoolPresent c -> ConstraintBoolPresent.check_model mo c
-        end
-
-end
-
-module All
-
-   use DomI as Dom2I
-   use DomB as Dom2B
-   use ConstraintSimple as Constraint2
-
-   clone Engine with
-
-         type DomI.t = Dom2I.t,
-         type DomI.value = Dom2I.value,
-         predicate DomI.is_true_in = Dom2I.is_true_in,
-         predicate DomI.is_singleton = Dom2I.is_singleton,
-         val DomI.get_singleton = Dom2I.get_singleton,
-         val DomI.is_singleton = Dom2I.is_singleton,
-         val DomI.mk_singleton = Dom2I.mk_singleton,
-         val DomI.default_value = Dom2I.default_value,
-         function DomI.size = Dom2I.size,
-
-         type DomB.t = Dom2B.t,
-         type DomB.value = Dom2B.value,
-         predicate DomB.is_true_in = Dom2B.is_true_in,
-         predicate DomB.is_singleton = Dom2B.is_singleton,
-         val DomB.get_singleton = Dom2B.get_singleton,
-         val DomB.is_singleton = Dom2B.is_singleton,
-         val DomB.mk_singleton = Dom2B.mk_singleton,
-         val DomB.default_value = Dom2B.default_value,
-         function DomB.size = Dom2B.size,
-
-         type Constraint.t = Constraint2.t,
-         function Constraint.is_true_in = Constraint2.constraint_is_true_in,
-         function Constraint.vars = Constraint2.vars,
-         val propagate = Constraint2.propagate,
-         val check_model = Constraint2.check_model,
-         function size = Constraint2.size,
-         val Constraint.compute_vars_ti = Constraint2.compute_vars_ti,
-         val Constraint.compute_vars_tb = Constraint2.compute_vars_tb
-
-
-   use list.List
-   use Type
-   use mach.int.Int
-
-   let start' (p:Prob.t) (minint:int) (maxint:int) : (model int bool)
-         ensures { forall v. S.mem v (defined_model result).Var.si -> minint <= get_mod_int result v <= maxint }
-         ensures { forall m:(interp int bool). is_model_of m result -> Prob.is_true_in m p }
-         raises { Unsat -> forall m:(interp int bool). (forall v. S.mem v (Prob.vars p).Var.si -> minint <= m.i v <= maxint) -> not (Prob.is_true_in m p) }
-         ensures { Var.equal_set (Prob.vars p) (defined_model result) }
-       =
-       let topbool = Dom2B.Top in
-       let topint = {Dom2I.min=minint; Dom2I.max=maxint} in
-       start p topbool topint
-
-end
-
-module API
-
-       use mach.int.Int
-       use bool.Bool
-       use list.List
-       use list.Mem as ListMem
-       use Var as Var
-       use mach.int.Int63
-       use mach.peano.Peano as Peano
-       use mach.peano.Int63 as PeanoInt63
-       use ConstraintSimple as Constraint
-       use ConstraintCst as ConstraintCst
-       use ConstraintIsTrue as ConstraintIsTrue
-       use ConstraintAdd as ConstraintAdd
-       use ConstraintOr as ConstraintOr
-       use ConstraintEquiv as ConstraintEquiv
-       use ConstraintNot as ConstraintNot
-       use ConstraintLe as ConstraintLe
-       use ConstraintBoolPresent as ConstraintBoolPresent
-       use All
-       use set.Fset as S
-       use Type as Type
-       use int.Int
-       use int.MinMax
-
-       type ti = Var.ti
-       type tb = Var.tb
-
-
-       type interp = Type.interp int bool
-
-       function i (m:interp) : ti -> int = m.Type.i
-
-       function b (m:interp) : tb -> bool = m.Type.b
-
-       let function true_ : tb = { Var.vb = 1 }
-       let function zero_ : ti = { Var.vi = 1 }
-
-       type context = {
-            mutable intmin : int;
-            mutable intmax : int;
-            mutable ghost sti: S.fset ti;
-            mutable nexti: Peano.t;
-            mutable ghost stb: S.fset tb;
-            mutable nextb: Peano.t;
-            mutable prob: list Constraint.t;
-       }
-       invariant { forall v. S.mem v sti <-> 1 <= v.Var.vi < nexti }
-       invariant { forall v. S.mem v stb <-> 1 <= v.Var.vb < nextb }
-       invariant { S.mem true_ stb }
-       invariant { S.mem zero_ sti }
-       invariant { 2 <= nexti }
-       invariant { 2 <= nextb }
-       invariant { forall m. All.Engine.Prob.is_true_in m prob -> m.Type.b true_ }
-       invariant { forall m. All.Engine.Prob.is_true_in m prob -> m.Type.i zero_ = 0 }
-       invariant { forall m. All.Engine.Prob.is_true_in m prob ->
-                                       forall vi. S.mem vi sti ->
-                                                 intmin <= m.Type.i vi <= intmax }
-       invariant { (S.(==) (All.Engine.Prob.vars prob).Var.si sti) } 
-       invariant { (S.(==) (All.Engine.Prob.vars prob).Var.sb stb) } 
-       by {
-        intmin = 0;
-        intmax = 0;
-        sti = S.add zero_ S.empty;
-        stb = S.add true_ S.empty;
-        nexti = Peano.succ Peano.one;
-        nextb = Peano.succ Peano.one;
-        prob =
-             Cons (Constraint.Cst { ConstraintCst.v = zero_; ConstraintCst.i = 0; ConstraintCst.b = true_ })
-             (Cons (Constraint.IsTrue { ConstraintIsTrue.b = true_ })
-              Nil);
-       }
-
-       predicate is_true_in (m:interp) (c:context) =
-            All.Engine.Prob.is_true_in m c.prob
-
-       let create_vari (c:context) (min_:int) (max_:int) : ti
-           ensures { not (S.mem result (old c.sti)) }
-           ensures { c.sti = S.add result (old c.sti) }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ min_ <= m.i result <= max_ ) }
-         =
-          c.nexti <- Peano.succ c.nexti;
-          let r = { Var.vi = PeanoInt63.to_int63 c.nexti - 1 } in
-          c.sti <- S.add r c.sti;
-          c.intmin <- min c.intmin min_;
-          c.intmax <- max c.intmax max_;
-          let ctr1 = { ConstraintLe.v1 = r; ConstraintLe.v2 = zero_;
-                                   ConstraintLe.i = max_; ConstraintLe.b = true_ } in
-          let ctr2 = { ConstraintLe.v1 = zero_; ConstraintLe.v2 = r;
-                                  ConstraintLe.i = - min_; ConstraintLe.b = true_ } in
-          c.prob <- Cons (Constraint.Le ctr1) (Cons (Constraint.Le ctr2) c.prob);
-          assert { ListMem.mem (Constraint.Le ctr1) c.prob };
-          assert { ListMem.mem (Constraint.Le ctr2) c.prob };
-          assert { forall ctr. ListMem.mem ctr (old c.prob) -> ListMem.mem ctr c.prob };
-          assert { forall m. All.Engine.Prob.is_true_in m c.prob -> ConstraintLe.constraint_is_true_in m ctr1 };
-          assert { forall m. All.Engine.Prob.is_true_in m c.prob -> ConstraintLe.constraint_is_true_in m ctr2 };
-          assert { forall v. S.mem v (All.Engine.Prob.vars c.prob).Var.si -> (v = r \/ v = zero_ \/ old (S.mem v (All.Engine.Prob.vars c.prob).Var.si)) };
-          r
-
-       let create_varb (c:context) : tb
-           ensures { not (S.mem result (old c.stb)) }
-           ensures { c.stb = S.add result (old c.stb) }
-           ensures { result.Var.vb <> true_.Var.vb }
-         =
-          if PeanoInt63.to_int63 c.nextb = true_.Var.vb then c.nextb <- Peano.succ c.nextb;
-          c.nextb <- Peano.succ c.nextb;
-          let r = { Var.vb = PeanoInt63.to_int63 c.nextb - 1 } in
-          let _ = PeanoInt63.to_int63 c.nextb in
-          c.stb <- S.add r c.stb;
-          c.prob <- Cons (Constraint.BoolPresent { ConstraintBoolPresent.b1 = r }) c.prob;
-          r
-
-       let create_context ()
-           ensures { forall m. is_true_in m result <-> (m.b true_ /\ m.i zero_ = 0) }
-       =
-         let c = {
-           intmin = 0;
-           intmax = 0;
-           sti = S.add zero_ S.empty;
-           nexti = Peano.succ Peano.one;
-           stb = S.add true_ S.empty;
-           nextb = Peano.succ Peano.one;
-           prob =
-             Cons (Constraint.Cst { ConstraintCst.v = zero_; ConstraintCst.i = 0; ConstraintCst.b = true_ })
-             (Cons (Constraint.IsTrue { ConstraintIsTrue.b = true_ })
-              Nil);
-         } in
-         c
-
-       lemma true_is_true: forall c:context. forall m. is_true_in m c -> m.b true_
-       lemma zero_is_zero: forall c:context. forall m. is_true_in m c -> m.i zero_ = 0
-
-       let is_cst_reif (c:context) (v:ti) (iv:int) (r:tb)
-           requires { S.mem v c.sti }
-           requires { S.mem r c.stb }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v = iv) ) }
-       =
-       c.prob <- Cons ((Constraint.Cst {
-              ConstraintCst.v = v;
-              ConstraintCst.i = iv;
-              ConstraintCst.b = r })) c.prob
-
-       let is_cst (c:context) (v:ti) (iv:int)
-           requires { S.mem v c.sti }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v = iv ) }
-       =
-        is_cst_reif c v iv true_
-
-       let add_reif (c:context) (v1:ti) (v2:ti) (v3:ti) (r:tb)
-           requires { S.mem v1 c.sti }
-           requires { S.mem v2 c.sti }
-           requires { S.mem v3 c.sti }
-           requires { S.mem r c.stb }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v1 + m.i v2 = m.i v3) ) }
-       =
-       c.prob <- Cons ((Constraint.Add {
-              ConstraintAdd.v1 = v1;
-              ConstraintAdd.v2 = v2;
-              ConstraintAdd.v3 = v3;
-              ConstraintAdd.b = r })) c.prob
-
-       let add (c:context) (v1:ti) (v2:ti) (v3:ti)
-           requires { S.mem v1 c.sti }
-           requires { S.mem v2 c.sti }
-           requires { S.mem v3 c.sti }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v1 + m.i v2 = m.i v3 ) }
-       =
-        add_reif c v1 v2 v3 true_
-
-       let le_reif (c:context) (v1:ti) (v2:ti) (cst:int) (r:tb)
-           requires { S.mem v1 c.sti }
-           requires { S.mem v2 c.sti }
-           requires { S.mem r c.stb }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v1 <= m.i v2 + cst) ) }
-       =
-       c.prob <- Cons ((Constraint.Le {
-              ConstraintLe.v1 = v1;
-              ConstraintLe.v2 = v2;
-              ConstraintLe.i = cst;
-              ConstraintLe.b = r })) c.prob
-
-       let le (c:context) (v1:ti) (v2:ti) (cst:int)
-           requires { S.mem v1 c.sti }
-           requires { S.mem v2 c.sti }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v1 <= m.i v2 + cst ) }
-       =
-        le_reif c v1 v2 cst true_
-
-
-       let or (c:context) (b1:tb) (b2:tb) (b3:tb)
-           requires { S.mem b1 c.stb }
-           requires { S.mem b2 c.stb }
-           requires { S.mem b3 c.stb }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b b3 <-> (m.b b1) \/ (m.b b2))) }
-       =
-       c.prob <- Cons ((Constraint.Or {
-              ConstraintOr.b1 = b1;
-              ConstraintOr.b2 = b2;
-              ConstraintOr.b3 = b3;
-              })) c.prob
-
-       let equiv (c:context) (b1:tb) (b2:tb) (b3:tb)
-           requires { S.mem b1 c.stb }
-           requires { S.mem b2 c.stb }
-           requires { S.mem b3 c.stb }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b b3 <-> ((m.b b1) <-> (m.b b2)))) }
-       =
-       c.prob <- Cons ((Constraint.Equiv {
-              ConstraintEquiv.b1 = b1;
-              ConstraintEquiv.b2 = b2;
-              ConstraintEquiv.b3 = b3;
-              })) c.prob
-
-       let not_ (c:context) (b1:tb) (b2:tb)
-           requires { S.mem b1 c.stb }
-           requires { S.mem b2 c.stb }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b b2 <-> not (m.b b1))) }
-       =
-       c.prob <- Cons ((Constraint.Not {
-              ConstraintNot.b1 = b1;
-              ConstraintNot.b2 = b2;
-              })) c.prob
-
-       let is_true (c:context) (b1:tb)
-           requires { S.mem b1 c.stb }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.b b1) }
-       =
-       c.prob <- Cons (Constraint.IsTrue { ConstraintIsTrue.b = b1 })
-                 c.prob
-
-
-      let solve (c:context) : Type.model int bool
-          ensures { is_true_in (All.Engine.interp_of_model result) c }
-          ensures { Var.equal_set (All.Engine.Prob.vars c.prob) (Type.defined_model result) }
-          raises { Type.Unsat -> forall m. not (is_true_in m c) } =
-          All.start' c.prob c.intmin c.intmax
-
-end
-
-module APIDefensive
-
-       use mach.int.Int
-       use bool.Bool
-       use list.List
-       use list.Mem as ListMem
-       use Var as Var
-       use mach.int.Int63
-       use mach.peano.Peano as Peano
-       use mach.peano.Int63 as PeanoInt63
-       use ConstraintSimple as Constraint
-       use ConstraintCst as ConstraintCst
-       use ConstraintIsTrue as ConstraintIsTrue
-       use ConstraintAdd as ConstraintAdd
-       use ConstraintOr as ConstraintOr
-       use ConstraintNot as ConstraintNot
-       use ConstraintLe as ConstraintLe
-       use All
-       use set.Fset as S
-       use Type as Type
-       use int.Int
-       use int.MinMax
-       use import API as API
-
-       type ti = Var.ti
-       type tb = Var.tb
-
-
-       type interp = Type.interp int bool
-
-       function i (m:interp) : ti -> int = m.Type.i
-
-       function b (m:interp) : tb -> bool = m.Type.b
-
-       let function true_ : tb = API.true_
-       let function zero_ : ti = API.zero_
-
-       type context = API.context
-       predicate is_true_in (m:interp) (c:context) = API.is_true_in m c
-
-       let create_vari (c:context) (min_:int) (max_:int) : ti
-           ensures { not (S.mem result (old c.sti)) }
-           ensures { c.sti = S.add result (old c.sti) }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ min_ <= m.i result <= max_ ) }
-         =
-          API.create_vari c min_ max_
-
-       let create_varb (c:context) : tb
-           ensures { not (S.mem result (old c.stb)) }
-           ensures { c.stb = S.add result (old c.stb) }
-           ensures { result.Var.vb <> true_.Var.vb }
-         =
-          API.create_varb c
-
-       let create_context ()
-           ensures { forall m. is_true_in m result <-> (m.b true_ /\ m.i zero_ = 0) }
-       =
-        API.create_context ()
-
-       lemma true_is_true: forall c:context. forall m. is_true_in m c -> m.b true_
-       lemma zero_is_zero: forall c:context. forall m. is_true_in m c -> m.i zero_ = 0
-
-       exception UnknownVariable
-
-       let check_ti (c:context) (v:ti) : unit
-           raises { UnknownVariable -> not (S.mem v c.sti) }
-           ensures { S.mem v c.sti } =
-            if 1 <= v.Var.vi < (PeanoInt63.to_int63 c.nexti) then ()
-            else raise UnknownVariable
-
-       let check_tb (c:context) (v:tb) : unit
-           raises { UnknownVariable -> not (S.mem v c.stb) }
-           ensures { S.mem v c.stb } =
-            if 1 <= v.Var.vb < (PeanoInt63.to_int63 c.nextb) then ()
-            else raise UnknownVariable
-
-       let is_cst_reif (c:context) (v:ti) (iv:int) (r:tb)
-           raises { UnknownVariable -> not (S.mem v c.sti) \/ not (S.mem r c.stb) }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v = iv) ) }
-       =
-        check_ti c v;
-        check_tb c r;
-        API.is_cst_reif c v iv r
-
-       let is_cst (c:context) (v:ti) (iv:int)
-           raises { UnknownVariable -> not (S.mem v c.sti) }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v = iv ) }
-       =
-        check_ti c v;
-        API.is_cst c v iv
-
-       let add_reif (c:context) (v1:ti) (v2:ti) (v3:ti) (r:tb)
-           raises { UnknownVariable -> not (S.mem v1 c.sti) \/ not (S.mem v2 c.sti) \/ not (S.mem v3 c.sti) \/ not (S.mem r c.stb) }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v1 + m.i v2 = m.i v3) ) }
-       =
-        check_ti c v1;
-        check_ti c v2;
-        check_ti c v3;
-        check_tb c r;
-        API.add_reif c v1 v2 v3 r
-
-       let add (c:context) (v1:ti) (v2:ti) (v3:ti)
-           raises { UnknownVariable -> not (S.mem v1 c.sti) \/ not (S.mem v2 c.sti) \/ not (S.mem v3 c.sti) }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v1 + m.i v2 = m.i v3 ) }
-       =
-        check_ti c v1;
-        check_ti c v2;
-        check_ti c v3;
-        API.add c v1 v2 v3
-
-       let le_reif (c:context) (v1:ti) (v2:ti) (cst:int) (r:tb)
-           raises { UnknownVariable -> not (S.mem v1 c.sti) \/ not (S.mem v2 c.sti) \/ not (S.mem r c.stb) }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v1 <= m.i v2 + cst) ) }
-       =
-        check_ti c v1;
-        check_ti c v2;
-        check_tb c r;
-        API.le_reif c v1 v2 cst r
-
-       let le (c:context) (v1:ti) (v2:ti) (cst:int)
-           raises { UnknownVariable -> not (S.mem v1 c.sti) \/ not (S.mem v2 c.sti) }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v1 <= m.i v2 + cst ) }
-       =
-        check_ti c v1;
-        check_ti c v2;
-        API.le c v1 v2 cst
-
-       let or (c:context) (b1:tb) (b2:tb) (b3:tb)
-           raises { UnknownVariable -> not (S.mem b1 c.stb) \/ not (S.mem b2 c.stb) \/ not (S.mem b3 c.stb) }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b b3 <-> (m.b b1) \/ (m.b b2))) }
-       =
-        check_tb c b1;
-        check_tb c b2;
-        check_tb c b3;
-        API.or c b1 b2 b3
-
-       let equiv (c:context) (b1:tb) (b2:tb) (b3:tb)
-           raises { UnknownVariable -> not (S.mem b1 c.stb) \/ not (S.mem b2 c.stb) \/ not (S.mem b3 c.stb) }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b b3 <-> ((m.b b1) <-> (m.b b2)))) }
-       =
-        check_tb c b1;
-        check_tb c b2;
-        check_tb c b3;
-        API.equiv c b1 b2 b3
-
-       let not_ (c:context) (b1:tb) (b2:tb)
-           raises { UnknownVariable -> not (S.mem b1 c.stb) \/ not (S.mem b2 c.stb) }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b b2 <-> not (m.b b1))) }
-       =
-        check_tb c b1;
-        check_tb c b2;
-        API.not_ c b1 b2
-
-       let is_true (c:context) (b1:tb)
-           raises { UnknownVariable -> not (S.mem b1 c.stb) }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b b1)) }
-       =
-        check_tb c b1;
-        API.is_true c b1
-
-      type model = {
-           mod : Type.model int bool;
-           lasti: int63;
-           lastb: int63;
-        }
-       invariant { forall v. 1 <= v.Var.vi <= lasti <-> S.mem v (Type.defined_model mod).Var.si  }
-       invariant { forall v. 1 <= v.Var.vb <= lastb <-> S.mem v (Type.defined_model mod).Var.sb  }
-       by { mod =
-            (let hi = Var.Hi.create (-1) (0:int) S.empty in
-             let hb = Var.Hb.create (-1) true S.empty in
-             { Type.modi = Var.Hi.copy_lock hi; Type.modb = Var.Hb.copy_lock hb });
-           lasti = 0; lastb = 0; }
-
-      let solve (c:context) : model
-          ensures { is_true_in (All.Engine.interp_of_model result.mod) c }
-          raises { Type.Unsat -> forall m. not (is_true_in m c) } =
-          {
-              mod = API.solve c;
-            lasti = PeanoInt63.to_int63 (Peano.pred c.nexti);
-            lastb = PeanoInt63.to_int63 (Peano.pred c.nextb);
-          }
-
-      let get_model_i (m:model) (v:ti): int
-          raises { UnknownVariable -> not (S.mem v (Type.defined_model m.mod).Var.si) }
-          ensures { Type.get_mod_int m.mod v = result } =
-          if 1 <= v.Var.vi <= m.lasti then ()
-          else raise UnknownVariable;
-          m.mod.Type.modi.Var.Hi.Lock.find v
-
-      let get_model_b (m:model) (v:tb): bool
-          raises { UnknownVariable -> not ( S.mem v (Type.defined_model m.mod).Var.sb) }
-          ensures { Type.get_mod_bool m.mod v = result } =
-          if 1 <= v.Var.vb <= m.lastb then ()
-          else raise UnknownVariable;
-          m.mod.Type.modb.Var.Hb.Lock.find v
-
-end
-
-
-
-(*
-module APIIntf
-(** commentaires *)
-       use mach.int.Int
-       use bool.Bool
-       use set.Fset as S
-       use list.List
-       use list.Mem as ListMem
-       use map.Map as Map
-
-       type int_var
-       type bool_var
-
-       type finite_mapping 'a 'b = abstract {
-            mapping: 'a -> 'b;
-            defined: S.fset 'a;
-       }
-
-       predicate extended (fm1:finite_mapping 'a 'b) (fm2:finite_mapping 'a 'b) (k:'a) (v:'b) =
-                 fm2.mapping = Map.set fm1.mapping k v /\
-                 fm2.defined = S.add k fm2.defined
-
-       type interp = abstract {
-            fm_int: finite_mapping int_var int;
-            fm_bool: finite_mapping bool_var bool;
-       }
-
-       function i (m:interp) : int_var -> int = m.fm_int.mapping
-       function b (m:interp) : bool_var -> bool = m.fm_bool.mapping
-
-       val function empty_interp: interp
-
-       axiom def_empty_interp:
-             empty_interp.fm_int.defined = S.empty /\
-             empty_interp.fm_bool.defined = S.empty
-
-
-       (** Inteprétation, une valuation, assigment *)
-
-       type interp_set = abstract { (** rename interp_set, infinite *)
-            mutable int_vars: S.fset int_var; (** finite set of usable integer variable *)
-            mutable bool_vars: S.fset bool_var; (** finite set of usable boolean variable *)
-            mutable interps: S.fset interp;
-       }
-       invariant { forall m. S.mem m interps -> int_vars = m.fm_int.defined }
-       invariant { forall m. S.mem m interps -> bool_vars = m.fm_bool.defined }
-       by {
-        interps = S.empty;
-        int_vars = S.empty;
-        bool_vars = S.empty;
-       }
-
-       (** tells if an interpretation is in the set of interpretion *)
-       predicate mem (m:interp) (c:interp_set) =
-                 S.mem m c.interps
-
-       (** start with all possible interpreatation *)
-       val create_interp_set () : interp_set
-           ensures { result.int_vars = S.empty }
-           ensures { result.bool_vars = S.empty }
-           ensures { S.cardinal result.interps = 1 }
-
-       val partial create_int_var (c:interp_set) (intmin:int) (intmax:int) : int_var
-           ensures { not (S.mem result (old c.int_vars)) }
-           ensures { c.int_vars = S.add result (old c.int_vars) }
-
-           ensures { forall m:interp. (old mem m c) -> forall i. intmin <= i <= intmax ->
-                        exists m'. mem m' c /\ extended m.fm_int m'.fm_int result i }
-           ensures { forall m':interp. (mem m' c) ->
-                        intmin <= m'.i result <= intmax /\
-                        exists m. (old mem m c) /\ extended m.fm_int m'.fm_int result (m'.i result) }
-
-           writes { c.int_vars }
-
-       val partial create_bool_var (c:interp_set) : bool_var
-           ensures { not (S.mem result (old c.bool_vars)) }
-           ensures { c.bool_vars = S.add result (old c.bool_vars) }
-
-           ensures { forall m:interp. (old mem m c) -> forall i.
-                        exists m'. mem m' c /\ extended m.fm_bool m'.fm_bool result i }
-           ensures { forall m':interp. (mem m' c) ->
-                        exists m. (old mem m c) /\ extended m.fm_bool m'.fm_bool result (m'.b result) }
-
-           writes { c.bool_vars }
-
-       (** We keep only from the set of interpretation the interpetation where [r] is true *)
-       val is_true (c:interp_set) (r:bool_var) : unit
-           requires { S.mem r c.bool_vars }
-           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r) ) }
-
-       (** Remove from the set of interpretation the interpetation where [r1] and [r2] are not opposite *)
-       val not_ (c:interp_set) (r1:bool_var) (r2:bool_var) : unit
-           requires { S.mem r1 c.bool_vars }
-           requires { S.mem r2 c.bool_vars }
-           ensures { forall m. mem m c <-> ((old mem m c) /\ notb (m.b r1) = m.b r2 ) }
-
-       (** Remove from the set of interpretation the interpetation where we don't have r = (v = iv) *)
-       val is_cst_reif (c:interp_set) (v:int_var) (iv:int) (r:bool_var) : unit
-           requires { S.mem v c.int_vars }
-           requires { S.mem r c.bool_vars }
-           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r <-> m.i v = iv) ) }
-           writes { c }
-
-       val add_reif (c:interp_set) (v1:int_var) (v2:int_var) (v3:int_var) (r:bool_var) : unit
-           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r <-> m.i v1 + m.i v2 = m.i v3) ) }
-           writes { c }
-
-       (** Remove from the set of interpretation the interpetation where [r1] and [r2] are not opposite *)
-       val le_reif (c:interp_set) (v1:int_var) (cst:int) (v2:int_var) (r:bool_var) : unit
-           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r <-> m.i v1 <= cst + m.i v2) ) }
-           writes { c }
-
-       exception Unsat
-
-       (** Create a model that belongs to the set of interpretation, if one exists. Otherwise raise Unsat *)
-       val partial solve (c:interp_set) : interp
-           (** The model is mem *)
-           ensures { mem result c }
-           raises { Unsat -> forall m. not (mem m c) } (** is_empty c *)
-
-       (** Create a model that belongs to the set of interpretation, if one exists. Otherwise raise Unsat *)
-       val partial solve_all (c:interp_set) : list interp
-           (** The model is mem *)
-           ensures { forall m. mem m c -> ListMem.mem m result }
-           raises { Unsat -> forall m. not (mem m c) } (** is_empty c *)
-
-       val get_int (m:interp) (v:int_var) : int
-           requires { S.mem v m.fm_int.defined }
-           ensures { result = m.i v }
-
-       val get_bool (m:interp) (v:bool_var) : bool
-           requires { S.mem v m.fm_bool.defined }
-           ensures { result = m.b v }
-
-end
-
-(**
-
-       let () =
-         let cxt = create_context () in
-         let a = create_vari cxt 0 10 in
-         let b = create_vari cxt 0 10 in
-         let c = create_vari cxt 0 10 in
-         add cxt a b c;
-         add cxt a c b;
-         let m = solve cxt in
-         let vc = get_int m c in
-         ....
-
-*)
-
-
-module API
-
-       use mach.int.Int
-       use bool.Bool
-       use list.List
-       use Var as Var
-       use mach.int.Int63
-       use mach.peano.Peano as Peano
-       use mach.peano.Int63 as PeanoInt63
-       use ConstraintSimple as Constraint
-       use ConstraintCst as ConstraintCst
-       use ConstraintIsTrue as ConstraintIsTrue
-       use ConstraintAdd as ConstraintAdd
-       use ConstraintLe as ConstraintLe
-       use ConstraintOr as ConstraintOr
-       use ConstraintNot as ConstraintNot
-       use All
-       use set.Fset as S
-       use map.Map as Map
-       use Type as Type
-       use list.Mem as ListMem
-
-
-       type int_var = Var.ti
-       type bool_var = Var.tb
-
-       type finite_mapping 'a 'b = {
-            mapping: 'a -> 'b;
-            defined: S.fset 'a;
-       }
-
-       predicate extended (fm1:finite_mapping 'a 'b) (fm2:finite_mapping 'a 'b) (k:'a) (v:'b) =
-                 fm2.mapping = Map.set fm1.mapping k v /\
-                 fm2.defined = S.add k fm2.defined
-
-       type interp = {
-            fm_int: finite_mapping int_var int;
-            fm_bool: finite_mapping bool_var bool;
-            model: Type.model int bool;
-       }
-       invariant { fm_int.mapping = model.Type.modi.Var.Hi.Lock.contents }
-       invariant { fm_int.defined = model.Type.modi.Var.Hi.Lock.defined }
-       invariant { fm_bool.mapping = model.Type.modb.Var.Hb.Lock.contents }
-       invariant { fm_bool.defined = model.Type.modb.Var.Hb.Lock.defined }
-
-       function i (m:interp) : int_var -> int = m.fm_int.mapping
-       function b (m:interp) : bool_var -> bool = m.fm_bool.mapping
-
-       (** Inteprétation, une valuation, assigment *)
-
-       let function true_ : bool_var = { Var.vb = 1 }
-       let function zero_ : int_var  = { Var.vi = 1 }
-
-       let ghost mk_interp (m:Type.model int bool) : interp =
-          {
-                fm_int = {
-                       mapping = m.Type.modi.Var.Hi.Lock.contents;
-                       defined = m.Type.modi.Var.Hi.Lock.defined;
-                };
-                fm_bool = {
-                       mapping = m.Type.modb.Var.Hb.Lock.contents;
-                       defined = m.Type.modb.Var.Hb.Lock.defined;
-                };
-                model = m;
-           }
-
-       let ghost base_interp () : interp
-           ensures { result.fm_int.defined = S.add zero_ S.empty }
-           ensures { result.fm_bool.defined = S.add true_ S.empty }
-           ensures { result.fm_int.mapping zero_ = 0 }
-           ensures { result.fm_bool.mapping true_ = true }
-       =
-           let modi = Var.Hi.create 2 0 (S.add zero_ S.empty) in
-           let modb = Var.Hb.create 2 true (S.add true_ S.empty) in
-           Var.Hi.set modi zero_ 0;
-           Var.Hb.set modb true_ true;
-           let p = mk_interp {
-               Type.modi = Var.Hi.copy_lock modi;
-               Type.modb = Var.Hb.copy_lock modb;
-           }
-           in
-           p
-
-       type interp_set = {
-            ghost mutable int_vars: S.fset int_var;
-            ghost mutable bool_vars: S.fset bool_var;
-            ghost mutable interps: S.fset interp;
-            mutable intmin : int;
-            mutable intmax : int;
-            mutable nexti: Peano.t;
-            mutable nextb: Peano.t;
-            mutable prob: list Constraint.t;
-       }
-       invariant { forall m. S.mem m interps -> int_vars = m.fm_int.defined }
-       invariant { forall m. S.mem m interps -> bool_vars = m.fm_bool.defined }
-       invariant { forall v. S.mem v int_vars -> 1 <= v.Var.vi < nexti }
-       invariant { forall v. S.mem v bool_vars -> 1 <= v.Var.vb < nextb }
-       invariant { let s = All.Engine.Prob.vars prob in
-                   (int_vars = s.Var.si)
-                /\ (bool_vars = s.Var.sb) }
-       invariant { 2 <= nexti }
-       invariant { 2 <= nextb }
-       invariant { S.mem true_ bool_vars }
-       invariant { forall m. All.Engine.Prob.is_true_in m prob -> m.Type.b true_ }
-       invariant { forall m. All.Engine.Prob.is_true_in m prob -> m.Type.i zero_ = 0 }
-       invariant { forall m. All.Engine.Prob.is_true_in m prob ->
-                   forall v. S.mem v int_vars -> intmin <= m.Type.i v <= intmax }
-       by {
-        interps = S.add (base_interp ()) S.empty;
-        intmin = 0;
-        intmax = 0;
-        int_vars = S.add zero_ S.empty;
-        bool_vars = S.add true_ S.empty;
-        nexti = Peano.succ Peano.one;
-        nextb = Peano.succ Peano.one;
-        prob =
-             (Cons (Constraint.Cst { ConstraintCst.v = zero_; ConstraintCst.i = 0; ConstraintCst.b = true_ })
-             (Cons (Constraint.IsTrue { ConstraintIsTrue.b = true_ })
-              Nil));
-       }
-
-       (** tells if an interpretation is in the set of interpretion *)
-       predicate mem (m:interp) (c:interp_set) =
-            m.fm_int.defined = c.int_vars /\ m.fm_bool.defined = c.bool_vars /\
-            All.Engine.Prob.is_true_in (All.Engine.interp_of_model m.model) c.prob
-
-
-       axiom only_defined_int: forall m c. mem m c -> c.int_vars = m.fm_int.defined
-       axiom only_defined_bool: forall m c. mem m c -> c.bool_vars = m.fm_bool.defined
-
-       (** start with all possible interpreatation *)
-       let create_interp_set () : interp_set
-           ensures { S.cardinal result.interps = 1 }
-       =
-         let c = {
-           interps = S.add (base_interp ()) S.empty;
-           intmin = 0;
-           intmax = 0;
-           int_vars = S.add zero_ S.empty;
-           nexti = Peano.succ Peano.one;
-           bool_vars = S.add true_ S.empty;
-           nextb = Peano.succ Peano.one;
-           prob =
-             (Cons (Constraint.Cst { ConstraintCst.v = zero_; ConstraintCst.i = 0; ConstraintCst.b = true_ })
-             (Cons (Constraint.IsTrue { ConstraintIsTrue.b = true_ })
-              Nil));
-         } in
-         c
-
-       type iter_fset 'a = {
-            mutable iter_fset_todo: S.fset 'a;
-            mutable iter_fset_done: S.fset 'a;
-            iter_fset_all: S.fset 'a;
-       }
-       invariant { S.(==) iter_fset_all (S.union iter_fset_done iter_fset_todo) }
-       invariant { S.(inter iter_fset_done iter_fset_todo == S.empty) }
-       by {
-         iter_fset_todo = S.empty;
-         iter_fset_done = S.empty;
-         iter_fset_all = S.empty;
-       }
-
-       let ghost create_iter_fset (s:S.fset 'a) : iter_fset 'a =
-        {
-         iter_fset_todo = s;
-         iter_fset_done = S.empty;
-         iter_fset_all = s
-        }
-
-       let ghost is_empty_iter_fset (s:iter_fset 'a) : bool
-          ensures { result = (S.is_empty s.iter_fset_todo) }
-         =
-           S.is_empty s.iter_fset_todo
-
-       let ghost next_iter_fset (s:iter_fset 'a) : 'a
-          requires { not (S.is_empty s.iter_fset_todo) }
-          ensures { S.mem result (old s.iter_fset_todo) }
-          ensures { s.iter_fset_todo = S.remove result (old s.iter_fset_todo) }
-          ensures { s.iter_fset_done = S.add result (old s.iter_fset_done) }
-         =
-           let e = S.pick s.iter_fset_todo in
-           s.iter_fset_todo <- S.remove e s.iter_fset_todo;
-           s.iter_fset_done <- S.add e s.iter_fset_done;
-           e
-
-       function variant_iter_fset (s:iter_fset 'a) : int
-           = S.cardinal s.iter_fset_todo
-
-       use ref.Ref
-
-       let partial create_int_var (c:interp_set) (intmin:int) (intmax:int) : int_var
-           ensures { not (S.mem result (old c.int_vars)) }
-           ensures { c.int_vars = S.add result (old c.int_vars) }
-
-           ensures { forall m:interp. (old mem m c) -> forall i. intmin <= i <= intmax ->
-                        exists m'. mem m' c /\ extended m.fm_int m'.fm_int result i }
-           ensures { forall m':interp. (mem m' c) ->
-                        intmin <= m'.i result <= intmax /\
-                        exists m. (old mem m c) /\ extended m.fm_int m'.fm_int result (m'.i result) }
-         =
-          c.nexti <- Peano.succ c.nexti;
-          let r = { Var.vi = (PeanoInt63.to_int63 c.nexti) - 1 } in
-          c.int_vars <- S.add r c.int_vars;
-          let constraint_min =
-              Constraint.Le { ConstraintLe.v1 = zero_; ConstraintLe.v2 = r;
-                              ConstraintLe.i = - intmin; ConstraintLe.b = true_}
-          in
-          let constraint_max =
-              Constraint.Le { ConstraintLe.v1 = r; ConstraintLe.v2 = zero_;
-                              ConstraintLe.i = intmax; ConstraintLe.b = true_}
-          in
-          c.prob <- Cons constraint_min (Cons constraint_max c.prob);
-          let ghost ref interps' = S.empty in
-          let ghost () =
-           if intmin <= intmax then
-             let iter = create_iter_fset c.interps in
-             while not (is_empty_iter_fset iter); do
-               variant { variant_iter_fset iter }
-               invariant { forall m:interp. S.mem m iter.iter_fset_done -> forall i. intmin <= i <= intmax ->
-                           exists m'. S.mem m' interps' /\ extended m.fm_int m'.fm_int r i }
-               invariant { forall m':interp. S.mem m' interps' ->
-                        intmin <= m'.i r <= intmax /\
-                        exists m. S.mem m iter.iter_fset_done /\ extended m.fm_int m'.fm_int r (m'.i r) }
-               let m = (next_iter_fset iter) in
-               let ref j = intmin in
-               let ghost ref interps'' = S.empty in
-               while j <= intmax do
-                 variant { intmax - j }
-                 invariant { intmin <= j <= intmax + 1 }
-                 invariant { forall i. intmin <= i < j ->
-                             exists m'. S.mem m' interps'' /\ extended m.fm_int m'.fm_int r i }
-                 invariant { forall m':interp. S.mem m' interps'' ->
-                          intmin <= m'.i r < j /\
-                          exists m. S.mem m iter.iter_fset_done /\ extended m.fm_int m'.fm_int r (m'.i r) }
-                 let m_modi = Var.Hi.copy_unlock m.model.Type.modi in
-                 Var.Hi.set m_modi r j;
-                 let m = mk_interp
-                     {
-                      Type.modi = Var.Hi.copy_lock m_modi;
-                      Type.modb = m.model.Type.modb
-                 } in
-                 interps'' <- S.add m interps'';
-                 j <- j+1;
-               done;
-               interps' <- S.union interps' interps'';
-             done;
-          in
-          c.interps <- interps';
-          r
-
-       let partial create_bool_var (c:interp_set) : bool_var
-           ensures { not (S.mem result (old c.bool_vars)) }
-           ensures { c.bool_vars = S.add result (old c.bool_vars) }
-
-           ensures { forall m:interp. (old mem m c) -> forall i.
-                        exists m'. mem m' c /\ extended m.fm_bool m'.fm_bool result i }
-           ensures { forall m':interp. (mem m' c) ->
-                        exists m. (old mem m c) /\ extended m.fm_bool m'.fm_bool result (m'.b result) }
-         =
-          c.nextb <- Peano.succ c.nextb;
-          let r = { Var.vb = PeanoInt63.to_int63 c.nextb - 1 } in
-          let _ = PeanoInt63.to_int63 c.nextb in
-          c.bool_vars <- S.add r c.bool_vars;
-          r
-
-       (** We keep only from the set of interpretation the interpetation where [r] is true *)
-       val is_true (c:interp_set) (r:bool_var) : unit
-           requires { S.mem r c.bool_vars }
-           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r) ) }
-
-       (** Remove from the set of interpretation the interpetation where [r1] and [r2] are not opposite *)
-       val not_ (c:interp_set) (r1:bool_var) (r2:bool_var) : unit
-           requires { S.mem r1 c.bool_vars }
-           requires { S.mem r2 c.bool_vars }
-           ensures { forall m. mem m c <-> ((old mem m c) /\ notb (m.b r1) = m.b r2 ) }
-
-       (** Remove from the set of interpretation the interpetation where we don't have r = (v = iv) *)
-       val is_cst_reif (c:interp_set) (v:int_var) (iv:int) (r:bool_var) : unit
-           requires { S.mem v c.int_vars }
-           requires { S.mem r c.bool_vars }
-           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r <-> m.i v = iv) ) }
-           writes { c }
-
-       val add_reif (c:interp_set) (v1:int_var) (v2:int_var) (v3:int_var) (r:bool_var) : unit
-           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r <-> m.i v1 + m.i v2 = m.i v3) ) }
-           writes { c }
-
-       (** Remove from the set of interpretation the interpetation where [r1] and [r2] are not opposite *)
-       val le_reif (c:interp_set) (v1:int_var) (cst:int) (v2:int_var) (r:bool_var) : unit
-           ensures { forall m. mem m c <-> ((old mem m c) /\ (m.b r <-> m.i v1 <= cst + m.i v2) ) }
-           writes { c }
-
-       exception Unsat
-
-       (** Create a model that belongs to the set of interpretation, if one exists. Otherwise raise Unsat *)
-       val partial solve (c:interp_set) : interp
-           (** The model is mem *)
-           ensures { mem result c }
-           raises { Unsat -> forall m. not (mem m c) } (** is_empty c *)
-
-       (** Create a model that belongs to the set of interpretation, if one exists. Otherwise raise Unsat *)
-       val partial solve_all (c:interp_set) : list interp
-           (** The model is mem *)
-           ensures { forall m. mem m c -> ListMem.mem m result }
-           raises { Unsat -> forall m. not (mem m c) } (** is_empty c *)
-
-       val get_int (m:interp) (v:int_var) : int
-           requires { S.mem v m.fm_int.defined }
-           ensures { result = m.i v }
-
-       val get_bool (m:interp) (v:bool_var) : bool
-           requires { S.mem v m.fm_bool.defined }
-           ensures { result = m.b v }
-(*
-       lemma true_is_true: forall c:context. forall m. is_true_in m c -> m.b true_
-
-       let is_cst_reif (c:context) (v:ti) (iv:int) (r:tb)
-           requires { S.mem v c.int_vars }
-           requires { S.mem r c.bool_vars }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v = iv) ) }
-       =
-       c.prob <- Cons ((Constraint.Cst {
-              ConstraintCst.v = v;
-              ConstraintCst.i = iv;
-              ConstraintCst.b = r })) c.prob
-
-       let is_cst (c:context) (v:ti) (iv:int)
-           requires { S.mem v c.int_vars }
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v = iv ) }
-       =
-        is_cst_reif c v iv true_
-
-       let add_reif (c:context) (v1:ti) (v2:ti) (v3:ti) (r:tb)
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ (m.b r <-> m.i v1 + m.i v2 = m.i v3) ) }
-       =
-       c.prob <- Cons ((Constraint.Add {
-              ConstraintAdd.v1 = v1;
-              ConstraintAdd.v2 = v2;
-              ConstraintAdd.v3 = v3;
-              ConstraintAdd.b = r })) c.prob
-
-       let add (c:context) (v1:ti) (v2:ti) (v3:ti)
-           ensures { forall m. is_true_in m c <-> ((old is_true_in m c) /\ m.i v1 + m.i v2 = m.i v3 ) }
-       =
-        add_reif c v1 v2 v3 true_
-
-       type model = Type.model int bool
-
-       function is_defined_ti (m:model) (v:ti) : bool =
-           S.mem v (Type.defined_model m).Var.si
-       function is_defined_tb (m:model) (v:tb) : bool =
-           S.mem v (Type.defined_model m).Var.sb
-
-       function interp_of_model (m:model) : interp = All.Engine.interp_of_model m
-
-       let solve' (c:context) : model
-           ensures { is_true_in (interp_of_model result) c }
-           ensures { forall v. S.mem v c.int_vars <-> is_defined_ti result v }
-           ensures { forall v. S.mem v c.bool_vars <-> is_defined_tb result v }
-           raises { Type.Unsat -> forall m. not (is_true_in m c) }
-           writes { } =
-           All.start' c.prob c.intmin c.intmax
-
-
-       let solve (c:context) : model
-           ensures { is_true_in (interp_of_model result) c }
-           ensures { forall v. S.mem v c.int_vars <-> is_defined_ti result v }
-           ensures { forall v. S.mem v c.bool_vars <-> is_defined_tb result v }
-           raises { Type.Unsat -> forall m. not (is_true_in m c) }
-           writes { } =
-           let _ = solve' c in absurd; raise Type.Unsat
-
-       let get_int (m:model) (v:ti) : int
-           requires { is_defined_ti m v }
-           ensures { result = (interp_of_model m).i v } =
-           Type.get_mod_int m v
-*)
-
-(*
-        clone APIIntf with
-              type ti = ti,
-              type tb = tb,
-              type interp = interp,
-              val mk_interp = mk_interp,
-              function i = i,
-              function b = b,
-              type context = context,
-              val true_ = true_,
-              predicate is_true_in = is_true_in,
-              val create_vari = create_vari,
-              val create_varb = create_varb,
-              val create_context = create_context,
-              val is_cst_reif = is_cst_reif,
-              val is_cst = is_cst,
-              val add_reif = add_reif,
-              val add = add,
-              lemma true_is_true,
-              exception Unsat = Type.Unsat,
-              type model = model,
-              function is_defined_ti = is_defined_ti,
-              function is_defined_tb = is_defined_tb,
-              function interp_of_model = interp_of_model,
-              val solve = solve,
-              val get_int = get_int
-*)
-end
-
-*)
diff --git a/src/lib/dune b/src/lib/dune
index af53de639a71f9f0654feb06ced9502c6b384dce..64ea512384e55422a9883396546f9db5eeabe211 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -1,16 +1,16 @@
 (library
         (public_name colibrics)
-        (modules cp__Int63 cp__Bool cp__Impl0 cp__Var0 cp__Type cp__Var cp__DomI cp__DomB cp__ConstraintSimple cp__ConstraintIsTrue cp__ConstraintAdd cp__ConstraintLe cp__ConstraintOr cp__ConstraintEquiv cp__ConstraintNot cp__ConstraintBoolPresent cp__ConstraintCst cp__All cp__ConstraintHelpers cp__API cp__APIDefensive colibrics)
+        (modules cp__Int63 cp__Bool cp__Impl0 cp__Var0 cp__Type cp__Var cp__DomI cp__DomB constraints__simple__Simple cp__ConstraintIsTrue cp__ConstraintAdd cp__ConstraintLe cp__ConstraintOr cp__ConstraintEquiv cp__ConstraintNot cp__ConstraintBoolPresent cp__ConstraintCst all__All cp__ConstraintHelpers all__API all__APIDefensive colibrics)
         (libraries zarith)
         (private_modules
-          cp__Int63 cp__Bool cp__Impl0 cp__Var0 cp__Type cp__Var cp__DomI cp__DomB cp__ConstraintSimple cp__ConstraintIsTrue cp__ConstraintAdd cp__ConstraintLe cp__ConstraintOr cp__ConstraintEquiv cp__ConstraintNot cp__ConstraintBoolPresent cp__ConstraintCst cp__All cp__ConstraintHelpers cp__API cp__APIDefensive)
+          cp__Int63 cp__Bool cp__Impl0 cp__Var0 cp__Type cp__Var cp__DomI cp__DomB constraints__simple__Simple cp__ConstraintIsTrue cp__ConstraintAdd cp__ConstraintLe cp__ConstraintOr cp__ConstraintEquiv cp__ConstraintNot cp__ConstraintBoolPresent cp__ConstraintCst all__All cp__ConstraintHelpers all__API all__APIDefensive)
        (flags (-w -3))
 )
 
 (rule
-   (deps cp.mlw cp.drv)
-   (targets cp__Int63.ml cp__Bool.ml cp__Impl0.ml cp__Var.ml cp__Var0.ml cp__Type.ml cp__DomB.ml cp__DomI.ml cp__ConstraintSimple.ml cp__ConstraintIsTrue.ml cp__ConstraintAdd.ml cp__ConstraintLe.ml cp__ConstraintOr.ml cp__ConstraintEquiv.ml cp__ConstraintNot.ml cp__ConstraintBoolPresent.ml cp__ConstraintCst.ml cp__ConstraintHelpers.ml cp__All.ml cp__API.ml cp__APIDefensive.ml)
+   (deps cp.mlw all.mlw cp.drv constraints/simple.mlw)
+   (targets cp__Int63.ml cp__Bool.ml cp__Impl0.ml cp__Var.ml cp__Var0.ml cp__Type.ml cp__DomB.ml cp__DomI.ml constraints__simple__Simple.ml cp__ConstraintIsTrue.ml cp__ConstraintAdd.ml cp__ConstraintLe.ml cp__ConstraintOr.ml cp__ConstraintEquiv.ml cp__ConstraintNot.ml cp__ConstraintBoolPresent.ml cp__ConstraintCst.ml cp__ConstraintHelpers.ml all__All.ml all__API.ml all__APIDefensive.ml)
    (action (run why3 extract -L . -D ocaml64 -D cp.drv -o . --modular
      cp.Int63 cp.Bool cp.Impl0 cp.Var cp.Var0 cp.Type cp.DomI cp.DomB cp.ConstraintCst cp.ConstraintCst
-     cp.ConstraintIsTrue cp.ConstraintAdd cp.ConstraintLe cp.ConstraintCst cp.ConstraintOr cp.ConstraintEquiv cp.ConstraintNot cp.ConstraintBoolPresent cp.ConstraintSimple cp.ConstraintHelpers cp.All cp.API cp.APIDefensive))
+     cp.ConstraintIsTrue cp.ConstraintAdd cp.ConstraintLe cp.ConstraintCst cp.ConstraintOr cp.ConstraintEquiv cp.ConstraintNot cp.ConstraintBoolPresent constraints.simple.Simple cp.ConstraintHelpers all.All all.API all.APIDefensive))
 )