diff --git a/Fixpoint.hs b/Fixpoint.hs
--- a/Fixpoint.hs
+++ b/Fixpoint.hs
@@ -38,7 +38,7 @@
   &= verbosity
   &= program "fixpoint" 
   &= help    "Predicate Abstraction Based Horn-Clause Solver" 
-  &= summary "fixpoint © Copyright 2009-13 Regents of the University of California." 
+  &= summary "fixpoint Copyright 2009-13 Regents of the University of California." 
   &= details [ "Predicate Abstraction Based Horn-Clause Solver"
              , ""
              , "To check a file foo.fq type:"
@@ -50,7 +50,7 @@
              putStrLn $ banner md
              return md
 
-banner args =  "Liquid-Fixpoint © Copyright 2009-13 Regents of the University of California.\n" 
+banner args =  "Liquid-Fixpoint Copyright 2009-13 Regents of the University of California.\n" 
             ++ "All Rights Reserved.\n"
 
 ---------------------------------------------------------------------------------
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2013, Ranjit Jhala
+Copyright (c) 2013-2014, Ranjit Jhala
 
 All rights reserved.
 
diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -4,37 +4,49 @@
 import Distribution.Simple
 import Distribution.Simple.LocalBuildInfo
 import Distribution.Simple.Setup
-import System.Posix.Env
-import System.Process
+import Distribution.System
+import System.Directory
+import System.Environment
 import System.Exit
+import System.FilePath
+import System.Process
 
-main         = defaultMainWithHooks fixHooks
+main       = defaultMainWithHooks fixHooks
   where
-    fixHooks = simpleUserHooks { postBuild = buildFixpoint
-                               , postCopy = copyFixpoint
-                               , postInst = copyFixpoint
-                               }
+  fixHooks = simpleUserHooks { postBuild = buildFixpoint
+                             , postCopy = copyFixpoint
+                             , postInst = copyFixpoint
+                             }
 
-buildFixpoint _ _ pkg lbi
-  = do setEnv "Z3MEM" (show z3mem) True
-       executeShellCommand "./configure"
-       executeShellCommand "./build.sh"
-       executeShellCommand "chmod a+x external/fixpoint/fixpoint.native "
+copyFixpoint _ _ pkg lbi = do
+  copyFile fixpoint bin
   where
-    allDirs     = absoluteInstallDirs pkg lbi NoCopyDest
-    binDir      = bindir allDirs ++ "/"
-    flags       = configConfigurationsFlags $ configFlags lbi
-    z3mem       = fromMaybe False $ lookup (FlagName "z3mem") flags
+  allDirs     = absoluteInstallDirs pkg lbi NoCopyDest
+  bin         = bindir allDirs </> "fixpoint.native"
+             ++ if system == "i686-w64-mingw32" then ".exe" else ""
+  fixpoint    = "external" </> "fixpoint" </> "fixpoint.native"
+             ++ if build then "" else "-" ++ system
+  system      = case hostPlatform lbi of
+                  Platform I386 Linux -> "i386-linux"
+                  Platform X86_64 Linux -> "x86_64-linux"
+                  Platform X86_64 OSX -> "x86_64-darwin"
+                  Platform _      Windows -> "i686-w64-mingw32"
+                  _ -> error "We don't have a prebuilt fixpoint.native for your system, please install with -fbuild-external (requires ocaml)"
+  flags       = configConfigurationsFlags $ configFlags lbi
+  build       = fromMaybe False $ lookup (FlagName "build-external") flags
 
-copyFixpoint _ _ pkg lbi
-  = do executeShellCommand $ "cp external/fixpoint/fixpoint.native " ++ binDir
-       when z3mem $
-         executeShellCommand $ "cp external/z3/lib/libz3.* "         ++ binDir
+
+buildFixpoint _ _ pkg lbi = when build $ do
+  setEnv "Z3MEM" (show z3mem)
+  executeShellCommand "./configure"
+  executeShellCommand "./build.sh"
+  executeShellCommand "chmod a+x external/fixpoint/fixpoint.native "
   where
-    allDirs     = absoluteInstallDirs pkg lbi NoCopyDest
-    binDir      = bindir allDirs ++ "/"
-    flags       = configConfigurationsFlags $ configFlags lbi
-    z3mem       = fromMaybe False $ lookup (FlagName "z3mem") flags
+  allDirs     = absoluteInstallDirs pkg lbi NoCopyDest
+  binDir      = bindir allDirs ++ "/"
+  flags       = configConfigurationsFlags $ configFlags lbi
+  z3mem       = fromMaybe False $ lookup (FlagName "z3mem") flags
+  build       = fromMaybe False $ lookup (FlagName "build-external") flags
 
 executeShellCommand cmd   = putStrLn ("EXEC: " ++ cmd) >> system cmd >>= check
   where
diff --git a/external/fixpoint/Makefile b/external/fixpoint/Makefile
--- a/external/fixpoint/Makefile
+++ b/external/fixpoint/Makefile
@@ -5,7 +5,7 @@
 
 LIBS_=-libs unix,str,graph
 IFLAGS_=-lflags -I,$(OCAMLGRAPHHOME)
-LFLAGS_=-lflags -cclib,-L$(OCAMLLIB) \
+LFLAGS_=-lflags -cclib,-L$(OCAMLLIB)
 
 CFLAGS_=-cflags -dtypes,-annot \
 		-cflags -I,$(OCAMLGRAPHHOME) \
diff --git a/external/fixpoint/ast.ml b/external/fixpoint/ast.ml
--- a/external/fixpoint/ast.ml
+++ b/external/fixpoint/ast.ml
@@ -1133,6 +1133,19 @@
   | Sort.Lvar _ -> None
   | Sort.LFun   -> None
 
+let uf_arity f uf =  
+  match sortcheck_sym f uf with None -> None | Some t -> 
+    match Sort.func_of_t t with None -> None | Some (i,_,_) -> 
+      Some i
+ 
+let solved_app f uf = function
+  | Some (s, t) -> begin match uf_arity f uf with
+                     | Some n -> if Sort.check_arity n s then Some t else None
+                     | _      -> None
+                   end 
+  | None        -> None
+
+
 let rec sortcheck_expr g f e = 
   match euw e with
   | Bot   -> 
@@ -1202,7 +1215,6 @@
   *)
 
 
-
 and sortcheck_op g f (e1, op, e2) =
 (* DEBUGGING   
   let (s1, s2) = Misc.map_pair (sortcheck_expr g f) (e1, e2) in 
@@ -1295,6 +1307,16 @@
          | Some tx -> not (None = sortcheck_app g f (Some tx) uf es)
          end
 
+    | Atom (((App (uf1, e1s), _) as e1), Eq, ((App (uf2, e2s), _) as e2))
+      -> let t1o = solved_app f uf1 <| sortcheck_app_sub g f None uf1 e1s in
+         let t2o = solved_app f uf2 <| sortcheck_app_sub g f None uf2 e2s in
+         begin match t1o, t2o with
+               | (Some t1, Some t2) -> t1 = t2
+               | (None, None)       -> false 
+               | (None, Some t2)    -> not (None = sortcheck_app g f (Some t2) uf1 e1s)
+               | (Some t1, None)    -> not (None = sortcheck_app g f (Some t1) uf2 e2s) 
+         end
+
     | Atom (e1, r, e2) ->
         sortcheck_rel g f (e1, r, e2)
     | Forall (qs,p) ->
@@ -1308,19 +1330,31 @@
   >> (fun b -> if not b then F.eprintf "WARNING: Malformed Lhs Pred (%a)\n" Predicate.print p) 
  *)
 
-let uf_arity f uf =  
-  match sortcheck_sym f uf with None -> None | Some t -> 
-    match Sort.func_of_t t with None -> None | Some (i,_,_) -> 
-      Some i
- 
+let opt_to_string p = function
+  | None   -> "none"
+  | Some x -> p x
+
+
 (* API *)
-let sortcheck_app g f t uf es = 
-  match uf_arity f uf, sortcheck_app_sub g f t uf es with 
-    | (Some n , Some (s, t)) -> 
-        if Sort.check_arity n s then Some (s, t) else
-           assertf "Ast.sortcheck_app: type args not fully instantiated %s" 
-             (expr_to_string (eApp (uf, es)))
+let sortcheck_app g f tExp uf es = 
+  match uf_arity f uf, sortcheck_app_sub g f tExp uf es with 
+    | (Some n, Some (s, t)) -> 
+        if Sort.check_arity n s then 
+           Some (s, t) 
+        else
+          None
+          (*
+          let msg = Printf.sprintf  "Ast.sortcheck_app: type params not instantiated %s: n = %d, s = %s, t = %s, tExp = %s"
+                      (expr_to_string (eApp (uf, es)))
+                      n
+                      (Sort.sub_to_string s)
+                      (Sort.to_string t)         
+                      (opt_to_string Sort.to_string tExp)
+          in
+             assertf "%s" msg
+             *)
     | _ -> None
