diff --git a/Makefile b/Makefile
index 3a79d2e9..9745db2b 100644
--- a/Makefile
+++ b/Makefile
@@ -3,7 +3,6 @@
 LOG=build.log
 COMP=ocamlbuild -log $(LOG) -use-ocamlfind
 FLAGS=
-# -cflags -color,always
 DOC=msat.docdir/index.html
 BIN=main.native
 NAME=msat
diff --git a/_tags b/_tags
index 36a8cd38..11e609f7 100644
--- a/_tags
+++ b/_tags
@@ -1,3 +1,6 @@
+# colors
+true: color(always)
+
 # optimization options
 true: optimize(3), unbox_closures
 
diff --git a/backend/dot.ml b/backend/dot.ml
index cc04791a..7878925f 100644
--- a/backend/dot.ml
+++ b/backend/dot.ml
@@ -18,6 +18,15 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemm
 
   let proof_id p = node_id (S.expand p)
 
+  let print_clause fmt c =
+    let v = c.S.St.atoms in
+    let n = Vec.size v in
+    for i = 0 to n - 1 do
+      Format.fprintf fmt "%a" A.print_atom (Vec.get v i);
+      if i < n - 1 then
+        Format.fprintf fmt ", "
+    done
+
   let print_edge fmt i j =
     Format.fprintf fmt "%s -> %s;@\n" i j
 
@@ -32,7 +41,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemm
     Format.fprintf fmt "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\" BGCOLOR=\"%s\"" color
 
   let table fmt (c, rule, color, l) =
-    Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR>" S.print_clause c;
+    Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR>" print_clause c;
     match l with
     | [] ->
       Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" colspan=\"2\">%s</TD></TR>" color rule
diff --git a/solver/solver.mli b/solver/solver.mli
index 05d4b5f0..e9e1ab7f 100644
--- a/solver/solver.mli
+++ b/solver/solver.mli
@@ -1,15 +1,8 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Mohamed Iguernelala                                   *)
-(*                  Universite Paris-Sud 11                               *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
 
 module type S = Solver_intf.S