diff --git a/domains/kaar.ml b/domains/kaar.ml
deleted file mode 100644
index b5eb352..0000000
--- a/domains/kaar.ml
+++ /dev/null
@@ -1,112 +0,0 @@
-let swap arr i j =
-  let tmp = arr.(i) in
-  arr.(i) <- arr.(j);
-  arr.(j) <- tmp
-
-module Matrix : sig
-  type t
-
-  val init : int -> int -> (int -> int -> Q.t) -> t
-  val copy : t -> t
-  val zero : int -> int -> t
-  val neg : t -> t
-  val add : t -> t -> t
-  val sub : t -> t -> t
-  val mul : t -> t -> t
-  val transpose : t -> t
-  val gauss : t * t -> t * t
-  val print : Format.formatter -> t -> unit
-end = struct
-  type t = { height : int; width : int; data : Q.t array array }
-
-  exception Incorrect_matrix_size
-
-  let init n m f =
-    {
-      height = n;
-      width = m;
-      data = Array.init n (fun i -> Array.init m (fun j -> f i j));
-    }
-
-  let copy m = init m.height m.width (fun i j -> m.data.(i).(j))
-  let zero n m = init n m (fun _ _ -> Q.zero)
-  let neg mat = init mat.width mat.height (fun i j -> Q.neg mat.data.(i).(j))
-
-  let add mat1 mat2 =
-    if mat1.width <> mat2.width || mat1.height <> mat2.height then
-      raise Incorrect_matrix_size
-    else
-      init mat1.height mat1.width (fun i j ->
-          Q.add mat1.data.(i).(j) mat2.data.(i).(j))
-
-  let sub mat1 mat2 = add mat1 (neg mat2)
-
-  let mul mat1 mat2 =
-    if mat1.width <> mat2.height then raise Incorrect_matrix_size
-    else
-      init mat1.height mat2.width (fun i j ->
-          List.fold_left
-            (fun sum k -> Q.add sum (Q.mul mat1.data.(i).(k) mat2.data.(k).(j)))
-            Q.zero
-            (List.init mat1.width (fun x -> x)))
-
-  let transpose mat = init mat.width mat.height (fun i j -> mat.data.(j).(i))
-
-  let gauss (m, c) =
-    let m' = copy m in
-    let c' = copy c in
-    let pivot line column =
-      let rec search_pivot l =
-        if l >= m'.height then None
-        else if not (Q.equal m'.data.(l).(column) Q.zero) then Some l
-        else search_pivot (l + 1)
-      in
-      let sub_line l sl coef =
-        for i = 0 to m'.width - 1 do
-          m'.data.(l).(i) <- Q.sub m'.data.(l).(i) (Q.mul coef m'.data.(sl).(i))
-        done;
-        for i = 0 to c'.width - 1 do
-          c'.data.(l).(i) <- Q.sub c'.data.(l).(i) (Q.mul coef c'.data.(sl).(i))
-        done
-      in
-      match search_pivot line with
-      | Some pline ->
-          swap m'.data line pline;
-          swap c'.data line pline;
-          let d = m'.data.(line).(column) in
-          for i = 0 to m'.width - 1 do
-            m'.data.(line).(i) <- Q.div m'.data.(line).(i) d
-          done;
-          for i = 0 to c'.width - 1 do
-            c'.data.(line).(i) <- Q.div c'.data.(line).(i) d
-          done;
-          if line <> m'.height - 1 then begin
-            for l = line + 1 to m'.height - 1 do
-              sub_line l line m'.data.(l).(column)
-            done;
-          end;
-          line + 1
-      | None -> line
-    in
-
-    if m'.height <> c'.height then raise Incorrect_matrix_size
-    else
-      let line = ref 0 in
-      for i = 0 to m'.width - 1 do
-        line := pivot !line i
-      done;
-      (m', c')
-
-  let print fmt mat =
-    Format.pp_print_string fmt "[";
-    Array.iter
-      (fun arr ->
-        Format.pp_print_string fmt "\n";
-        Array.iter
-          (fun elt ->
-            Format.pp_print_string fmt " ";
-            Q.pp_print fmt elt)
-          arr)
-      mat.data;
-    Format.pp_print_string fmt "\n]"
-end
diff --git a/domains/karr.ml b/domains/karr.ml
new file mode 100644
index 0000000..11abf77
--- /dev/null
+++ b/domains/karr.ml
@@ -0,0 +1,236 @@
+open Domain
+open Cfg
+open Abstract_syntax_tree
+
+let swap arr i j =
+  let tmp = arr.(i) in
+  arr.(i) <- arr.(j);
+  arr.(j) <- tmp
+
+module Matrix : sig
+  type t
+
+  val width : t -> int
+  val height : t -> int
+  val set : t -> int -> int -> Q.t -> unit
+  val get : t -> int -> int -> Q.t
+  val init : int -> int -> (int -> int -> Q.t) -> t
+  val copy : t -> t
+  val zero : int -> int -> t
+  val is_all_zero : t -> bool
+  val map : t -> (Q.t -> Q.t) -> t
+  val neg : t -> t
+  val add : t -> t -> t
+  val sub : t -> t -> t
+  val mul : t -> t -> t
+  val transpose : t -> t
+  val gauss : t * t -> t * t
+  val extend : t -> t -> t
+  val print : Format.formatter -> t -> unit
+end = struct
+  type t = { height : int; width : int; data : Q.t array array }
+
+  exception Incorrect_matrix_size
+
+  let width mat = mat.width
+  let height mat = mat.height
+
+  let set mat i j q =
+    mat.data.(i).(j) <- q;
+    ()
+
+  let get mat i j = mat.data.(i).(j)
+
+  let init n m f =
+    {
+      height = n;
+      width = m;
+      data = Array.init n (fun i -> Array.init m (fun j -> f i j));
+    }
+
+  let copy m = init m.height m.width (fun i j -> m.data.(i).(j))
+  let zero n m = init n m (fun _ _ -> Q.zero)
+
+  let is_all_zero mat =
+    Array.for_all
+      (fun a -> Array.for_all (fun elt -> Q.equal elt Q.zero) a)
+      mat.data
+
+  let map mat f = init mat.height mat.width (fun i j -> f mat.data.(i).(j))
+  let neg mat = init mat.height mat.width (fun i j -> Q.neg mat.data.(i).(j))
+
+  let add mat1 mat2 =
+    if mat1.width <> mat2.width || mat1.height <> mat2.height then
+      raise Incorrect_matrix_size
+    else
+      init mat1.height mat1.width (fun i j ->
+          Q.add mat1.data.(i).(j) mat2.data.(i).(j))
+
+  let sub mat1 mat2 = add mat1 (neg mat2)
+
+  let mul mat1 mat2 =
+    if mat1.width <> mat2.height then raise Incorrect_matrix_size
+    else
+      init mat1.height mat2.width (fun i j ->
+          List.fold_left
+            (fun sum k -> Q.add sum (Q.mul mat1.data.(i).(k) mat2.data.(k).(j)))
+            Q.zero
+            (List.init mat1.width (fun x -> x)))
+
+  let transpose mat = init mat.width mat.height (fun i j -> mat.data.(j).(i))
+
+  let gauss (m, c) =
+    let m' = copy m in
+    let c' = copy c in
+    let pivot line column =
+      let rec search_pivot l =
+        if l >= m'.height then None
+        else if not (Q.equal m'.data.(l).(column) Q.zero) then Some l
+        else search_pivot (l + 1)
+      in
+      let sub_line l sl coef =
+        for i = 0 to m'.width - 1 do
+          m'.data.(l).(i) <- Q.sub m'.data.(l).(i) (Q.mul coef m'.data.(sl).(i))
+        done;
+        for i = 0 to c'.width - 1 do
+          c'.data.(l).(i) <- Q.sub c'.data.(l).(i) (Q.mul coef c'.data.(sl).(i))
+        done
+      in
+      match search_pivot line with
+      | Some pline ->
+          swap m'.data line pline;
+          swap c'.data line pline;
+          let d = m'.data.(line).(column) in
+          for i = 0 to m'.width - 1 do
+            m'.data.(line).(i) <- Q.div m'.data.(line).(i) d
+          done;
+          for i = 0 to c'.width - 1 do
+            c'.data.(line).(i) <- Q.div c'.data.(line).(i) d
+          done;
+          if line <> m'.height - 1 then
+            for l = line + 1 to m'.height - 1 do
+              sub_line l line m'.data.(l).(column)
+            done;
+          line + 1
+      | None -> line
+    in
+
+    if m'.height <> c'.height then raise Incorrect_matrix_size
+    else
+      let line = ref 0 in
+      for i = 0 to m'.width - 1 do
+        line := pivot !line i
+      done;
+      let m'' = init !line m'.width (fun i j -> m'.data.(i).(j)) in
+      let c'' = init !line c'.width (fun i j -> c'.data.(i).(j)) in
+      (m'', c'')
+
+  let extend mat1 mat2 =
+    if mat1.width <> mat2.width then raise Incorrect_matrix_size
+    else
+      {
+        height = mat1.height + mat2.height;
+        width = mat1.width;
+        data = Array.append mat1.data mat2.data;
+      }
+
+  let print fmt mat =
+    Format.pp_print_string fmt "[";
+    Array.iter
+      (fun arr ->
+        Format.pp_print_string fmt "\n";
+        Array.iter
+          (fun elt ->
+            Format.pp_print_string fmt " ";
+            Q.pp_print fmt elt)
+          arr)
+      mat.data;
+    Format.pp_print_string fmt "\n]"
+end
+
+module Kaar : DOMAIN = struct
+  type t = Bot | E of Matrix.t * Matrix.t
+
+  exception Cant_assign
+
+  let init n = E (Matrix.zero 0 n, Matrix.zero 0 1)
+  let bottom = Bot
+
+  let assign env var expr =
+    match env with
+    | Bot -> Bot
+    | E (vars, consts) -> (
+        let n = Matrix.width vars in
+        let rec explore e =
+          match e with
+          | CFG_int_unary (unop, e') -> (
+              let v, c = explore e' in
+              match unop with
+              | AST_UNARY_PLUS -> (v, c)
+              | AST_UNARY_MINUS -> (Matrix.neg v, Q.neg c))
+          | CFG_int_binary (binop, e', e'') -> (
+              let v', c' = explore e' in
+              let v'', c'' = explore e'' in
+              match binop with
+              | AST_PLUS -> (Matrix.add v' v'', Q.add c' c'')
+              | AST_MINUS -> (Matrix.sub v' v'', Q.sub c' c'')
+              | AST_MULTIPLY ->
+                  if Matrix.is_all_zero v' then
+                    (Matrix.map v'' (fun q -> Q.mul q c'), Q.mul c' c'')
+                  else if Matrix.is_all_zero v'' then
+                    (Matrix.map v' (fun q -> Q.mul q c''), Q.mul c' c'')
+                  else raise Cant_assign
+              | AST_DIVIDE ->
+                  if Matrix.is_all_zero v'' then
+                    (Matrix.map v' (fun q -> Q.div q c''), Q.div c' c'')
+                  else raise Cant_assign
+              | AST_MODULO -> raise Cant_assign)
+          | CFG_int_var var ->
+              ( Matrix.init 1 n (fun i j ->
+                    if j = var.var_id then Q.one else Q.zero),
+                Q.zero )
+          | CFG_int_const const -> (Matrix.zero 1 n, Q.make const Z.one)
+          | CFG_int_rand (_, _) -> raise Cant_assign
+        in
+        try
+          let new_line, new_const = explore expr in
+          Matrix.set new_line 0 var.var_id
+            (Q.add (Matrix.get new_line 0 var.var_id) Q.one);
+          let new_vars = Matrix.extend vars new_line in
+          let new_consts =
+            Matrix.extend consts (Matrix.init 1 1 (fun _ _ -> new_const))
+          in
+          let v, c = Matrix.gauss (new_vars, new_consts) in
+          E (v, c)
+        with Cant_assign -> env)
+
+  let meet a b =
+    match (a, b) with
+    | Bot, _ | _, Bot -> Bot
+    | E (vars, consts), E (vars', consts') ->
+        let v, c =
+          Matrix.gauss (Matrix.extend vars vars', Matrix.extend consts consts')
+        in
+        E (v, c)
+
+  let widen = join
+
+  let narrow = meet
+
+  let subset a b =
+    match (a, b) with
+    | Bot, _ -> true
+    | _, Bot -> false
+    | E (vars, consts), E (vars', consts') ->
+        let v = Matrix.extend vars vars' in
+        let c = Matrix.extend consts consts' in
+        let v', c' = Matrix.gauss (v, c) in
+        Matrix.is_all_zero (Matrix.sub v' vars)
+        && Matrix.is_all_zero (Matrix.sub c' consts)
+
+  let is_bottom = function Bot -> true | _ -> false
+
+  let print fmt = function
+    | Bot -> Format.pp_print_string fmt "Bot\n"
+    | E (vars, consts) -> Matrix.print fmt vars
+end