+
 
 (*
 let sortcheck_pred f p = 
diff --git a/external/fixpoint/fixParse.mly b/external/fixpoint/fixParse.mly
--- a/external/fixpoint/fixParse.mly
+++ b/external/fixpoint/fixParse.mly
@@ -232,15 +232,15 @@
 ;
 
 pred:
-    TRUE				                { A.pTrue }
-  | FALSE				                { A.pFalse }
+    TRUE				{ A.pTrue }
+  | FALSE				{ A.pFalse }
   | BEXP expr                           { A.pBexp $2 }
   | QM expr                             { A.pBexp $2 }
   | Id LPAREN argsne RPAREN             { A.pBexp (A.eApp ((Sy.of_string $1), $3)) }
-  | AND preds   			            { A.pAnd ($2) }
-  | OR  preds 	        		        { A.pOr  ($2) }
-  | NOT pred				            { A.pNot ($2) }
-  | NOTWORD pred				        { A.pNot ($2) }
+  | AND preds   			{ A.pAnd ($2) }
+  | OR  preds 	        		{ A.pOr  ($2) }
+  | NOT pred				{ A.pNot ($2) }
+  | NOTWORD pred			{ A.pNot ($2) }
   | LPAREN pred AND pred RPAREN         { A.pAnd [$2; $4] }
   | LPAREN pred OR  pred RPAREN         { A.pOr  [$2; $4] }
   | expr rel expr                       { A.pAtom  ($1, $2, $3) }
@@ -249,7 +249,7 @@
   | pred IMPL pred                      { A.pImp ($1, $3) }
   | pred IFF pred                       { A.pIff ($1, $3) }
   | pred IFFWORD pred                   { A.pIff ($1, $3) }
-  | LPAREN pred RPAREN			        { $2 }
+  | LPAREN pred RPAREN			{ $2 }
   ;
 
 argsne:
diff --git a/external/fixpoint/fixpoint.native-i386-linux b/external/fixpoint/fixpoint.native-i386-linux
new file mode 100644
Binary files /dev/null and b/external/fixpoint/fixpoint.native-i386-linux differ
diff --git a/external/fixpoint/fixpoint.native-i686-w64-mingw32 b/external/fixpoint/fixpoint.native-i686-w64-mingw32
new file mode 100644
Binary files /dev/null and b/external/fixpoint/fixpoint.native-i686-w64-mingw32 differ
diff --git a/external/fixpoint/fixpoint.native-x86_64-darwin b/external/fixpoint/fixpoint.native-x86_64-darwin
new file mode 100644
# file too large to diff: external/fixpoint/fixpoint.native-x86_64-darwin
diff --git a/external/fixpoint/fixpoint.native-x86_64-linux b/external/fixpoint/fixpoint.native-x86_64-linux
new file mode 100644
# file too large to diff: external/fixpoint/fixpoint.native-x86_64-linux
diff --git a/external/fixpoint/foo.ml b/external/fixpoint/foo.ml
new file mode 100644
--- /dev/null
+++ b/external/fixpoint/foo.ml
@@ -0,0 +1,6 @@
+let main ()
+  = let co,ci = Unix.open_process "cvc4 --print-success --incremental" in
+    output_string ci "QUERY TRUE;\n";
+    let r = input_line co in
+    print_endline r
+let _ = main ()
diff --git a/external/fixpoint/smtLIB2.ml b/external/fixpoint/smtLIB2.ml
--- a/external/fixpoint/smtLIB2.ml
+++ b/external/fixpoint/smtLIB2.ml
@@ -95,8 +95,8 @@
 (*********************** Set Theory ********************************)
 (*******************************************************************)
 
-let elt = "Elt"
-let set = "Set"
+let elt = "SMT_Elt"
+let set = "SMT_Set"
 let emp = "smt_set_emp"
 let add = "smt_set_add"
 let cup = "smt_set_cup"
@@ -117,9 +117,15 @@
    (define-fun smt_set_sub ((s1 Set) (s2 Set)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
 *)
 
+let (++) = List.append
+
 (* z3 specific *)
 let z3_preamble _  
- = if not !Co.set_theory then [] else
+ =  [ "(set-option :auto-config false)"
+    ; "(set-option :model true)"
+    ; "(set-option :model.partial false)"
+    ; "(set-option :smt.mbqi false)"
+    ] ++ if not !Co.set_theory then [] else
     [ spr "(define-sort %s () Int)"
         elt
     ; spr "(define-sort %s () (Array %s Bool))" 
@@ -142,6 +148,36 @@
         sub set set emp dif 
     ] 
 
+(* cvc4 specific *)
+let cvc4_preamble _  
+ =  if not !Co.set_theory then [] else
+    [ spr "(set-logic QF_UFNIRAFS)"
+    ; spr "(define-sort %s () Int)"
+        elt
+    ; spr "(define-sort %s () (Set %s))" 
+        set elt
+    ; spr "(define-fun %s () %s (as emptyset (Set %s)))"
+        emp set elt
+    ; spr "(define-fun %s ((x %s) (s %s)) Bool (member x s))"
+        mem elt set
+    ; spr "(define-fun %s ((s %s) (x %s)) %s (insert x s))"
+        add set elt set
+    ; spr "(define-fun %s ((s1 %s) (s2 %s)) %s (union s1 s2))"
+        cup set set set
+    ; spr "(define-fun %s ((s1 %s) (s2 %s)) %s (intersection s1 s2))"
+        cap set set set
+    ; spr "(declare-fun %s (%s) %s)"
+        com set set
+    (* 
+    ; spr "(define-fun %s ((s %s)) %s ((_ map not) s))"
+        com set set
+     *)
+    ; spr "(define-fun %s ((s1 %s) (s2 %s)) %s (setminus s1 s2))"
+        dif set set set
+    ; spr "(define-fun %s ((s1 %s) (s2 %s)) Bool (subset s1 s2))"
+        sub set set
+    ] 
+
 let smtlib_preamble 
   = [ spr "(set-logic QF_UFLIA)"
     ; spr "(define-sort %s () Int)"       elt
@@ -198,6 +234,7 @@
 
 let smt_preamble = function
   | Z3 -> z3_preamble ()
+  | Cvc4 -> cvc4_preamble ()
   | _  -> smtlib_preamble 
 
 
@@ -205,8 +242,30 @@
   output_now me.clog s; 
   output_now me.cout s
 
+(* copied from String.trim in ocaml-4.0 since mingw-ocaml uses 3.x *)
+let trim s =
+  let is_space = function
+    | ' ' | '\012' | '\n' | '\r' | '\t' -> true
+    | _ -> false in
+  let len = String.length s in
+  let i = ref 0 in
+  while !i < len && is_space (String.get s !i) do
+    incr i
+  done;
+  let j = ref (len - 1) in
+  while !j >= !i && is_space (String.get s !j) do
+    decr j
+  done;
+  if !i = 0 && !j = len - 1 then
+    s
+  else if !j >= !i then
+    String.sub s !i (!j - !i + 1)
+  else
+    ""
+
+(* strip off trailing whitespace, e.g. \r on windows.. *)
 let smt_read_raw me = 
-  input_line me.cin
+  trim (input_line me.cin)
 
 let smt_write me ?nl:(nl=true) ?tab:(tab=false) s =
   let pre = if tab then "    " else "" in
@@ -320,8 +379,10 @@
 let mkRealSort _   = "Real"          
 let mkBoolSort _   = "Bool"         
 
-let mkInt _ i _    = string_of_int i
-let mkReal _ i _   = string_of_float i
+let mkInt _ i _    = if i >= 0 then string_of_int i
+                     else spr "(- %d)" (abs i)
+let mkReal _ i _   = if i >= 0. then string_of_float i ^ "0" (* add trailing 0 for floats like 1. *)
+                     else spr "(- %s)" (string_of_float (i *. -1.0) ^ "0")
 let mkTrue _       = "true"
 let mkFalse _      = "false" 
 
diff --git a/external/fixpoint/smtZ3.ml b/external/fixpoint/smtZ3.ml
deleted file mode 100644
--- a/external/fixpoint/smtZ3.ml
+++ /dev/null
@@ -1,84 +0,0 @@
-(*
- * Copyright © 2008 The Regents of the University of California. All rights reserved.
- *
- * Permission is hereby granted, without written agreement and without
- * license or royalty fees, to use, copy, modify, and distribute this
- * software and its documentation for any purpose, provided that the
- * above copyright notice and the following two paragraphs appear in
- * all copies of this software.
- *
- * IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY
- * FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES
- * ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN
- * IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY
- * OF SUCH DAMAGE.
- *
- * THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
- * INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY
- * AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
- * ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION
- * TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
- *)
-
-(********************************************************************************)
-(** DUMMY SMT-Z3 Solver (for non Z3MEM builds) **********************************)
-(********************************************************************************)
-
-let assertf = FixMisc.Ops.assertf
-let msg     = "This build is NOT linked against Z3. Please rebuild with Z3MEM=true. Only possible on linux"
-
-module SMTZ3 : ProverArch.SMTSOLVER = struct
-
-type context     = ()
-type symbol      = ()   
-type sort        = () 
-type ast         = () 
-type fun_decl    = ()  
-
-let var          _   = failwith msg 
-let boundVar     _   = failwith msg
-let stringSymbol _   = failwith msg
-let funcDecl     _   = failwith msg
-let isBool _         = failwith msg
-let isInt _          = failwith msg
-let mkAll _          = failwith msg
-let mkRel _          = failwith msg
-let mkApp _          = failwith msg  
-let mkMul _          = failwith msg
-let mkDiv _          = failwith msg
-let mkAdd _          = failwith msg
-let mkSub _          = failwith msg
-let mkMod _          = failwith msg
-let mkIte _          = failwith msg
-let mkInt _          = failwith msg  
-let mkReal _         = failwith msg  
-let mkTrue _         = failwith msg
-let mkFalse _        = failwith msg
-let mkNot _          = failwith msg
-let mkAnd _          = failwith msg 
-let mkOr _           = failwith msg 
-let mkImp _          = failwith msg 
-let mkIff _          = failwith msg
-let astString _      = failwith msg
-let mkIntSort _      = failwith msg
-let mkRealSort _     = failwith msg
-let mkBoolSort _     = failwith msg
-let mkSetSort _      = failwith msg
-let mkEmptySet _     = failwith msg
-let mkSetAdd _       = failwith msg
-let mkSetMem _       = failwith msg
-let mkSetCup _       = failwith msg
-let mkSetCap _       = failwith msg
-let mkSetDif _       = failwith msg
-let mkSetSub _       = failwith msg
-let mkContext _      = failwith msg
-let unsat _          = failwith msg  
-let assertAxiom _    = failwith msg
-let assertDistinct _ = failwith msg
-let bracket _        = failwith msg
-let assertPreds _    = failwith msg
-let valid _          = failwith msg 
-let contra _         = failwith msg
-let print_stats _    = failwith msg
-
-end
diff --git a/external/fixpoint/theories.ml b/external/fixpoint/theories.ml
--- a/external/fixpoint/theories.ml
+++ b/external/fixpoint/theories.ml
@@ -33,6 +33,9 @@
 let is_interp t = t = set_tycon
 
 (* API *)
+let emp0 = ( Sy.of_string "Set_empty"
+           , So.t_func 1 [So.t_int; t_set (So.t_generic 0)] )
+
 let emp = ( Sy.of_string "Set_emp"
           , So.t_func 1 [t_set (So.t_generic 0); So.t_bool] )
 
@@ -57,7 +60,7 @@
 
 let interp_syms _ 
   = if !Constants.set_theory 
-     then [emp; sng; mem; cup; cap; dif; sub]
+     then [emp0; emp; sng; mem; cup; cap; dif; sub]
      else []
 
 module MakeTheory(SMT : SMTSOLVER): 
@@ -98,6 +101,17 @@
                  | _ -> assertf "Set_set: type mismatch"
   }  
 
+
+let set_empty : appDef  = 
+  { sy_name  = fst emp0
+  ; sy_sort  = snd emp0 
+  ; sy_emb   = fun c ts es -> match ts, es with
+                 | [t], [_] -> SMT.mkEmptySet c t
+                 | _        -> assertf "Set_empty: type mismatch"
+  }
+
+
+
 let set_emp : appDef  = 
   { sy_name  = fst emp 
   ; sy_sort  = snd emp 
@@ -189,6 +203,7 @@
 (* API *)
 let theories = 
   ([set_set], [set_emp; 
+	       set_empty; 
                set_sng; 
                set_mem; 
                set_cup; 
diff --git a/external/fixpoint/tpGen.ml b/external/fixpoint/tpGen.ml
--- a/external/fixpoint/tpGen.ml
+++ b/external/fixpoint/tpGen.ml
@@ -187,9 +187,23 @@
 (********************** Pred/Expr Transl ******************************)
 (**********************************************************************)
 
+let opt_to_string p = function
+  | None   -> "none"
+  | Some x -> p x
  
 exception Z3RelTypeError
 
+let pred_sort env p = 
+  A.sortcheck_pred Theories.is_interp (Misc.flip SM.maybe_find env) p 
+
+let app_sort env tyo f es =
+  A.sortcheck_app Theories.is_interp (Misc.flip SM.maybe_find env) tyo f es
+
+let expr_sort env = function
+  | A.App (f, es), _ -> Misc.maybe_map snd <| app_sort env None f es 
+  | e                -> A.sortcheck_expr Theories.is_interp (Misc.flip SM.maybe_find env) e
+
+
 let z3Bind me env x t =
   let vx = Vbl (x, varSort env x) in
   me.bnd <- me.bnd + 1; 
@@ -198,12 +212,15 @@
   SMT.stringSymbol me.c (fresh "z3b")
 
 let rec z3Rel me env (e1, r, e2) =
-  let p  = A.pAtom (e1, r, e2)                                   in
-  let ok = A.sortcheck_pred Theories.is_interp (Misc.flip SM.maybe_find env) p   in 
+  let p  = A.pAtom (e1, r, e2) in
+  let ok = pred_sort env p     in 
   (* let _  = F.printf "z3Rel: e = %a, res = %b \n" P.print p ok in
      let _  = F.print_flush ()                                   in *)
+
   if ok then 
-    SMT.mkRel me.c r (z3Exp me env e1) (z3Exp me env e2)
+    z3Rel_cast me env (e1, r, e2)
+    (* z3Rel_real me env (e1, r, e2) *)
+    (* SMT.mkRel me.c r (z3Exp me env e1) (z3Exp me env e2) *)
   else begin 
     SM.iter (fun s t -> F.printf "@[%a :: %a@]@." Sy.print s So.print t) env;
     F.printf "@[%a@]@.@." P.print (A.pAtom (e1, r, e2));
@@ -211,13 +228,38 @@
     raise Z3RelTypeError
   end
 
+
+
+
+and z3Rel_cast me env = function
+  | (e1, A.Eq, e2) -> begin
+      let (t1o, t2o) = (expr_sort env e1, expr_sort env e2) in 
+      (* let _ = F.printf "z3Rel_cast: t1o = %s, t2o = %s \n" 
+                (opt_to_string So.to_string t1o) (opt_to_string So.to_string t2o) in
+       *)
+      match (t1o, t2o) with
+        | (Some t , None  ) -> z3Rel_real me env (e1, A.Eq, A.eCst (e2, t))  
+        | (None   , Some t) -> z3Rel_real me env (A.eCst (e1, t), A.Eq, e2)
+        | (_      , _     ) -> z3Rel_real me env (e1, A.Eq, e2) 
+    end
+  | (e1, r, e2) -> 
+      z3Rel_real me env (e1, r, e2) 
+
+and z3Rel_real me env (e1, r, e2) =
+  (* let _ = F.printf "z3Rel_real: e1 = %s, e2 = %s \n"
+            (E.to_string e1)
+            (E.to_string e2) in
+   *)
+  SMT.mkRel me.c r (z3Exp me env e1) (z3Exp me env e2)
+
 and z3App me env p zes =
   let t  = funSort env p                      in
   let cf = z3Fun me env p t (List.length zes) in
   SMT.mkApp me.c cf zes
 
 and z3AppThy me env def tyo f es = 
-  match A.sortcheck_app Theories.is_interp (Misc.flip SM.maybe_find env) tyo f es with 
+  (* match A.sortcheck_app Theories.is_interp (Misc.flip SM.maybe_find env) tyo f es with *)
+  match app_sort env tyo f es with 
     | Some (s, t) ->
         let zts = So.sub_args s |> List.map (snd <+> z3Type me) in
         let zes = es            |> List.map (z3Exp me env)      in
@@ -299,10 +341,9 @@
   | A.Bexp e, _ -> 
       let a  = z3Exp me env e in
       let s2  = E.to_string e in
-      let so = match A.sortcheck_expr Theories.is_interp (Misc.flip SM.maybe_find env) e with  
-                | Some so -> so
-                | _ -> F.printf "No type for %s" (E.to_string e);
-                       assert false in
+      let so = match expr_sort env e with Some so -> so
+                 | _ -> F.printf "No type for %s" (E.to_string e);
+                        assert false in
       let sos = So.to_string so in
       (* let s1  = SMT.astString me.c a in
       let _   = asserts (SMT.isBool me.c a) 
diff --git a/external/ocamlgraph/META b/external/ocamlgraph/META
deleted file mode 100644
--- a/external/ocamlgraph/META
+++ /dev/null
@@ -1,5 +0,0 @@
-version = "0.99b"
-description = "Generic Graph Library"
-requires=""
-archive(byte) = "graph.cma"
-archive(native) = "graph.cmxa"
diff --git a/external/ocamlgraph/Makefile b/external/ocamlgraph/Makefile
deleted file mode 100644
--- a/external/ocamlgraph/Makefile
+++ /dev/null
@@ -1,386 +0,0 @@
-##########################################################################
-#                                                                        #
-#  Ocamlgraph: a generic graph library for OCaml                         #
-#  Copyright (C) 2004-2007                                               #
-#  Sylvain Conchon, Jean-Christophe Filliatre and Julien Signoles        #
-#                                                                        #
-#  This software is free software; you can redistribute it and/or        #
-#  modify it under the terms of the GNU Library General Public           #
-#  License version 2, with the special exception on linking              #
-#  described in file LICENSE.                                            #
-#                                                                        #
-#  This software is distributed in the hope that it will be useful,      #
-#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
-#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  #
-#                                                                        #
-##########################################################################
-
-# Where to install the binaries
-prefix=/usr/local
-exec_prefix=${prefix}
-BINDIR=${exec_prefix}/bin
-
-# Where to install the man page
-MANDIR=${prefix}/share/man
-
-# Other variables set by ./configure
-OCAMLC   = ocamlc.opt
-OCAMLOPT = ocamlopt.opt
-OCAMLDEP = ocamldep
-OCAMLDOC = ocamldoc.opt
-OCAMLLEX = ocamllex.opt
-OCAMLYACC= ocamlyacc
-OCAMLLIB = /nix/store/547bsyhad0whqa62qkji1q0pfy5lm0qx-ocaml-4.01.0/lib/ocaml
-OCAMLBEST= opt
-OCAMLVERSION = 4.01.0
-OCAMLWEB = true
-OCAMLWIN32 = no
-OCAMLFIND = 
-EXE = 
-LIBEXT = .a
-OBJEXT = .o
-
-# Others global variables
-SRCDIR	= src
-LIBDIR	= lib
-
-INCLUDES= -I $(SRCDIR) -I $(LIBDIR) 
-BFLAGS = $(INCLUDES)
-OFLAGS = $(INCLUDES) -for-pack Graph
-
-# main target
-#############
-
-NAME=ocamlgraph
-
-all: byte $(OCAMLBEST)
-#all: byte $(OCAMLBEST) editor-no
-
-# bytecode and native-code compilation
-######################################
-
-LIB= unionfind heap bitv
-LIB:=$(patsubst %, $(LIBDIR)/%.cmo, $(LIB))
-
-CMO = util blocks persistent imperative \
-	delaunay builder classic rand oper \
-	gpath traverse gcoloring topological components kruskal flow \
-        graphviz gml dot_parser dot_lexer dot pack \
-	gmap minsep cliquetree mcs_m md strat
-CMO := $(LIB) $(patsubst %, $(SRCDIR)/%.cmo, $(CMO))
-
-CMX = $(CMO:.cmo=.cmx)
-CMA = graph.cma
-CMXA = graph.cmxa
-
-CMI = sig dot_ast sig_pack
-CMI := $(patsubst %, src/%.cmi, $(CMI))
-
-GENERATED = META \
-	src/gml.ml src/version.ml \
-	src/dot_parser.ml src/dot_parser.mli src/dot_lexer.ml
-
-byte: $(CMA)
-opt: $(CMXA)
-
-graph.cma: graph.cmo
-	$(OCAMLC) $(INCLUDES) -a -o $@ $^
-
-graph.cmxa: graph.cmx
-	$(OCAMLOPT) $(INCLUDES) -a -o $@ $^
-
-graph.cmo: $(CMI) $(CMO)
-	$(OCAMLC) $(INCLUDES) -pack -o $@ $^
-
-graph.cmx: $(CMI) $(CMX)
-	$(OCAMLOPT) $(INCLUDES) -pack -o $@ $^
-
-EXAMPLESBIN=bin/demo.$(OCAMLBEST) bin/demo_planar.$(OCAMLBEST) \
-  bin/bench.$(OCAMLBEST) bin/color.$(OCAMLBEST) bin/sudoku.$(OCAMLBEST) \
-  bin/test.$(OCAMLBEST) 
-
-.PHONY: examples
-examples: $(EXAMPLESBIN)
-
-.PHONY: demo
-demo: bin/demo.$(OCAMLBEST)
-
-bin/demo.byte: $(CMA) examples/demo.cmo
-	$(OCAMLC) -o $@ $^
-
-bin/demo.opt: $(CMXA) examples/demo.cmx
-	$(OCAMLOPT) -o $@ $^
-
-bin/demo_planar.byte: $(CMA) examples/demo_planar.cmo
-	$(OCAMLC) -o $@ graphics.cma unix.cma $^
-
-bin/demo_planar.opt: $(CMXA) examples/demo_planar.cmx
-	$(OCAMLOPT) -o $@ graphics.cmxa unix.cmxa $^
-
-bin/color.byte: $(CMA) examples/color.cmo
-	$(OCAMLC) -o $@ graphics.cma unix.cma $^
-
-bin/color.opt: $(CMXA) examples/color.cmx
-	$(OCAMLOPT) -o $@ graphics.cmxa unix.cmxa $^
-
-bin/sudoku.byte: $(CMA) examples/sudoku.cmo
-	$(OCAMLC) -o $@ graphics.cma unix.cma $^
-
-bin/sudoku.opt: $(CMXA) examples/sudoku.cmx
-	$(OCAMLOPT) -o $@ graphics.cmxa unix.cmxa $^
-
-test: $(CMA) tests/test.ml
-	ocaml unix.cma graphics.cma $^
-
-bin/test.byte: $(CMA) tests/test.cmo
-	$(OCAMLC) -g -unsafe -o $@ unix.cma graphics.cma $^
-
-bin/test.opt: $(CMXA) tests/test.cmx
-	$(OCAMLOPT) -unsafe -inline 100 -o $@ unix.cmxa graphics.cmxa $^
-
-bench: bin/bench.$(OCAMLBEST)
-	bin/bench.opt
-
-bin/bench.opt: $(CMXA) tests/bench.ml
-	$(OCAMLOPT) -unsafe -inline 100 -o $@ unix.cmxa $^
-
-check: $(CMA) tests/check.ml
-	ocaml $^
-
-# gtk2 graph editor
-
-ED_DIR=editor
-
-editor-no:
-editor-yes: $(ED_DIR)/editor.$(OCAMLBEST)
-
-editor: $(ED_DIR)/editor.byte editor-yes
-
-ED_CMO = ed_hyper ed_graph ed_draw ed_display ed_main
-ED_CMO:= $(patsubst %, $(ED_DIR)/%.cmo, $(ED_CMO))
-ED_CMX = $(ED_CMO:.cmo=.cmx)
-
-ED_INCLUDES =  -I +threads -I $(ED_DIR)
-
-$(ED_CMO): BFLAGS+= $(ED_INCLUDES)
-$(ED_CMX): OFLAGS+= $(ED_INCLUDES)
-
-$(ED_DIR)/editor.byte: $(CMA) $(ED_CMO)
-	$(OCAMLC) -g -o $@  \
-		lablgtk.cma lablgnomecanvas.cma unix.cma $^
-
-$(ED_DIR)/editor.opt: $(CMXA) $(ED_CMX)
-	$(OCAMLOPT) -o $@  \
-		lablgtk.cmxa lablgnomecanvas.cmxa unix.cmxa $^
-
-VERSION=0.99b
-
-src/version.ml: Makefile
-	echo "let version = \""$(VERSION)"\"" > $@
-	echo "let date = \""`date`"\"" >> $@
-
-META: META.in Makefile
-	sed -e s/VERSION/$(VERSION)/ -e s/CMA/$(CMA)/ -e s/CMXA/$(CMXA)/ \
-		$@.in > $@
-
-# Additional rules
-##################
-
-EXAMPLES = demo color demo_planar sudoku
-EXAMPLES:= $(patsubst %, examples/%.ml, $(EXAMPLES))
-
-TESTS = test check
-TESTS := $(patsubst %, tests/%.ml, $(TESTS))
-
-DPD_GRAPH_ML= $(TESTS) $(EXAMPLES)
-
-$(DPD_GRAPH_ML:.ml=.cmo): $(CMA)
-$(DPD_GRAPH_ML:.ml=.cmx): $(CMXA)
-
-# installation
-##############
-
-install: install-$(OCAMLBEST) install-byte
-
-install-byte: 
-	cp -f graph.cmo graph.cmi $(CMA) "$(OCAMLLIB)"
-
-install-opt: install-byte
-	cp -f graph$(LIBEXT) graph.cmx $(CMXA) "$(OCAMLLIB)"
-
-install-findlib: META
-ifdef OCAMLFIND
-	$(OCAMLFIND) install ocamlgraph META *.mli \
-		graph$(LIBEXT) graph.cmx graph.cmo graph.cmi $(CMA) $(CMXA)
-endif
-
-# documentation
-###############
-
-DOCFILES=$(NAME).ps $(NAME).html
-
-NODOC	= util blocks dot_parser dot_lexer
-NODOC	:= $(patsubst %, $(SRCDIR)/%.cmo, $(NODOC))
-DOC_CMO	= $(filter-out $(NODOC) $(LIB), $(CMO))
-DOC_SRC	= $(CMI:.cmi=.mli) $(DOC_CMO:.cmo=.mli) $(DOC_CMO:.cmo=.ml)
-
-.PHONY: doc
-doc: $(DOC_CMO)
-	mkdir -p doc
-	rm -f doc/*
-	$(OCAMLDOC) -d doc -html $(INCLUDES) $(DOC_SRC)
-
-# literate programming
-$(NAME).tex: $(DOC_SRC)
-	$(OCAMLWEB) -o $@ $^
-
-wc:
-	ocamlwc -p $(SRCDIRC)/*.mli $(SRCDIRC)/*.ml
-
-# file headers
-##############
-headers:
-	headache -c misc/headache_config.txt -h misc/header.txt \
-		Makefile.in configure.in README \
-		$(LIBDIR)*.ml $(LIBDIR)*.ml[ily] \
-		$(SRCDIR)*.ml $(SRCDIR)*.ml[ily] \
-		$(ED_DIR)/*.ml $(ED_DIR)/*.mli \
-
-# export
-########
-
-EXPORTDIR=$(NAME)-$(VERSION)
-TAR=$(EXPORTDIR).tar
-
-FTP = $$HOME/ftp/$(NAME)
-WWW = $$HOME/WWW/$(NAME)
-
-FILES = src/*.ml* lib/*.ml* Makefile.in configure configure.in META.in  \
-	.depend editor/ed_*.ml* editor/Makefile \
-        editor/tests/*.dot editor/tests/*.gml \
-	examples/*.ml tests/*.ml \
-	.depend README FAQ CREDITS INSTALL COPYING LICENSE CHANGES
-
-export: source export-doc export-web export-delaunay
-
-source: 
-	mkdir -p export
-	cd export; rm -rf $(EXPORTDIR)
-	mkdir -p export/$(EXPORTDIR)/bin
-	cp --parents $(FILES) export/$(EXPORTDIR)
-	cd export ; tar cf $(TAR) $(EXPORTDIR) ; gzip -f --best $(TAR)
-	cp export/$(TAR).gz $(FTP)
-	cp README FAQ CREDITS COPYING LICENSE CHANGES $(EXAMPLES) $(FTP)
-
-www/version.prehtml: Makefile.in
-	echo "<#def version>$(VERSION)</#def>" > www/version.prehtml
-
-export-web: www/version.prehtml
-	make -C www install
-
-export-doc: $(DOC_CMO)
-	rm -f $(WWW)/doc/*
-	-$(OCAMLDOC) -d $(WWW)/doc -html $(INCLUDES) $(DOC_SRC)
-
-MISCFTP = $(HOME)/WWW/ftp/ocaml/misc
-DELAUNAY=delaunay.ml delaunay.mli
-export-delaunay:
-	cd src; cp -f $(DELAUNAY) $(MISCFTP)
-	cd src; caml2html -d $(MISCFTP) $(DELAUNAY)
-
-# generic rules
-###############
-
-.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .tex .dvi .ps .html
-
-.mli.cmi:
-	$(OCAMLC) -c $(BFLAGS) $<
-
-.ml.cmo:
-	$(OCAMLC) -c $(BFLAGS) $<
-
-.ml.o:
-	$(OCAMLOPT) -c $(OFLAGS) $<
-
-.ml.cmx:
-	$(OCAMLOPT) -c $(OFLAGS) $<
-
-.mll.ml:
-	$(OCAMLLEX) $<
-
-.mly.ml:
-	$(OCAMLYACC) -v $<
-
-.mly.mli:
-	$(OCAMLYACC) -v $<
-
-.tex.dvi:
-	latex $< && latex $<
-
-.dvi.ps:
-	dvips $< -o $@ 
-
-.tex.html:
-	hevea $<
-
-# Emacs tags
-############
-
-otags:
-	otags -r src editor
-
-tags:
-	find . -name "*.ml*" | sort -r | xargs \
-	etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
-	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
-	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
-	      "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
-              "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
-	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
-	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"
-
-# Makefile is rebuilt whenever Makefile.in or configure.in is modified
-######################################################################
-
-Makefile: Makefile.in config.status
-	if test -e $@; then chmod a+w $@; fi		
-	./config.status
-	chmod a-w $@
-
-config.status: configure
-	./config.status --recheck
-
-configure: configure.in
-	autoconf 
-
-# clean
-#######
-
-clean:
-	rm -f *~
-	for d in $(SRCDIR) $(LIBDIR) $(ED_DIR) tests examples; do \
-	  rm -f $$d/*.cm[iox] $$d/*$(OBJEXT) $$d/*~; \
-	done
-	rm -f $(GENERATED) $(SRCDIR)/dot_parser.output
-	rm -f graph.*a graph$(LIBEXT) bin/$(NAME).byte bin/$(NAME).opt
-	rm -f *.haux *.aux *.log $(NAME).tex $(NAME).dvi $(DOCFILES)
-	rm -f $(EXAMPLESBIN)
-
-dist-clean distclean:: clean
-	rm -f Makefile config.cache config.log config.status *.byte *.opt
-
-svnclean svn-clean:: dist-clean
-	rm -f config.* configure configure.lineno
-
-# depend
-########
-
-.PHONY: depend
-.depend depend: $(GENERATED)
-	rm -f .depend
-	$(OCAMLDEP) $(INCLUDES) \
-		$(LIBDIR)/*.ml $(LIBDIR)/*.mli \
-		$(SRCDIR)/*.ml $(SRCDIR)/*.mli \
-		$(ED_DIR)/*.mli $(ED_DIR)/*.ml > .depend
-
-include .depend
diff --git a/external/ocamlgraph/src/dot_lexer.ml b/external/ocamlgraph/src/dot_lexer.ml
deleted file mode 100644
--- a/external/ocamlgraph/src/dot_lexer.ml
+++ /dev/null
@@ -1,386 +0,0 @@
-# 20 "src/dot_lexer.mll"
- 
-  open Lexing
-  open Dot_ast
-  open Dot_parser
-
-  let string_buf = Buffer.create 1024
-
-  let keyword =
-    let h = Hashtbl.create 17 in
-    List.iter 
-      (fun (s,k) -> Hashtbl.add h s k)
-      [
-	"strict", STRICT;
-	"graph", GRAPH;
-	"digraph", DIGRAPH;
-	"subgraph", SUBGRAPH;
-	"node", NODE;
-	"edge", EDGE;
-      ];
-    fun s -> let s = String.lowercase s in Hashtbl.find h s
-
-
-# 25 "src/dot_lexer.ml"
-let __ocaml_lex_tables = {
-  Lexing.lex_base = 
-   "\000\000\238\255\239\255\240\255\241\255\078\000\088\000\098\000\
-    \176\000\245\255\246\255\247\255\248\255\249\255\250\255\251\255\
-    \252\255\114\000\001\000\005\000\254\255\002\000\253\255\191\000\
-    \244\255\211\000\221\000\157\000\252\255\253\255\002\000\255\255\
-    \254\255\032\000\252\255\253\255\254\255\255\255\054\000\253\255\
-    \254\255\015\000\255\255";
-  Lexing.lex_backtrk = 
-   "\255\255\255\255\255\255\255\255\255\255\013\000\017\000\012\000\
-    \017\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\017\000\017\000\000\000\255\255\255\255\255\255\255\255\
-    \255\255\013\000\013\000\255\255\255\255\255\255\002\000\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\001\000\255\255";
-  Lexing.lex_default = 
-   "\001\000\000\000\000\000\000\000\000\000\255\255\255\255\255\255\
-    \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\255\255\021\000\255\255\000\000\021\000\000\000\255\255\
-    \000\000\255\255\255\255\029\000\000\000\000\000\255\255\000\000\
-    \000\000\035\000\000\000\000\000\000\000\000\000\040\000\000\000\
-    \000\000\255\255\000\000";
-  Lexing.lex_trans = 
-   "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\019\000\019\000\020\000\020\000\019\000\019\000\019\000\
-    \000\000\000\000\019\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \019\000\000\000\004\000\018\000\032\000\019\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\015\000\008\000\006\000\017\000\
-    \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\
-    \005\000\005\000\016\000\014\000\003\000\013\000\042\000\000\000\
-    \000\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\010\000\036\000\009\000\037\000\007\000\
-    \041\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\012\000\026\000\011\000\005\000\005\000\
-    \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\
-    \025\000\025\000\025\000\025\000\025\000\025\000\025\000\025\000\
-    \025\000\025\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\022\000\000\000\000\000\000\000\
-    \000\000\021\000\000\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\000\000\000\000\031\000\
-    \000\000\007\000\000\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\024\000\023\000\000\000\
-    \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\
-    \005\000\005\000\000\000\000\000\000\000\000\000\024\000\025\000\
-    \025\000\025\000\025\000\025\000\025\000\025\000\025\000\025\000\
-    \025\000\030\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \002\000\255\255\255\255\025\000\025\000\025\000\025\000\025\000\
-    \025\000\025\000\025\000\025\000\025\000\026\000\026\000\026\000\
-    \026\000\026\000\026\000\026\000\026\000\026\000\026\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \034\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\039\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\028\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000";
-  Lexing.lex_check = 
-   "\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\000\000\000\000\018\000\021\000\000\000\019\000\019\000\
-    \255\255\255\255\019\000\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \000\000\255\255\000\000\000\000\030\000\019\000\255\255\255\255\
-    \255\255\255\255\255\255\255\255\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\041\000\255\255\
-    \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\033\000\000\000\033\000\000\000\
-    \038\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\005\000\000\000\005\000\005\000\
-    \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\017\000\255\255\255\255\255\255\
-    \255\255\017\000\255\255\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\255\255\255\255\027\000\
-    \255\255\007\000\255\255\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\008\000\008\000\255\255\
-    \008\000\008\000\008\000\008\000\008\000\008\000\008\000\008\000\
-    \008\000\008\000\255\255\255\255\255\255\255\255\008\000\023\000\
-    \023\000\023\000\023\000\023\000\023\000\023\000\023\000\023\000\
-    \023\000\027\000\255\255\255\255\255\255\255\255\255\255\255\255\
-    \000\000\018\000\021\000\025\000\025\000\025\000\025\000\025\000\
-    \025\000\025\000\025\000\025\000\025\000\026\000\026\000\026\000\
-    \026\000\026\000\026\000\026\000\026\000\026\000\026\000\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \033\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\038\000\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\027\000\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255";
-  Lexing.lex_base_code = 
-   "";
-  Lexing.lex_backtrk_code = 
-   "";
-  Lexing.lex_default_code = 
-   "";
-  Lexing.lex_trans_code = 
-   "";
-  Lexing.lex_check_code = 
-   "";
-  Lexing.lex_code = 
-   "";
-}
-
-let rec token lexbuf =
-    __ocaml_lex_token_rec lexbuf 0
-and __ocaml_lex_token_rec lexbuf __ocaml_lex_state =
-  match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with
-      | 0 ->
-# 52 "src/dot_lexer.mll"
-      ( token lexbuf )
-# 191 "src/dot_lexer.ml"
-
-  | 1 ->
-# 54 "src/dot_lexer.mll"
-      ( token lexbuf )
-# 196 "src/dot_lexer.ml"
-
-  | 2 ->
-# 56 "src/dot_lexer.mll"
-      ( comment lexbuf; token lexbuf )
-# 201 "src/dot_lexer.ml"
-
-  | 3 ->
-# 58 "src/dot_lexer.mll"
-      ( COLON )
-# 206 "src/dot_lexer.ml"
-
-  | 4 ->
-# 60 "src/dot_lexer.mll"
-      ( COMMA )
-# 211 "src/dot_lexer.ml"
-
-  | 5 ->
-# 62 "src/dot_lexer.mll"
-      ( SEMICOLON )
-# 216 "src/dot_lexer.ml"
-
-  | 6 ->
-# 64 "src/dot_lexer.mll"
-      ( EQUAL )
-# 221 "src/dot_lexer.ml"
-
-  | 7 ->
-# 66 "src/dot_lexer.mll"
-      ( LBRA )
-# 226 "src/dot_lexer.ml"
-
-  | 8 ->
-# 68 "src/dot_lexer.mll"
-      ( RBRA )
-# 231 "src/dot_lexer.ml"
-
-  | 9 ->
-# 70 "src/dot_lexer.mll"
-      ( LSQ )
-# 236 "src/dot_lexer.ml"
-
-  | 10 ->
-# 72 "src/dot_lexer.mll"
-      ( RSQ )
-# 241 "src/dot_lexer.ml"
-
-  | 11 ->
-# 74 "src/dot_lexer.mll"
-      ( EDGEOP )
-# 246 "src/dot_lexer.ml"
-
-  | 12 ->
-let
-# 75 "src/dot_lexer.mll"
-             s
-# 252 "src/dot_lexer.ml"
-= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in
-# 76 "src/dot_lexer.mll"
-      ( try keyword s with Not_found -> ID (Ident s) )
-# 256 "src/dot_lexer.ml"
-
-  | 13 ->
-let
-# 77 "src/dot_lexer.mll"
-              s
-# 262 "src/dot_lexer.ml"
-= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in
-# 78 "src/dot_lexer.mll"
-      ( ID (Number s) )
-# 266 "src/dot_lexer.ml"
-
-  | 14 ->
-# 80 "src/dot_lexer.mll"
-      ( Buffer.clear string_buf; 
-	let s = string lexbuf in
-	ID (String s) )
-# 273 "src/dot_lexer.ml"
-
-  | 15 ->
-# 84 "src/dot_lexer.mll"
-      ( Buffer.clear string_buf; 
-	html lexbuf; 
-	ID (Html (Buffer.contents string_buf)) )
-# 280 "src/dot_lexer.ml"
-
-  | 16 ->
-# 88 "src/dot_lexer.mll"
-      ( EOF )
-# 285 "src/dot_lexer.ml"
-
-  | 17 ->
-let
-# 89 "src/dot_lexer.mll"
-         c
-# 291 "src/dot_lexer.ml"
-= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in
-# 90 "src/dot_lexer.mll"
-      ( failwith ("Dot_lexer: invalid character " ^ String.make 1 c) )
-# 295 "src/dot_lexer.ml"
-
-  | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_token_rec lexbuf __ocaml_lex_state
-
-and string lexbuf =
-    __ocaml_lex_string_rec lexbuf 27
-and __ocaml_lex_string_rec lexbuf __ocaml_lex_state =
-  match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with
-      | 0 ->
-# 94 "src/dot_lexer.mll"
-      ( Buffer.contents string_buf )
-# 306 "src/dot_lexer.ml"
-
-  | 1 ->
-# 96 "src/dot_lexer.mll"
-      ( Buffer.add_char string_buf '"';
-	string lexbuf )
-# 312 "src/dot_lexer.ml"
-
-  | 2 ->
-let
-# 98 "src/dot_lexer.mll"
-         c
-# 318 "src/dot_lexer.ml"
-= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in
-# 99 "src/dot_lexer.mll"
-      ( Buffer.add_char string_buf c;
-	string lexbuf )
-# 323 "src/dot_lexer.ml"
-
-  | 3 ->
-# 102 "src/dot_lexer.mll"
-      ( failwith ("Dot_lexer: unterminated string literal") )
-# 328 "src/dot_lexer.ml"
-
-  | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_string_rec lexbuf __ocaml_lex_state
-
-and html lexbuf =
-    __ocaml_lex_html_rec lexbuf 33
-and __ocaml_lex_html_rec lexbuf __ocaml_lex_state =
-  match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with
-      | 0 ->
-# 106 "src/dot_lexer.mll"
-      ( () )
-# 339 "src/dot_lexer.ml"
-
-  | 1 ->
-# 108 "src/dot_lexer.mll"
-      ( Buffer.add_char string_buf '<'; html lexbuf;
-	Buffer.add_char string_buf '>'; html lexbuf )
-# 345 "src/dot_lexer.ml"
-
-  | 2 ->
-let
-# 110 "src/dot_lexer.mll"
-         c
-# 351 "src/dot_lexer.ml"
-= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in
-# 111 "src/dot_lexer.mll"
-      ( Buffer.add_char string_buf c;
-	html lexbuf )
-# 356 "src/dot_lexer.ml"
-
-  | 3 ->
-# 114 "src/dot_lexer.mll"
-      ( failwith ("Dot_lexer: unterminated html literal") )
-# 361 "src/dot_lexer.ml"
-
-  | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_html_rec lexbuf __ocaml_lex_state
-
-and comment lexbuf =
-    __ocaml_lex_comment_rec lexbuf 38
-and __ocaml_lex_comment_rec lexbuf __ocaml_lex_state =
-  match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with
-      | 0 ->
-# 118 "src/dot_lexer.mll"
-      ( () )
-# 372 "src/dot_lexer.ml"
-
-  | 1 ->
-# 120 "src/dot_lexer.mll"
-      ( comment lexbuf )
-# 377 "src/dot_lexer.ml"
-
-  | 2 ->
-# 122 "src/dot_lexer.mll"
-      ( failwith "Dot_lexer: unterminated comment" )
-# 382 "src/dot_lexer.ml"
-
-  | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_comment_rec lexbuf __ocaml_lex_state
-
-;;
-
diff --git a/external/ocamlgraph/src/dot_parser.ml b/external/ocamlgraph/src/dot_parser.ml
deleted file mode 100644
--- a/external/ocamlgraph/src/dot_parser.ml
+++ /dev/null
@@ -1,552 +0,0 @@
-type token =
-  | ID of (Dot_ast.id)
-  | COLON
-  | COMMA
-  | EQUAL
-  | SEMICOLON
-  | EDGEOP
-  | STRICT
-  | GRAPH
-  | DIGRAPH
-  | LBRA
-  | RBRA
-  | LSQ
-  | RSQ
-  | NODE
-  | EDGE
-  | SUBGRAPH
-  | EOF
-
-open Parsing;;
-let _ = parse_error;;
-# 23 "src/dot_parser.mly"
-  open Dot_ast
-  open Parsing
-
-  let compass_pt = function
-    | Ident "n" -> N
-    | Ident "ne" -> Ne
-    | Ident "e" -> E
-    | Ident "se" -> Se
-    | Ident "s" -> S
-    | Ident "sw" -> Sw
-    | Ident "w" -> W
-    | Ident "nw" -> Nw
-    | _ -> invalid_arg "compass_pt"
-
-# 38 "src/dot_parser.ml"
-let yytransl_const = [|
-  258 (* COLON *);
-  259 (* COMMA *);
-  260 (* EQUAL *);
-  261 (* SEMICOLON *);
-  262 (* EDGEOP *);
-  263 (* STRICT *);
-  264 (* GRAPH *);
-  265 (* DIGRAPH *);
-  266 (* LBRA *);
-  267 (* RBRA *);
-  268 (* LSQ *);
-  269 (* RSQ *);
-  270 (* NODE *);
-  271 (* EDGE *);
-  272 (* SUBGRAPH *);
-    0 (* EOF *);
-    0|]
-
-let yytransl_block = [|
-  257 (* ID *);
-    0|]
-
-let yylhs = "\255\255\
-\001\000\002\000\002\000\003\000\003\000\005\000\005\000\006\000\
-\006\000\008\000\008\000\007\000\007\000\007\000\007\000\007\000\
-\009\000\010\000\011\000\011\000\011\000\016\000\018\000\018\000\
-\015\000\015\000\013\000\019\000\019\000\020\000\020\000\014\000\
-\014\000\017\000\017\000\004\000\004\000\021\000\021\000\022\000\
-\022\000\023\000\023\000\012\000\012\000\012\000\012\000\000\000"
-
-let yylen = "\002\000\
-\007\000\000\000\001\000\001\000\001\000\000\000\001\000\002\000\
-\003\000\000\000\001\000\001\000\001\000\001\000\003\000\001\000\
-\002\000\003\000\002\000\002\000\002\000\003\000\000\000\003\000\
-\001\000\001\000\002\000\000\000\001\000\002\000\004\000\000\000\
-\001\000\003\000\004\000\000\000\001\000\002\000\003\000\001\000\
-\003\000\000\000\001\000\002\000\005\000\004\000\003\000\002\000"
-
-let yydefred = "\000\000\
-\000\000\000\000\003\000\048\000\000\000\004\000\005\000\000\000\
-\037\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\000\000\000\000\007\000\000\000\012\000\013\000\014\000\000\000\
-\000\000\000\000\000\000\000\000\027\000\029\000\000\000\019\000\
-\000\000\020\000\021\000\000\000\000\000\000\000\011\000\000\000\
-\017\000\033\000\000\000\000\000\000\000\015\000\000\000\000\000\
-\000\000\047\000\000\000\000\000\001\000\009\000\000\000\026\000\
-\025\000\000\000\018\000\000\000\000\000\000\000\043\000\000\000\
-\000\000\046\000\000\000\022\000\031\000\041\000\035\000\039\000\
-\045\000\000\000\024\000"
-
-let yydgoto = "\002\000\
-\004\000\005\000\008\000\010\000\018\000\019\000\020\000\040\000\
-\021\000\022\000\023\000\024\000\025\000\041\000\026\000\044\000\
-\042\000\068\000\029\000\030\000\048\000\049\000\064\000"
-
-let yysindex = "\009\000\
-\024\255\000\000\000\000\000\000\000\255\000\000\000\000\031\255\
-\000\000\029\255\131\255\011\255\033\255\131\255\033\255\033\255\
-\051\255\040\255\000\000\048\255\000\000\000\000\000\000\000\000\
-\033\255\050\255\057\255\067\255\000\000\000\000\069\255\000\000\
-\062\255\000\000\000\000\070\255\131\255\091\000\000\000\131\255\
-\000\000\000\000\018\255\033\255\090\255\000\000\099\255\081\255\
-\101\255\000\000\131\255\095\255\000\000\000\000\107\255\000\000\
-\000\000\110\255\000\000\114\255\117\255\033\255\000\000\069\255\
-\111\255\000\000\018\255\000\000\000\000\000\000\000\000\000\000\
-\000\000\110\255\000\000"
-
-let yyrindex = "\000\000\
-\074\255\000\000\000\000\000\000\000\000\000\000\000\000\116\255\
-\000\000\000\000\118\255\006\255\000\000\118\255\000\000\000\000\
-\000\000\000\000\000\000\120\255\000\000\000\000\000\000\049\255\
-\061\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\000\000\000\000\000\000\073\255\118\255\000\000\000\000\122\255\
-\000\000\000\000\000\000\097\255\032\255\000\000\023\255\000\000\
-\022\255\000\000\118\255\000\000\000\000\000\000\006\255\000\000\
-\000\000\085\255\000\000\000\000\000\000\109\255\000\000\124\255\
-\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-\000\000\085\255\000\000"
-
-let yygindex = "\000\000\
-\000\000\000\000\000\000\000\000\246\255\087\000\000\000\000\000\
-\000\000\000\000\000\000\214\255\218\255\094\000\219\255\000\000\
-\243\255\066\000\000\000\000\000\078\000\000\000\000\000"
-
-let yytablesize = 147
-let yytable = "\032\000\
-\056\000\034\000\035\000\033\000\057\000\058\000\028\000\006\000\
-\007\000\001\000\028\000\028\000\027\000\028\000\028\000\028\000\
-\028\000\028\000\055\000\028\000\028\000\028\000\042\000\040\000\
-\056\000\040\000\052\000\014\000\057\000\074\000\003\000\009\000\
-\030\000\017\000\042\000\040\000\030\000\030\000\011\000\030\000\
-\065\000\030\000\030\000\030\000\031\000\030\000\030\000\030\000\
-\071\000\016\000\038\000\036\000\039\000\016\000\026\000\043\000\
-\016\000\045\000\016\000\016\000\037\000\032\000\016\000\016\000\
-\016\000\032\000\025\000\046\000\032\000\047\000\032\000\032\000\
-\050\000\044\000\032\000\032\000\032\000\044\000\044\000\051\000\
-\044\000\002\000\002\000\044\000\044\000\023\000\044\000\044\000\
-\044\000\023\000\053\000\060\000\023\000\062\000\023\000\023\000\
-\023\000\032\000\023\000\023\000\023\000\032\000\061\000\063\000\
-\032\000\066\000\032\000\032\000\027\000\034\000\032\000\032\000\
-\032\000\034\000\069\000\067\000\034\000\070\000\034\000\034\000\
-\010\000\073\000\034\000\034\000\034\000\036\000\054\000\010\000\
-\006\000\010\000\010\000\012\000\008\000\010\000\010\000\010\000\
-\038\000\059\000\013\000\075\000\014\000\072\000\000\000\000\000\
-\015\000\016\000\017\000"
-
-let yycheck = "\013\000\
-\043\000\015\000\016\000\014\000\043\000\043\000\001\001\008\001\
-\009\001\001\000\005\001\006\001\002\001\008\001\004\001\010\001\
-\011\001\012\001\001\001\014\001\015\001\016\001\001\001\001\001\
-\067\000\003\001\037\000\010\001\067\000\067\000\007\001\001\001\
-\001\001\016\001\013\001\013\001\005\001\006\001\010\001\008\001\
-\051\000\010\001\011\001\012\001\012\001\014\001\015\001\016\001\
-\062\000\001\001\011\001\001\001\005\001\005\001\006\001\006\001\
-\008\001\001\001\010\001\011\001\010\001\001\001\014\001\015\001\
-\016\001\005\001\006\001\001\001\008\001\001\001\010\001\011\001\
-\011\001\001\001\014\001\015\001\016\001\005\001\006\001\010\001\
-\008\001\008\001\009\001\011\001\012\001\001\001\014\001\015\001\
-\016\001\005\001\000\000\002\001\008\001\013\001\010\001\011\001\
-\012\001\001\001\014\001\015\001\016\001\005\001\004\001\003\001\
-\008\001\011\001\010\001\011\001\002\001\001\001\014\001\015\001\
-\016\001\005\001\001\001\006\001\008\001\001\001\010\001\011\001\
-\001\001\011\001\014\001\015\001\016\001\010\001\040\000\008\001\
-\011\001\010\001\011\001\001\001\011\001\014\001\015\001\016\001\
-\013\001\044\000\008\001\074\000\010\001\064\000\255\255\255\255\
-\014\001\015\001\016\001"
-
-let yynames_const = "\
-  COLON\000\
-  COMMA\000\
-  EQUAL\000\
-  SEMICOLON\000\
-  EDGEOP\000\
-  STRICT\000\
-  GRAPH\000\
-  DIGRAPH\000\
-  LBRA\000\
-  RBRA\000\
-  LSQ\000\
-  RSQ\000\
-  NODE\000\
-  EDGE\000\
-  SUBGRAPH\000\
-  EOF\000\
-  "
-
-let yynames_block = "\
-  ID\000\
-  "
-
-let yyact = [|
-  (fun _ -> failwith "parser")
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 6 : 'strict_opt) in
-    let _2 = (Parsing.peek_val __caml_parser_env 5 : 'graph_or_digraph) in
-    let _3 = (Parsing.peek_val __caml_parser_env 4 : 'id_opt) in
-    let _5 = (Parsing.peek_val __caml_parser_env 2 : 'stmt_list) in
-    Obj.repr(
-# 49 "src/dot_parser.mly"
-    ( { strict = _1; digraph = _2; id = _3; stmts = _5 } )
-# 200 "src/dot_parser.ml"
-               : Dot_ast.file))
-; (fun __caml_parser_env ->
-    Obj.repr(
-# 53 "src/dot_parser.mly"
-                ( false )
-# 206 "src/dot_parser.ml"
-               : 'strict_opt))
-; (fun __caml_parser_env ->
-    Obj.repr(
-# 54 "src/dot_parser.mly"
-                ( true )
-# 212 "src/dot_parser.ml"
-               : 'strict_opt))
-; (fun __caml_parser_env ->
-    Obj.repr(
-# 58 "src/dot_parser.mly"
-          ( false )
-# 218 "src/dot_parser.ml"
-               : 'graph_or_digraph))
-; (fun __caml_parser_env ->
-    Obj.repr(
-# 59 "src/dot_parser.mly"
-          ( true )
-# 224 "src/dot_parser.ml"
-               : 'graph_or_digraph))
-; (fun __caml_parser_env ->
-    Obj.repr(
-# 63 "src/dot_parser.mly"
-                ( [] )
-# 230 "src/dot_parser.ml"
-               : 'stmt_list))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 0 : 'list1_stmt) in
-    Obj.repr(
-# 64 "src/dot_parser.mly"
-                ( _1 )
-# 237 "src/dot_parser.ml"
-               : 'stmt_list))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 1 : 'stmt) in
-    let _2 = (Parsing.peek_val __caml_parser_env 0 : 'semicolon_opt) in
-    Obj.repr(
-# 68 "src/dot_parser.mly"
-                     ( [_1] )
-# 245 "src/dot_parser.ml"
-               : 'list1_stmt))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 2 : 'stmt) in
-    let _2 = (Parsing.peek_val __caml_parser_env 1 : 'semicolon_opt) in
-    let _3 = (Parsing.peek_val __caml_parser_env 0 : 'list1_stmt) in
-    Obj.repr(
-# 69 "src/dot_parser.mly"
-                                ( _1 :: _3 )
-# 254 "src/dot_parser.ml"
-               : 'list1_stmt))
-; (fun __caml_parser_env ->
-    Obj.repr(
-# 73 "src/dot_parser.mly"
-                ( () )
-# 260 "src/dot_parser.ml"
-               : 'semicolon_opt))
-; (fun __caml_parser_env ->
-    Obj.repr(
-# 74 "src/dot_parser.mly"
-                ( () )
-# 266 "src/dot_parser.ml"
-               : 'semicolon_opt))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 0 : 'node_stmt) in
-    Obj.repr(
-# 78 "src/dot_parser.mly"
-            ( _1 )
-# 273 "src/dot_parser.ml"
-               : 'stmt))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 0 : 'edge_stmt) in
-    Obj.repr(
-# 79 "src/dot_parser.mly"
-            ( _1 )
-# 280 "src/dot_parser.ml"
-               : 'stmt))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 0 : 'attr_stmt) in
-    Obj.repr(
-# 80 "src/dot_parser.mly"
-            ( _1 )
-# 287 "src/dot_parser.ml"
-               : 'stmt))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 2 : Dot_ast.id) in
-    let _3 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in
-    Obj.repr(
-# 81 "src/dot_parser.mly"
-              ( Equal (_1, _3) )
-# 295 "src/dot_parser.ml"
-               : 'stmt))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 0 : 'subgraph) in
-    Obj.repr(
-# 82 "src/dot_parser.mly"
-            ( Subgraph _1 )
-# 302 "src/dot_parser.ml"
-               : 'stmt))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 1 : 'node_id) in
-    let _2 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list_opt) in
-    Obj.repr(
-# 86 "src/dot_parser.mly"
-                        ( Node_stmt (_1, _2) )
-# 310 "src/dot_parser.ml"
-               : 'node_stmt))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 2 : 'node) in
-    let _2 = (Parsing.peek_val __caml_parser_env 1 : 'edge_rhs) in
-    let _3 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list_opt) in
-    Obj.repr(
-# 90 "src/dot_parser.mly"
-                              ( Edge_stmt (_1, _2, _3) )
-# 319 "src/dot_parser.ml"
-               : 'edge_stmt))
-; (fun __caml_parser_env ->
-    let _2 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in
-    Obj.repr(
-# 94 "src/dot_parser.mly"
-                  ( Attr_graph _2 )
-# 326 "src/dot_parser.ml"
-               : 'attr_stmt))
-; (fun __caml_parser_env ->
-    let _2 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in
-    Obj.repr(
-# 95 "src/dot_parser.mly"
-                  ( Attr_node _2 )
-# 333 "src/dot_parser.ml"
-               : 'attr_stmt))
-; (fun __caml_parser_env ->
-    let _2 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in
-    Obj.repr(
-# 96 "src/dot_parser.mly"
-                  ( Attr_edge _2 )
-# 340 "src/dot_parser.ml"
-               : 'attr_stmt))
-; (fun __caml_parser_env ->
-    let _2 = (Parsing.peek_val __caml_parser_env 1 : 'node) in
-    let _3 = (Parsing.peek_val __caml_parser_env 0 : 'edge_rhs_opt) in
-    Obj.repr(
-# 100 "src/dot_parser.mly"
-                           ( _2 :: _3 )
-# 348 "src/dot_parser.ml"
-               : 'edge_rhs))
-; (fun __caml_parser_env ->
-    Obj.repr(
-# 104 "src/dot_parser.mly"
-                ( [] )
-# 354 "src/dot_parser.ml"
-               : 'edge_rhs_opt))
-; (fun __caml_parser_env ->
-    let _2 = (Parsing.peek_val __caml_parser_env 1 : 'node) in
-    let _3 = (Parsing.peek_val __caml_parser_env 0 : 'edge_rhs_opt) in
-    Obj.repr(
-# 105 "src/dot_parser.mly"
-                           ( _2 :: _3 )
-# 362 "src/dot_parser.ml"
-               : 'edge_rhs_opt))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 0 : 'node_id) in
-    Obj.repr(
-# 109 "src/dot_parser.mly"
-           ( NodeId _1 )
-# 369 "src/dot_parser.ml"
-               : 'node))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 0 : 'subgraph) in
-    Obj.repr(
-# 110 "src/dot_parser.mly"
-           ( NodeSub _1 )
-# 376 "src/dot_parser.ml"
-               : 'node))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 1 : Dot_ast.id) in
-    let _2 = (Parsing.peek_val __caml_parser_env 0 : 'port_opt) in
-    Obj.repr(
-# 114 "src/dot_parser.mly"
-              ( _1, _2 )
-# 384 "src/dot_parser.ml"
-               : 'node_id))
-; (fun __caml_parser_env ->
-    Obj.repr(
-# 118 "src/dot_parser.mly"
-                ( None )
-# 390 "src/dot_parser.ml"
-               : 'port_opt))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 0 : 'port) in
-    Obj.repr(
-# 119 "src/dot_parser.mly"
-                ( Some _1 )
-# 397 "src/dot_parser.ml"
-               : 'port_opt))
-; (fun __caml_parser_env ->
-    let _2 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in
-    Obj.repr(
-# 123 "src/dot_parser.mly"
-           ( try PortC (compass_pt _2)
-             with Invalid_argument _ -> PortId (_2, None) )
-# 405 "src/dot_parser.ml"
-               : 'port))
-; (fun __caml_parser_env ->
-    let _2 = (Parsing.peek_val __caml_parser_env 2 : Dot_ast.id) in
-    let _4 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in
-    Obj.repr(
-# 126 "src/dot_parser.mly"
-      ( let cp = 
-  	  try compass_pt _4 with Invalid_argument _ -> raise Parse_error 
-	in
-	PortId (_2, Some cp) )
-# 416 "src/dot_parser.ml"
-               : 'port))
-; (fun __caml_parser_env ->
-    Obj.repr(
-# 133 "src/dot_parser.mly"
-                ( [] )
-# 422 "src/dot_parser.ml"
-               : 'attr_list_opt))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in
-    Obj.repr(
-# 134 "src/dot_parser.mly"
-               ( _1 )
-# 429 "src/dot_parser.ml"
-               : 'attr_list_opt))
-; (fun __caml_parser_env ->
-    let _2 = (Parsing.peek_val __caml_parser_env 1 : 'a_list) in
-    Obj.repr(
-# 138 "src/dot_parser.mly"
-                 ( [_2] )
-# 436 "src/dot_parser.ml"
-               : 'attr_list))
-; (fun __caml_parser_env ->
-    let _2 = (Parsing.peek_val __caml_parser_env 2 : 'a_list) in
-    let _4 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in
-    Obj.repr(
-# 139 "src/dot_parser.mly"
-                           ( _2 :: _4 )
-# 444 "src/dot_parser.ml"
-               : 'attr_list))
-; (fun __caml_parser_env ->
-    Obj.repr(
-# 143 "src/dot_parser.mly"
-                ( None )
-# 450 "src/dot_parser.ml"
-               : 'id_opt))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in
-    Obj.repr(
-# 144 "src/dot_parser.mly"
-                ( Some _1 )
-# 457 "src/dot_parser.ml"
-               : 'id_opt))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 1 : 'equality) in
-    let _2 = (Parsing.peek_val __caml_parser_env 0 : 'comma_opt) in
-    Obj.repr(
-# 148 "src/dot_parser.mly"
-                     ( [_1] )
-# 465 "src/dot_parser.ml"
-               : 'a_list))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 2 : 'equality) in
-    let _2 = (Parsing.peek_val __caml_parser_env 1 : 'comma_opt) in
-    let _3 = (Parsing.peek_val __caml_parser_env 0 : 'a_list) in
-    Obj.repr(
-# 149 "src/dot_parser.mly"
-                            ( _1 :: _3 )
-# 474 "src/dot_parser.ml"
-               : 'a_list))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in
-    Obj.repr(
-# 153 "src/dot_parser.mly"
-     ( _1, None )
-# 481 "src/dot_parser.ml"
-               : 'equality))
-; (fun __caml_parser_env ->
-    let _1 = (Parsing.peek_val __caml_parser_env 2 : Dot_ast.id) in
-    let _3 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in
-    Obj.repr(
-# 154 "src/dot_parser.mly"
-              ( _1, Some _3 )
-# 489 "src/dot_parser.ml"
-               : 'equality))
-; (fun __caml_parser_env ->
-    Obj.repr(
-# 158 "src/dot_parser.mly"
-                ( () )
-# 495 "src/dot_parser.ml"
-               : 'comma_opt))
-; (fun __caml_parser_env ->
-    Obj.repr(
-# 159 "src/dot_parser.mly"
-                ( () )
-# 501 "src/dot_parser.ml"
-               : 'comma_opt))
-; (fun __caml_parser_env ->
-    let _2 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in
-    Obj.repr(
-# 164 "src/dot_parser.mly"
-              ( SubgraphId _2 )
-# 508 "src/dot_parser.ml"
-               : 'subgraph))
-; (fun __caml_parser_env ->
-    let _2 = (Parsing.peek_val __caml_parser_env 3 : Dot_ast.id) in
-    let _4 = (Parsing.peek_val __caml_parser_env 1 : 'stmt_list) in
-    Obj.repr(
-# 165 "src/dot_parser.mly"
-                                  ( SubgraphDef (Some _2, _4) )
-# 516 "src/dot_parser.ml"
-               : 'subgraph))
-; (fun __caml_parser_env ->
-    let _3 = (Parsing.peek_val __caml_parser_env 1 : 'stmt_list) in
-    Obj.repr(
-# 166 "src/dot_parser.mly"
-                               ( SubgraphDef (None, _3) )
-# 523 "src/dot_parser.ml"
-               : 'subgraph))
-; (fun __caml_parser_env ->
-    let _2 = (Parsing.peek_val __caml_parser_env 1 : 'stmt_list) in
-    Obj.repr(
-# 167 "src/dot_parser.mly"
-                      ( SubgraphDef (None, _2) )
-# 530 "src/dot_parser.ml"
-               : 'subgraph))
-(* Entry file *)
-; (fun __caml_parser_env -> raise (Parsing.YYexit (Parsing.peek_val __caml_parser_env 0)))
-|]
-let yytables =
-  { Parsing.actions=yyact;
-    Parsing.transl_const=yytransl_const;
-    Parsing.transl_block=yytransl_block;
-    Parsing.lhs=yylhs;
-    Parsing.len=yylen;
-    Parsing.defred=yydefred;
-    Parsing.dgoto=yydgoto;
-    Parsing.sindex=yysindex;
-    Parsing.rindex=yyrindex;
-    Parsing.gindex=yygindex;
-    Parsing.tablesize=yytablesize;
-    Parsing.table=yytable;
-    Parsing.check=yycheck;
-    Parsing.error_function=parse_error;
-    Parsing.names_const=yynames_const;
-    Parsing.names_block=yynames_block }
-let file (lexfun : Lexing.lexbuf -> token) (lexbuf : Lexing.lexbuf) =
-   (Parsing.yyparse yytables 1 lexfun lexbuf : Dot_ast.file)
diff --git a/external/ocamlgraph/src/dot_parser.mli b/external/ocamlgraph/src/dot_parser.mli
deleted file mode 100644
--- a/external/ocamlgraph/src/dot_parser.mli
+++ /dev/null
@@ -1,21 +0,0 @@
-type token =
-  | ID of (Dot_ast.id)
-  | COLON
-  | COMMA
-  | EQUAL
-  | SEMICOLON
-  | EDGEOP
-  | STRICT
-  | GRAPH
-  | DIGRAPH
-  | LBRA
-  | RBRA
-  | LSQ
-  | RSQ
-  | NODE
-  | EDGE
-  | SUBGRAPH
-  | EOF
-
-val file :
-  (Lexing.lexbuf  -> token) -> Lexing.lexbuf -> Dot_ast.file
diff --git a/external/ocamlgraph/src/gml.ml b/external/ocamlgraph/src/gml.ml
deleted file mode 100644
--- a/external/ocamlgraph/src/gml.ml
+++ /dev/null
@@ -1,670 +0,0 @@
-# 20 "src/gml.mll"
-  
-
-  open Lexing
-
-  type value = 
-    | Int of int 
-    | Float of float
-    | String of string
-    | List of value_list
-
-  and value_list = (string * value) list
-
-
-# 16 "src/gml.ml"
-let __ocaml_lex_tables = {
-  Lexing.lex_base = 
-   "\000\000\252\255\253\255\114\000\002\000\007\000\228\000\086\001\
-    \252\255\253\255\200\001\009\000\014\000\058\002\002\000\251\255\
-    \252\255\001\000\080\000\102\000\194\000\216\000\052\001\071\001\
-    \253\255\006\000";
-  Lexing.lex_backtrk = 
-   "\255\255\255\255\255\255\003\000\000\000\001\000\255\255\255\255\
-    \255\255\255\255\003\000\000\000\001\000\255\255\255\255\255\255\
-    \255\255\004\000\001\000\000\000\004\000\255\255\001\000\255\255\
-    \255\255\255\255";
-  Lexing.lex_default = 
-   "\001\000\000\000\000\000\255\255\255\255\255\255\255\255\008\000\
-    \000\000\000\000\255\255\255\255\255\255\255\255\015\000\000\000\
-    \000\000\025\000\255\255\255\255\255\255\255\255\255\255\255\255\
-    \000\000\025\000";
-  Lexing.lex_trans = 
-   "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\004\000\004\000\004\000\004\000\004\000\000\000\004\000\
-    \005\000\005\000\011\000\011\000\005\000\000\000\011\000\012\000\
-    \012\000\000\000\000\000\012\000\000\000\000\000\000\000\000\000\
-    \004\000\000\000\004\000\024\000\017\000\000\000\000\000\005\000\
-    \024\000\011\000\000\000\000\000\000\000\020\000\012\000\020\000\
-    \018\000\000\000\019\000\019\000\019\000\019\000\019\000\019\000\
-    \019\000\019\000\019\000\019\000\000\000\000\000\000\000\000\000\
-    \000\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\000\000\000\000\016\000\000\000\000\000\
-    \000\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\005\000\005\000\000\000\000\000\005\000\
-    \018\000\018\000\018\000\018\000\018\000\018\000\018\000\018\000\
-    \018\000\018\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\005\000\000\000\018\000\021\000\019\000\019\000\
-    \019\000\019\000\019\000\019\000\019\000\019\000\019\000\019\000\
-    \000\000\000\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\005\000\005\000\000\000\
-    \018\000\005\000\019\000\019\000\019\000\019\000\019\000\019\000\
-    \019\000\019\000\019\000\019\000\000\000\000\000\000\000\000\000\
-    \002\000\255\255\255\255\023\000\005\000\023\000\255\255\000\000\
-    \022\000\022\000\022\000\022\000\022\000\022\000\022\000\022\000\
-    \022\000\022\000\000\000\000\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\011\000\
-    \011\000\000\000\000\000\011\000\022\000\022\000\022\000\022\000\
-    \022\000\022\000\022\000\022\000\022\000\022\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\011\000\022\000\
-    \022\000\022\000\022\000\022\000\022\000\022\000\022\000\022\000\
-    \022\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\000\000\000\000\009\000\000\000\000\000\000\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\012\000\012\000\000\000\000\000\012\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \012\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\012\000\012\000\000\000\000\000\012\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\255\255\000\000\
-    \000\000\000\000\012\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000";
-  Lexing.lex_check = 
-   "\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\000\000\000\000\004\000\004\000\000\000\255\255\004\000\
-    \005\000\005\000\011\000\011\000\005\000\255\255\011\000\012\000\
-    \012\000\255\255\255\255\012\000\255\255\255\255\255\255\255\255\
-    \000\000\255\255\004\000\017\000\014\000\255\255\255\255\005\000\
-    \025\000\011\000\255\255\255\255\255\255\014\000\012\000\014\000\
-    \014\000\255\255\014\000\014\000\014\000\014\000\014\000\014\000\
-    \014\000\014\000\014\000\014\000\255\255\255\255\255\255\255\255\
-    \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\255\255\255\255\014\000\255\255\255\255\
-    \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\003\000\003\000\255\255\255\255\003\000\
-    \018\000\018\000\018\000\018\000\018\000\018\000\018\000\018\000\
-    \018\000\018\000\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\003\000\255\255\019\000\018\000\019\000\019\000\
-    \019\000\019\000\019\000\019\000\019\000\019\000\019\000\019\000\
-    \255\255\255\255\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\255\255\255\255\255\255\
-    \255\255\255\255\255\255\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\006\000\006\000\255\255\
-    \020\000\006\000\020\000\020\000\020\000\020\000\020\000\020\000\
-    \020\000\020\000\020\000\020\000\255\255\255\255\255\255\255\255\
-    \000\000\017\000\014\000\021\000\006\000\021\000\025\000\255\255\
-    \021\000\021\000\021\000\021\000\021\000\021\000\021\000\021\000\
-    \021\000\021\000\255\255\255\255\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\255\255\
-    \255\255\255\255\255\255\255\255\255\255\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\007\000\
-    \007\000\255\255\255\255\007\000\022\000\022\000\022\000\022\000\
-    \022\000\022\000\022\000\022\000\022\000\022\000\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\007\000\023\000\
-    \023\000\023\000\023\000\023\000\023\000\023\000\023\000\023\000\
-    \023\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\255\255\255\255\007\000\255\255\255\255\255\255\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\010\000\010\000\255\255\255\255\010\000\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \010\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\255\255\255\255\255\255\255\255\255\255\
-    \255\255\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\013\000\013\000\255\255\255\255\013\000\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\007\000\255\255\
-    \255\255\255\255\013\000\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\255\255\255\255\255\255\
-    \255\255\255\255\255\255\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255";
-  Lexing.lex_base_code = 
-   "\000\000\000\000\000\000\075\000\000\000\000\000\150\000\208\000\
-    \000\000\000\000\027\001\000\000\000\000\102\001\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000";
-  Lexing.lex_backtrk_code = 
-   "\000\000\000\000\000\000\000\000\000\000\004\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\004\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000";
-  Lexing.lex_default_code = 
-   "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000";
-  Lexing.lex_trans_code = 
-   "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\
-    \001\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000";
-  Lexing.lex_check_code = 
-   "\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\255\255\255\255\255\255\255\255\255\255\
-    \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
-    \000\000\000\000\000\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\003\000\255\255\255\255\
-    \255\255\255\255\255\255\255\255\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\
-    \003\000\003\000\003\000\003\000\003\000\003\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\255\255\255\255\255\255\255\255\255\255\255\255\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\
-    \006\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\255\255\255\255\255\255\255\255\255\255\
-    \255\255\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\
-    \007\000\007\000\007\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\255\255\255\255\
-    \255\255\255\255\255\255\255\255\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\
-    \010\000\010\000\010\000\010\000\010\000\010\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\255\255\255\255\255\255\255\255\255\255\255\255\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\
-    \013\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
-    \255\255\255\255\255\255\255\255\255\255\255\255\255\255";
-  Lexing.lex_code = 
-   "\255\001\255\255\000\001\255";
-}
-
-let rec file lexbuf =
-  lexbuf.Lexing.lex_mem <- Array.create 2 (-1) ;   __ocaml_lex_file_rec lexbuf 0
-and __ocaml_lex_file_rec lexbuf __ocaml_lex_state =
-  match Lexing.new_engine __ocaml_lex_tables __ocaml_lex_state lexbuf with
-      | 0 ->
-# 45 "src/gml.mll"
-      ( file lexbuf )
-# 425 "src/gml.ml"
-
-  | 1 ->
-let
-# 46 "src/gml.mll"
-              key
-# 431 "src/gml.ml"
-= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_mem.(0) in
-# 47 "src/gml.mll"
-      ( let v = value lexbuf in
-	(key, v) :: file lexbuf )
-# 436 "src/gml.ml"
-
-  | 2 ->
-# 50 "src/gml.mll"
-      ( [] )
-# 441 "src/gml.ml"
-
-  | 3 ->
-let
-# 51 "src/gml.mll"
-         c
-# 447 "src/gml.ml"
-= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in
-# 52 "src/gml.mll"
-      ( failwith ("Gml: invalid character " ^ String.make 1 c) )
-# 451 "src/gml.ml"
-
-  | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_file_rec lexbuf __ocaml_lex_state
-
-and value_list lexbuf =
-  lexbuf.Lexing.lex_mem <- Array.create 2 (-1) ;   __ocaml_lex_value_list_rec lexbuf 7
-and __ocaml_lex_value_list_rec lexbuf __ocaml_lex_state =
-  match Lexing.new_engine __ocaml_lex_tables __ocaml_lex_state lexbuf with
-      | 0 ->
-# 56 "src/gml.mll"
-      ( value_list lexbuf )
-# 462 "src/gml.ml"
-
-  | 1 ->
-let
-# 57 "src/gml.mll"
-              key
-# 468 "src/gml.ml"
-= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_mem.(0) in
-# 58 "src/gml.mll"
-      ( let v = value lexbuf in
-	(key, v) :: value_list lexbuf )
-# 473 "src/gml.ml"
-
-  | 2 ->
-# 61 "src/gml.mll"
-      ( [] )
-# 478 "src/gml.ml"
-
-  | 3 ->
-let
-# 62 "src/gml.mll"
-         c
-# 484 "src/gml.ml"
-= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in
-# 63 "src/gml.mll"
-      ( failwith ("Gml: invalid character " ^ String.make 1 c) )
-# 488 "src/gml.ml"
-
-  | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_value_list_rec lexbuf __ocaml_lex_state
-
-and value lexbuf =
-    __ocaml_lex_value_rec lexbuf 14
-and __ocaml_lex_value_rec lexbuf __ocaml_lex_state =
-  match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with
-      | 0 ->
-let
-# 66 "src/gml.mll"
-               i
-# 500 "src/gml.ml"
-= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in
-# 67 "src/gml.mll"
-      ( Int (int_of_string i) )
-# 504 "src/gml.ml"
-
-  | 1 ->
-let
-# 68 "src/gml.mll"
-            r
-# 510 "src/gml.ml"
-= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in
-# 69 "src/gml.mll"
-      ( Float (float_of_string r) )
-# 514 "src/gml.ml"
-
-  | 2 ->
-let
-# 70 "src/gml.mll"
-                      s
-# 520 "src/gml.ml"
-= Lexing.sub_lexeme lexbuf (lexbuf.Lexing.lex_start_pos + 1) (lexbuf.Lexing.lex_curr_pos + -1) in
-# 71 "src/gml.mll"
-      ( String s )
-# 524 "src/gml.ml"
-
-  | 3 ->
-# 73 "src/gml.mll"
-      ( let l = value_list lexbuf in List l )
-# 529 "src/gml.ml"
-
-  | 4 ->
-let
-# 74 "src/gml.mll"
-         c
-# 535 "src/gml.ml"
-= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in
-# 75 "src/gml.mll"
-      ( failwith ("Gml: invalid character " ^ String.make 1 c) )
-# 539 "src/gml.ml"
-
-  | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_value_rec lexbuf __ocaml_lex_state
-
-;;
-
-# 77 "src/gml.mll"
- 
-
-  let parse f =
-    let c = open_in f in
-    let lb = from_channel c in
-    let v = file lb in
-    close_in c;
-    v
-
-  module Parse
-    (B : Builder.S)
-    (L : sig val node : value_list -> B.G.V.label
-	     val edge : value_list -> B.G.E.label end) = 
-  struct
-
-    let create_graph l =
-      let nodes = Hashtbl.create 97 in
-      let g = B.empty () in
-      (* 1st pass: create the nodes *)
-      let g =
-	List.fold_left 
-	  (fun g v -> match v with
-	     | "node", List l ->
-		 let n = B.G.V.create (L.node l) in
-		 begin 
-		   try 
-		     let id = List.assoc "id" l in Hashtbl.add nodes id n
-		   with Not_found -> 
-		     ()
-		 end;
-		 B.add_vertex g n
-	     | _ -> 
-		 g)
-	  g l
-      in
-      (* 2nd pass: add the edges *)
-      List.fold_left
-	(fun g v -> match v with
-	   | "edge", List l ->
-	       begin try
-		 let source = List.assoc "source" l in
-		 let target = List.assoc "target" l in
-		 let nsource = Hashtbl.find nodes source in
-		 let ntarget = Hashtbl.find nodes target in
-		 let e = B.G.E.create nsource (L.edge l) ntarget in
-		 B.add_edge_e g e
-	       with Not_found ->
-		 g
-	       end
-	   | _ ->
-	       g)
-	g l
-	
-    let parse f =
-      match parse f with
-	| ["graph", List l] -> create_graph l
-	| _ -> invalid_arg "Gml.Parse.parse: not a graph file"
-      
-  end
-
-  module Print
-    (G : sig
-       module V : sig
-	 type t
-	 val hash : t -> int
-	 val equal : t -> t -> bool
-	 type label
-	 val label : t -> label
-       end
-       module E : sig
-	 type t
-	 type label
-	 val src : t -> V.t
-	 val dst : t -> V.t
-	 val label : t -> label
-       end
-       type t
-       val iter_vertex : (V.t -> unit) -> t -> unit
-       val iter_edges_e : (E.t -> unit) -> t -> unit
-     end)
-    (L : sig
-       val node : G.V.label -> value_list
-       val edge : G.E.label -> value_list
-     end) =
-  struct
-
-    open Format
-
-    module H = Hashtbl.Make(G.V)
-
-    let print fmt g =
-      let nodes = H.create 97 in
-      let cpt = ref 0 in
-      let id n = 
-	try H.find nodes n
-	with Not_found -> incr cpt; let id = !cpt in H.add nodes n id; id
-      in
-      fprintf fmt "@[graph [@\n";
-      let rec value fmt = function
-	| Int n -> fprintf fmt "%d" n
-	| Float f -> fprintf fmt "%f" f
-	| String s -> fprintf fmt "\"%s\"" s
-	| List l -> fprintf fmt "[@\n  @[%a@]@\n]" value_list l
-      and value_list fmt = function
-	| [] -> ()
-	| [s,v] -> fprintf fmt "%s %a" s value v
-	| (s,v) :: l -> fprintf fmt "%s %a@\n" s value v; value_list fmt l
-      in
-      G.iter_vertex
-	(fun v -> 
-	   fprintf fmt "  @[node [@\n  id %d@\n  @[%a@]@\n]@]@\n" 
-	     (id v) value_list (L.node (G.V.label v)))
-	g;
-      G.iter_edges_e
-	(fun e ->
-	   fprintf fmt 
-	     "  @[edge [@\n  source %d@\n  target %d@\n  @[%a@]@\n]@]@\n"
-	     (id (G.E.src e)) (id (G.E.dst e)) 
-	     value_list (L.edge (G.E.label e)))
-	g;
-      fprintf fmt "]@\n"
-
-  end
-
-
-# 671 "src/gml.ml"
diff --git a/external/ocamlgraph/src/version.ml b/external/ocamlgraph/src/version.ml
deleted file mode 100644
--- a/external/ocamlgraph/src/version.ml
+++ /dev/null
@@ -1,2 +0,0 @@
-let version = "0.99b"
-let date = "Tue Aug 12 13:29:08 PDT 2014"
diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal
--- a/liquid-fixpoint.cabal
+++ b/liquid-fixpoint.cabal
@@ -1,5 +1,6 @@
 name:                liquid-fixpoint
-version:             0.2.0.0
+version:             0.2.1.0
+Copyright:           2010-15 Ranjit Jhala, University of California, San Diego.
 synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
 homepage:            https://github.com/ucsd-progsys/liquid-fixpoint
 license:             BSD3
@@ -24,7 +25,7 @@
                  .
                  3. Code for parsing the results from the fixpoint.native binary
                  .
-                 4. The Ocaml fixpoint code
+                 4. The Ocaml fixpoint code and pre-compiled binaries
                  .
                  5. (Deprecated) Z3 binaries if you want to link against the API.
                  .
@@ -32,9 +33,11 @@
                  .
                  In addition to the .cabal dependencies you require 
                  .
-                 - A Recent Ocaml compiler
+                 - A Z3 (<http://z3.codeplex.com>) or CVC4 (<http://cvc4.cs.nyu.edu>) binary.
+                   If on Windows, please make sure to place the binary and any associated DLLs
+                   in your "cabal/bin" folder, right next to the fixpoint.native.exe binary.
                  .
-                 - A Z3 Binary (<http://z3.codeplex.com>)
+                 - An ocaml compiler (if installing with -fbuild-external).
 
 Extra-Source-Files: configure
                   , external/fixpoint/Makefile
@@ -47,9 +50,7 @@
                   , external/misc/*.ml
                   , external/misc/*.mli
                   , external/ocamlgraph/.depend
-                  , external/ocamlgraph/Makefile
                   , external/ocamlgraph/Makefile.in
-                  , external/ocamlgraph/META
                   , external/ocamlgraph/META.in
                   , external/ocamlgraph/configure
                   , external/ocamlgraph/configure.in
@@ -67,11 +68,19 @@
                   , external/z3/ocaml/build-lib.sh
                   , external/z3/ocaml/z3.ml
                   , external/z3/ocaml/*.c
+                  , external/fixpoint/fixpoint.native-i386-linux
+                  , external/fixpoint/fixpoint.native-i686-w64-mingw32
+                  , external/fixpoint/fixpoint.native-x86_64-darwin
+                  , external/fixpoint/fixpoint.native-x86_64-linux
 
 Flag z3mem
   Description: Link to Z3
   Default:     False
 
+Flag build-external
+  Description: Build fixpoint.native binary from source (requires ocaml)
+  Default:     False
+
 Source-Repository head
   Type:        git
   Location:    https://github.com/ucsd-progsys/liquid-fixpoint/
@@ -93,7 +102,7 @@
                , containers
                , deepseq
                , directory
-               , filemanip
+               -- , filemanip
                , filepath
                , mtl
                , parsec
@@ -119,7 +128,7 @@
                , containers
                , deepseq
                , directory
-               , filemanip
+               -- , filemanip
                , filepath
                , mtl
                , parsec
@@ -139,6 +148,7 @@
                    Language.Fixpoint.Errors,
                    Language.Fixpoint.Config,
                    Language.Fixpoint.Types,
+                   Language.Fixpoint.Visitor,
                    Language.Fixpoint.Sort,
                    Language.Fixpoint.Interface, 
                    Language.Fixpoint.Parse,
diff --git a/src/Language/Fixpoint/Files.hs b/src/Language/Fixpoint/Files.hs
--- a/src/Language/Fixpoint/Files.hs
+++ b/src/Language/Fixpoint/Files.hs
@@ -22,9 +22,9 @@
   , getFixpointPath, getZ3LibPath
 
   -- * Various generic utility functions for finding and removing files
-  , getHsTargets
+  -- , getHsTargets
   , getFileInDirs
-  , findFileInDirs
+  -- , findFileInDirs
   , copyFiles
 
 ) where
@@ -37,14 +37,17 @@
 import           System.Directory
 import           System.Environment
 import           System.FilePath
-import           System.FilePath.Find
+-- import           System.FilePath.Find
 import           Language.Fixpoint.Misc
 
 ------------------------------------------------------------
 -- | Hardwired Paths and Files -----------------------------
 ------------------------------------------------------------
 
-getFixpointPath = fromMaybe msg <$> findExecutable "fixpoint.native"
+getFixpointPath = fromMaybe msg . msum <$>
+                  sequence [ findExecutable "fixpoint.native"
+                           , findExecutable "fixpoint.native.exe"
+                           ]
   where msg     = errorstar "Cannot find fixpoint binary [fixpoint.native]"
 
 getZ3LibPath    = dropFileName <$> getFixpointPath
@@ -149,15 +152,15 @@
 
 ----------------------------------------------------------------------------------
 
-getHsTargets p = mapM canonicalizePath =<< files
-  where
-    files
-      | hasTrailingPathSeparator p = getHsSourceFiles p
-      | otherwise                  = return [p]
+-- getHsTargets p = mapM canonicalizePath =<< files
+--   where
+--     files
+--       | hasTrailingPathSeparator p = getHsSourceFiles p
+--       | otherwise                  = return [p]
 
-getHsSourceFiles = find dirs hs
-  where hs   = extension ==? ".hs" ||? extension ==? ".lhs"
-        dirs = liftM (not . ("dist" `isSuffixOf`)) directory
+-- getHsSourceFiles = find dirs hs
+--   where hs   = extension ==? ".hs" ||? extension ==? ".lhs"
+--         dirs = liftM (not . ("dist" `isSuffixOf`)) directory
 
 ---------------------------------------------------------------------------
 
@@ -165,7 +168,7 @@
 getFileInDirs :: FilePath -> [FilePath] -> IO (Maybe FilePath)
 getFileInDirs name = findFirst (testM doesFileExist . (</> name))
 
-findFileInDirs ::  FilePath -> [FilePath] -> IO FilePath
-findFileInDirs file dirs
-  = liftM (fromMaybe err) (findFirst (find always (fileName ==? file)) dirs)
-    where err = errorstar $ "findFileInDirs: cannot find " ++ file ++ " in " ++ show dirs
+-- findFileInDirs ::  FilePath -> [FilePath] -> IO FilePath
+-- findFileInDirs file dirs
+--   = liftM (fromMaybe err) (findFirst (find always (fileName ==? file)) dirs)
+--     where err = errorstar $ "findFileInDirs: cannot find " ++ file ++ " in " ++ show dirs
diff --git a/src/Language/Fixpoint/Misc.hs b/src/Language/Fixpoint/Misc.hs
--- a/src/Language/Fixpoint/Misc.hs
+++ b/src/Language/Fixpoint/Misc.hs
@@ -3,6 +3,7 @@
 
 module Language.Fixpoint.Misc where
 
+import Data.Traversable               (traverse)
 import Data.Hashable
 import qualified Control.Exception     as Ex
 -- import qualified Data.HashSet        as S 
@@ -41,11 +42,12 @@
 
 wrapStarsWithOptStars True  msg = "\n**** " ++ msg ++ " " ++ replicate (74 - length msg) '*'
 wrapStarsWithOptStars False msg = wrapStars msg
-    
+
+-- withColor _ act = act  
 withColor c act
-  = do setSGR [ SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid c] 
-       act
-       setSGR [ Reset]
+   = do setSGR [ SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid c] 
+        act
+        setSGR [ Reset]
 
 colorStrLn c       = withColor (moodColor c) . putStrLn 
 colorPhaseLn c msg = colorStrLn c . wrapStars .  (msg ++)
@@ -384,4 +386,4 @@
                         Left l  -> go (l:ls) rs  xs
                         Right r -> go ls  (r:rs) xs
 
-
+f <$$> x = traverse f x
diff --git a/src/Language/Fixpoint/Names.hs b/src/Language/Fixpoint/Names.hs
--- a/src/Language/Fixpoint/Names.hs
+++ b/src/Language/Fixpoint/Names.hs
@@ -262,6 +262,7 @@
         , "Set_cap"
         , "Set_dif"
         , "Set_emp"
+        , "Set_empty"
         , "Set_mem"
         , "Set_sub"
         , "FAppTy" 
diff --git a/src/Language/Fixpoint/Parse.hs b/src/Language/Fixpoint/Parse.hs
--- a/src/Language/Fixpoint/Parse.hs
+++ b/src/Language/Fixpoint/Parse.hs
@@ -517,7 +517,7 @@
 
 remainderP p  
   = do res <- p
-       str <- stateInput <$> getParserState
+       str <- getInput
        pos <- getPosition 
        return (res, str, pos) 
 
@@ -533,7 +533,7 @@
 parseFromFile p f = doParse' p f <$> readFile f
 
 freshIntP :: Parser Integer
-freshIntP = do n <- stateUser <$> getParserState
+freshIntP = do n <- getState
                updateState (+ 1)
                return n
 
diff --git a/src/Language/Fixpoint/SmtLib2.hs b/src/Language/Fixpoint/SmtLib2.hs
--- a/src/Language/Fixpoint/SmtLib2.hs
+++ b/src/Language/Fixpoint/SmtLib2.hs
@@ -30,6 +30,7 @@
     -- * Creating and killing SMTLIB2 Process
     , Context (..)
     , makeContext
+    , makeContextNoLog
     , cleanupContext
 
     -- * Execute Queries
@@ -112,7 +113,7 @@
 data Context      = Ctx { pId  :: ProcessHandle
                         , cIn  :: Handle
                         , cOut :: Handle
-                        , cLog :: Handle
+                        , cLog :: Maybe Handle
                         , verbose :: Bool
                         }
 
@@ -147,7 +148,7 @@
        case A.eitherResult res of
          Left e  -> error e
          Right r -> do
-           hPutStrLnNow (cLog me) $ format "; SMT Says: {}" (Only $ show r)
+           maybe (return ()) (\h -> hPutStrLnNow h $ format "; SMT Says: {}" (Only $ show r)) (cLog me)
            when (verbose me) $
              LTIO.putStrLn $ format "SMT Says: {}" (Only $ show r)
            return r
@@ -189,7 +190,9 @@
               ((x:y:[]),zs) -> (x,y) : pairs zs
 
 smtWriteRaw      :: Context -> LT.Text -> IO ()
-smtWriteRaw me !s = {-# SCC smtWriteRaw #-} hPutStrLnNow (cOut me) s >>  hPutStrLnNow (cLog me) s
+smtWriteRaw me !s = {-# SCC smtWriteRaw #-} do
+  hPutStrLnNow (cOut me) s
+  maybe (return ()) (\h -> hPutStrLnNow h s) (cLog me)
 
 smtReadRaw       :: Context -> IO Raw
 smtReadRaw me    = {-# SCC smtReadRaw #-} TIO.hGetLine (cIn me)
@@ -204,15 +207,23 @@
 makeContext   :: SMTSolver -> IO Context
 --------------------------------------------------------------------------
 makeContext s
+  = do me  <- makeProcess s
+       pre <- smtPreamble s me
+       createDirectoryIfMissing True $ takeDirectory smtFile
+       hLog               <- openFile smtFile WriteMode
+       let me' = me { cLog = Just hLog }
+       mapM_ (smtWrite me') pre
+       return me'
+
+makeContextNoLog s
   = do me <- makeProcess s
-       mapM_ (smtWrite me) $ smtPreamble s
+       pre <- smtPreamble s me
+       mapM_ (smtWrite me) pre
        return me
 
 makeProcess s
   = do (hOut, hIn, _ ,pid) <- runInteractiveCommand $ smtCmd s
-       createDirectoryIfMissing True $ takeDirectory smtFile
-       hLog                <- openFile smtFile WriteMode
-       return $ Ctx pid hIn hOut hLog False
+       return $ Ctx pid hIn hOut Nothing False
 
 --------------------------------------------------------------------------
 cleanupContext :: Context -> IO ExitCode
@@ -222,20 +233,26 @@
        code <- waitForProcess pId
        hClose cIn
        hClose cOut
-       hClose cLog
+       maybe (return ()) hClose cLog
        return code
 
 {- "z3 -smt2 -in"                   -}
 {- "z3 -smtc SOFT_TIMEOUT=1000 -in" -}
 {- "z3 -smtc -in MBQI=false"        -}
 
--- ERIC: Do we really need to set mbqi to false? It seems useful for generating test data
-smtCmd Z3      = "z3 -smt2 -in MODEL=true MODEL.PARTIAL=true auto-config=false"
+smtCmd Z3      = "z3 -smt2 -in"
 smtCmd Mathsat = "mathsat -input=smt2"
 smtCmd Cvc4    = "cvc4 --incremental -L smtlib2"
 
-smtPreamble Z3 = z3Preamble
-smtPreamble _  = smtlibPreamble
+-- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...
+smtPreamble Z3 me 
+  = do smtWrite me "(get-info :version)"
+       r <- (!!1) . T.splitOn "\"" <$> smtReadRaw me
+       case r of
+         "4.3.2" -> return $ z3_432_options ++ z3Preamble
+         _       -> return $ z3_options ++ z3Preamble
+smtPreamble _  _  
+  = return smtlibPreamble
 
 smtFile :: FilePath
 smtFile = extFileName Smt2 "out"
@@ -282,6 +299,18 @@
                           ,("Set_cap",cap),("Set_mem",mem),("Set_dif",dif)
                           ,("Set_sub",sub),("Set_com",com)]
 
+-- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...
+z3_432_options 
+  = [ "(set-option :auto-config false)"
+    , "(set-option :model true)"
+    , "(set-option :model.partial false)"
+    , "(set-option :smt.mbqi false)" ]
+z3_options 
+  = [ "(set-option :auto-config false)"
+    , "(set-option :model true)"
+    , "(set-option :model-partial false)"
+    , "(set-option :mbqi false)" ]
+
 z3Preamble
   = [ format "(define-sort {} () Int)"
         (Only elt)
@@ -355,7 +384,7 @@
   foldr (\(x,y) t -> T.replace x y t) t [("[", "ZM"), ("]", "ZN"), (":", "ZC")
                                         ,("(", "ZL"), (")", "ZR"), (",", "ZT")
                                         ,("|", "zb"), ("#", "zh"), ("\\","zr")
-                                        ,("z", "zz"), ("Z", "ZZ")]
+                                        ,("z", "zz"), ("Z", "ZZ"), ("%","zv")]
 
 instance SMTLIB2 SymConst where
   smt2 (SL s) = LT.fromStrict s
diff --git a/src/Language/Fixpoint/Sort.hs b/src/Language/Fixpoint/Sort.hs
--- a/src/Language/Fixpoint/Sort.hs
+++ b/src/Language/Fixpoint/Sort.hs
@@ -94,10 +94,14 @@
   check γ e = do {checkExpr f e; return ()}
    where f =  (`lookupSEnvWithDistance` γ)
 
-  checkSort γ s e = do {t <- checkExpr f e; checkEqSort s t}
-   where f =  (`lookupSEnvWithDistance` γ)
+  checkSort γ s e = checkExpr f (ECst e s) >> return ()
+    where
+      f           =  (`lookupSEnvWithDistance` γ)
 
+  -- ORIG checkSort γ s e = do {t <- checkExpr f e; checkEqSort s t}
+  -- ORIG  where f =  (`lookupSEnvWithDistance` γ)
 
+
 checkEqSort s t
   | s == t    = return ()
   | otherwise = throwError $ "Couldn't match expected type '" 
@@ -159,8 +163,11 @@
          then return t
          else throwError (errCast e t' t)
 
--- | Helper for checking uninterpreted function applications
 
+checkApp f to g es
+  = snd <$> checkApp' f to g es
+
+-- | Helper for checking uninterpreted function applications
 checkApp' f to g es 
   = do gt           <- checkLocSym f g
        (n, its, ot) <- sortFunction gt
@@ -174,10 +181,6 @@
                           return (θ', apply θ' t)
 
 
-checkApp f to g es
-  = snd <$> checkApp' f to g es
-
-
 -- | Helper for checking binary (numeric) operations
 
 checkOp f e1 o e2 
@@ -198,6 +201,9 @@
 checkOpTy f e t t'
   = throwError $ errOp e t t'
 
+checkFractional f l
+  = throwError $ errNonFractional l
+
 checkNumeric f l
   = do t <- checkSym f l
        unless (t == FNum) (throwError $ errNonNumeric l)
@@ -238,10 +244,22 @@
   = (checkNumeric f l >> checkNumeric f l') `catchError` (\_ -> throwError $ errNonNumerics l l') 
 checkRelTy f _ _ FInt (FObj l)     = (checkNumeric f l) `catchError` (\_ -> throwError $ errNonNumeric l) 
 checkRelTy f _ _ (FObj l) FInt     = (checkNumeric f l) `catchError` (\_ -> throwError $ errNonNumeric l)
-checkRelTy f _ _ FReal (FObj l)    = (checkNumeric f l) `catchError` (\_ -> throwError $ errNonNumeric l) 
-checkRelTy f _ _ (FObj l) FReal    = (checkNumeric f l) `catchError` (\_ -> throwError $ errNonNumeric l)
-checkRelTy _ e Eq t1 t2            = unless (t1 == t2 && t1 /= fProp)  (throwError $ errRel e t1 t2)
-checkRelTy _ e Ne t1 t2            = unless (t1 == t2 && t1 /= fProp)  (throwError $ errRel e t1 t2)
+checkRelTy f _ _ FReal FReal       = return ()
+checkRelTy f _ _ FReal (FObj l)    = (checkFractional f l) `catchError` (\_ -> throwError $ errNonFractional l) 
+checkRelTy f _ _ (FObj l) FReal    = (checkFractional f l) `catchError` (\_ -> throwError $ errNonFractional l)
+
+checkRelTy _ e Eq t1 t2
+  | t1 == fProp || t2 == fProp     = throwError $ errRel e t1 t2
+checkRelTy _ e Ne t1 t2
+  | t1 == fProp || t2 == fProp     = throwError $ errRel e t1 t2
+checkRelTy _ e Eq t1 t2            = unify [t1] [t2] >> return ()
+checkRelTy _ e Ne t1 t2            = unify [t1] [t2] >> return ()
+
+-- ORIG checkRelTy _ e Eq t1 t2            = unless (t1 == t2 && t1 /= fProp)  (throwError $ errRel e t1 t2)
+-- ORIG checkRelTy _ e Ne t1 t2            = unless (t1 == t2 && t1 /= fProp)  (throwError $ errRel e t1 t2)
+
+
+
 checkRelTy _ e Ueq t1 t2           = unless (isAppTy t1 && isAppTy t2) (throwError $ errRel e t1 t2)
 checkRelTy _ e Une t1 t2           = unless (isAppTy t1 && isAppTy t2) (throwError $ errRel e t1 t2)
 checkRelTy _ e _  t1 t2            = unless (t1 == t2)                 (throwError $ errRel e t1 t2)
@@ -258,6 +276,16 @@
 isAppTy (FApp _ _) = True
 isAppTy _          = False
 
+
+isPoly :: Sort -> Bool
+isPoly = not . null . fVars
+
+fVars (FVar i)     = [i]
+fVars (FFunc _ ts) = concatMap fVars ts
+fVars (FApp _ ts)  = concatMap fVars ts
+fVars _            = []
+
+
 -------------------------------------------------------------------------
 -- | Error messages -----------------------------------------------------
 -------------------------------------------------------------------------
@@ -295,7 +323,9 @@
 errNonFunction t     = printf "Sort %s is not a function" (showFix t)
 
 errNonNumeric  l     = printf "FObj sort %s is not numeric" (showFix l)
-errNonNumerics l l'   = printf "FObj sort %s and %s are different and not numeric" (showFix l) (showFix l')
+errNonNumerics l l'  = printf "FObj sort %s and %s are different and not numeric" (showFix l) (showFix l')
+
+errNonFractional  l  = printf "FObj sort %s is not fractional" (showFix l)
 
 errUnexpectedPred p  = printf "Sort Checking: Unexpected Predicate %s" (showFix p)
 
diff --git a/src/Language/Fixpoint/Types.hs b/src/Language/Fixpoint/Types.hs
--- a/src/Language/Fixpoint/Types.hs
+++ b/src/Language/Fixpoint/Types.hs
@@ -789,7 +789,7 @@
 type BindId        = Int
 type FEnv          = SEnv SortedReft
 
-newtype IBindEnv   = FB (S.HashSet BindId)
+newtype IBindEnv   = FB (S.HashSet BindId) deriving (Data, Typeable)
 newtype SEnv a     = SE { se_binds :: M.HashMap Symbol a } deriving (Eq, Data, Typeable, Generic, F.Foldable, Traversable)
 data BindEnv       = BE { be_size  :: Int
                         , be_binds :: M.HashMap BindId (Symbol, SortedReft)
diff --git a/src/Language/Fixpoint/Visitor.hs b/src/Language/Fixpoint/Visitor.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Fixpoint/Visitor.hs
@@ -0,0 +1,127 @@
+{-# LANGUAGE TupleSections #-}
+
+module Language.Fixpoint.Visitor (
+  -- * Visitor
+     Visitor (..)
+     
+  -- * Default Visitor
+  , defaultVisitor
+
+  -- * Transformers
+  , trans
+            
+  -- * Accumulators
+  , fold
+
+  ) where
+
+import           Data.Monoid
+import           Data.Traversable               (traverse)
+import           Control.Applicative            (Applicative (), (<$>), (<*>))
+import           Control.Exception              (throw)
+import           Control.Monad.Trans.State      (modify, State, runState)
+import           Language.Fixpoint.Misc         (mapSnd)
+import           Language.Fixpoint.Types
+
+
+
+data Visitor acc ctx = Visitor {
+ -- | Context @ctx@ is built up in a "top-down" fashion but not across siblings
+    ctxExpr :: ctx -> Expr -> ctx
+  , ctxPred :: ctx -> Pred -> ctx
+
+  -- | Transforms can access current @ctx@
+  , txExpr  :: ctx -> Expr -> Expr 
+  , txPred  :: ctx -> Pred -> Pred 
+
+  -- | Accumulations can access current @ctx@; @acc@ value is monoidal
+  , accExpr :: ctx -> Expr -> acc
+  , accPred :: ctx -> Pred -> acc
+  }
+                         
+---------------------------------------------------------------------------------
+defaultVisitor :: Monoid acc => Visitor acc ctx
+---------------------------------------------------------------------------------
+defaultVisitor = Visitor {
+    ctxExpr    = \c _ -> c
+  , ctxPred    = \c _ -> c
+  , txExpr     = \_ x -> x
+  , txPred     = \_ x -> x
+  , accExpr    = \_ _ -> mempty
+  , accPred    = \_ _ -> mempty
+  }           
+
+
+------------------------------------------------------------------------          
+
+fold         :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> a 
+fold v c a t = snd $ execVisitM v c a visit t
+
+trans        :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> t 
+trans v c a z = fst $ execVisitM v c mempty visit z 
+
+execVisitM v c a f x = runState (f v c x) a
+
+type VisitM acc = State acc 
+
+accum :: (Monoid a) => a -> VisitM a ()
+accum = modify . mappend
+
+f <$$> x = traverse f x
+
+------------------------------------------------------------------------------
+class Visitable t where
+  visit :: (Monoid a) => Visitor a c -> c -> t -> VisitM a t
+
+instance Visitable Expr where
+  visit = visitExpr
+
+instance Visitable Pred where
+  visit = visitPred
+
+instance Visitable Refa where
+  visit v c (RConc p) = RConc <$> visit v c p
+  visit _ _ r         = return r 
+
+instance Visitable Reft where
+  visit v c (Reft (vv, ras)) = (Reft . (vv,)) <$> visitMany v c ras 
+
+visitMany :: (Monoid a, Visitable t) => Visitor a ctx -> ctx -> [t] -> VisitM a [t]
+visitMany v c xs = visit v c <$$> xs
+
+visitExpr :: (Monoid a) => Visitor a ctx -> ctx -> Expr -> VisitM a Expr 
+visitExpr v = vE
+  where
+    vP      = visitPred v
+    vE c e  = accum acc >> step c' e' where c'  = ctxExpr v c e
+                                            e'  = txExpr v c' e
+                                            acc = accExpr v c' e
+    step c e@EBot         = return e
+    step c e@(ESym _)     = return e   
+    step c e@(ECon _)     = return e 
+    step c e@(ELit _ _)   = return e 
+    step c e@(EVar _)     = return e
+    step c (EApp f es)    = EApp f     <$> (vE c <$$> es)  
+    step c (EBin o e1 e2) = EBin o     <$> vE c e1 <*> vE c e2
+    step c (EIte p e1 e2) = EIte       <$> vP c p  <*> vE c e1 <*> vE c e2
+    step c (ECst e t)     = (`ECst` t) <$> vE c e
+ 
+visitPred :: (Monoid a) => Visitor a ctx -> ctx -> Pred -> VisitM a Pred 
+visitPred v = vP
+  where
+    vE     = visitExpr v
+    vP c p = accum acc >> step c' p' where c'   = ctxPred v c p
+                                           p'   = txPred v c' p
+                                           acc  = accPred v c' p
+    step c (PAnd  ps)      = PAnd     <$> (vP c <$$> ps)
+    step c (POr  ps)       = POr      <$> (vP c <$$> ps) 
+    step c (PNot p)        = PNot     <$> vP c p
+    step c (PImp p1 p2)    = PImp     <$> vP c p1 <*> vP c p2 
+    step c (PIff p1 p2)    = PIff     <$> vP c p1 <*> vP c p2
+    step c (PBexp  e)      = PBexp    <$> vE c e
+    step c (PAtom r e1 e2) = PAtom r  <$> vE c e1 <*> vE c e2 
+    step c (PAll xts p)    = PAll xts <$> vP c p
+    step c p@PTrue         = return p
+    step c p@PFalse        = return p
+    step c p@PTop          = return p
+