diff --git a/external/fixpoint/ast.ml b/external/fixpoint/ast.ml
--- a/external/fixpoint/ast.ml
+++ b/external/fixpoint/ast.ml
@@ -1,30 +1,30 @@
 (*
- * Copyright © 2009 The Regents of the University of California. All rights reserved. 
+ * Copyright © 2009 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 
+ * 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.
  *
  *)
 
 (**
- * This module implements a DAG representation for expressions and 
+ * This module implements a DAG representation for expressions and
  * predicates: each sub-predicate or sub-expression is paired with
- * a unique int ID, which enables constant time hashing. 
+ * a unique int ID, which enables constant time hashing.
  * However, one must take care when using DAGS:
  * (1) they can only be constructed using the appropriate functions
  * (2) when destructed via pattern-matching, one must discard the ID
@@ -42,17 +42,17 @@
 module Cone = struct
   type 'a t = Empty | Cone of ('a * 'a t) list
 
-  let rec map f = function 
+  let rec map f = function
     | Empty    -> Empty
     | Cone xcs -> Cone (List.map (f <**> map f) xcs)
-end 
+end
 
 module Sort =
   struct
-    type loc = 
-      | Loc  of string 
+    type loc =
+      | Loc  of string
       | Lvar of int
-      | LFun 
+      | LFun
 
     type tycon = string
 
@@ -63,25 +63,27 @@
       | Obj
       | Var of int              (* type-var *)
       | Ptr of loc              (* c-pointer *)
-      | Func of int * t list    (* type-var-arity, in-types @ [out-type]      *)
-      | Num                     (* kind, for numeric tyvars -- ptr(loc(s)) -- *)
+      | Func of int * t list    (* type-var-arity, in-types @ [out-type]         *)
+      | Num                     (* kind, for numeric tyvars -- ptr(loc(s))    -- *)
+      | Frac                    (* kind, for fractional tyvars -- ptr(loc(s)) -- *)
       | App of tycon * t list   (* type constructors *)
 
-    type sub = { locs: (int * string) list; 
+    type sub = { locs: (int * string) list;
                  vars: (int * t) list; }
 
-   
+
     let tycon_string x = x
     (*
-    let is_loc_string s = 
-      let re = Str.regexp "[a-zA-Z]+[0-9]+" in 
+    let is_loc_string s =
+      let re = Str.regexp "[a-zA-Z]+[0-9]+" in
       Str.string_match re s 0
-    
+
     let loc_of_string = fun s -> let _ = asserts (is_loc_string s) in Loc s
     let loc_of_index  = fun i -> Lvar i
     *)
 
-    let t_num       = Num 
+    let t_num       = Num
+    let t_frac      = Frac
     let t_obj       = Obj
     let t_bool      = Bool
     let t_int       = Int
@@ -89,17 +91,17 @@
     let t_generic   = fun i -> let _ = asserts (0 <= i) "t_generic: %d" i in Var i
     let t_ptr       = fun l -> Ptr l
     let t_func      = fun i ts -> Func (i, ts)
-    let tycon s     = s 
+    let tycon s     = s
     let tc_app      = "FAppTy"
 
     (* let tycon_re    = Str.regexp "[A-Z][0-9 a-z A-Z '.']"
-     * function | s when Str.string_match tycon_re s 0 -> s  
-                | s -> assertf "Error: Invalid tycon: %s" s 
+     * function | s when Str.string_match tycon_re s 0 -> s
+                | s -> assertf "Error: Invalid tycon: %s" s
      *)
 
-    let t_app c ts  = if c = tc_app then App (c, ts) else 
+    let t_app c ts  = if c = tc_app then App (c, ts) else
                         List.fold_left (fun t1 t2 -> App (tc_app, [t1; t2])) (App (c, [])) ts
-    (* let t_app c ts  = List.fold_left (fun t1 t2 -> App ("FAppTy", [t1; t2])) (App (c, [])) ts *)   
+    (* let t_app c ts  = List.fold_left (fun t1 t2 -> App ("FAppTy", [t1; t2])) (App (c, [])) ts *)
     (* let t_app c ts  = App (c, ts) *)
 
     let loc_to_string = function
@@ -114,36 +116,37 @@
       | Bool         -> "bool"
       | Obj          -> "obj"
       | Num          -> "num"
-      | Ptr l        -> loc_to_string l 
+      | Frac         -> "frac"
+      | Ptr l        -> loc_to_string l
                         (* Printf.sprintf "ptr(%s)" (loc_to_string l) *)
-      | Func (n, ts) -> ts |> List.map to_string 
-                           |> String.concat " ; " 
-                           |> Printf.sprintf "func(%d, [%s])" n 
-      | App (c, ts)  -> ts |> List.map to_string_arg 
-                           |> String.concat " " 
-                           |> Printf.sprintf "%s %s" c 
-    
-    and to_string_arg t = match t with 
+      | Func (n, ts) -> ts |> List.map to_string
+                           |> String.concat " ; "
+                           |> Printf.sprintf "func(%d, [%s])" n
+      | App (c, ts)  -> ts |> List.map to_string_arg
+                           |> String.concat " "
+                           |> Printf.sprintf "%s %s" c
+
+    and to_string_arg t = match t with
       | App (_, _) -> Printf.sprintf "(%s)" (to_string t)
       | _          -> to_string t
 
     let to_string_short = function
       | Func _ -> "func"
    (* | Ptr _  -> "ptr" *)
-      | t      -> to_string t      
+      | t      -> to_string t
 
-    let print fmt t = 
-      t |> to_string 
+    let print fmt t =
+      t |> to_string
         |> Format.fprintf fmt "%s"
 
     let sub_to_string {locs = ls; vars = vs} =
       let lts = fun (i, s) -> Printf.sprintf "(%d := %s)" i s in
       let vts = fun (i, t) -> Printf.sprintf "(%d := %s)" i (to_string t) in
-      Printf.sprintf "locs := %s, vars := %s \n" 
-        (String.concat "" (List.map lts ls)) 
-        (String.concat "" (List.map vts vs)) 
+      Printf.sprintf "locs := %s, vars := %s \n"
+        (String.concat "" (List.map lts ls))
+        (String.concat "" (List.map vts vs))
 
-    let rec map f = function 
+    let rec map f = function
       | Func (n, ts) -> Func (n, List.map (map f) ts)
       | App  (c, ts) -> App  (c, List.map (map f) ts)
       | t            -> f t
@@ -152,8 +155,8 @@
       | Func (n, ts) as t -> List.fold_left (fold f) (f b t) ts
       | t                 -> f b t
 
-    let subs_tvar ts = 
-      map begin function 
+    let subs_tvar ts =
+      map begin function
           | Var i -> Misc.do_catchf "ERROR: subs_tvar" (List.nth ts) i
           | t     -> t
       end
@@ -165,7 +168,7 @@
     let is_int = function
       | Int -> true
       | _   -> false
-    
+
     let is_real = function
       | Real -> true
       | _    -> false
@@ -179,19 +182,19 @@
       | _      -> false
 
     let app_of_t = function
-      | App (c, ts) -> Some (c, ts) 
+      | App (c, ts) -> Some (c, ts)
       | _           -> None
 
     (* (L t1 t2 t3) is now encoded as
         ---> (((L @ t1) @ t2) @ t3)
         ---> App(@, [App(@, [App(@, [L[]; t1]); t2]); t3])
-        The following decodes the above as 
+        The following decodes the above as
      *)
-    let rec app_args_of_t acc = function 
-      | App (c, [t1; t2]) when c = tc_app -> app_args_of_t (t2 :: acc) t1 
+    let rec app_args_of_t acc = function
+      | App (c, [t1; t2]) when c = tc_app -> app_args_of_t (t2 :: acc) t1
       | App (c, [])                       -> (c, acc)
       | t                                 -> (tc_app, t :: acc)
-      
+
       (*
       | Ptr (Loc s)                       -> (tycon s, acc)
       | t                                 -> assertf "app_args_of_t: unexpected t1 = %s" (to_string t)
@@ -200,10 +203,10 @@
     let app_of_t = function
       | App (c, _) as t when c = tc_app   -> Some (app_args_of_t [] t)
       | App (c, ts)                       -> Some (c, ts)
-      | _                                 -> None 
+      | _                                 -> None
 
     let func_of_t = function
-      | Func (i, ts) -> let (xts, t) = ts |> Misc.list_snoc |> Misc.swap in 
+      | Func (i, ts) -> let (xts, t) = ts |> Misc.list_snoc |> Misc.swap in
                         Some (i, xts, t)
       | _            -> None
 
@@ -218,57 +221,57 @@
       | (Ptr _), Int -> true
       | _            -> t1 = t2
 
-    (* {{{ 
-    let concretize ts = function 
-      | Func (n, ats) when n = List.length ts -> 
+    (* {{{
+    let concretize ts = function
+      | Func (n, ats) when n = List.length ts ->
           Func (n, List.map (subs_tvar ts) ats)
-      | _ -> 
-          assertf "ERROR: bad application" 
+      | _ ->
+          assertf "ERROR: bad application"
 
-    let is_monotype t = 
+    let is_monotype t =
       fold (fun b t -> b && (match t with Var _ -> false | _ -> true)) true t
     }}} *)
 
 
     let lookup_var = fun s i -> try Some (List.assoc i s.vars) with Not_found -> None
     let lookup_loc = fun s j -> try Some (List.assoc j s.locs) with Not_found -> None
-    
-    let rec unifyt s = function 
+
+    let rec unifyt s = function
       | Num,_ | _, Num -> None
-      | ct, (Var i) 
-      | (Var i), ct 
-        (* when ct != Bool *) -> 
-          begin match lookup_var s i with 
+      | ct, (Var i)
+      | (Var i), ct
+        (* when ct != Bool *) ->
+          begin match lookup_var s i with
           | Some ct' when ct = ct' -> Some s
           | Some _                 -> None
           | None                   -> Some {s with vars = (i,ct) :: s.vars}
           end
 
-      | Ptr LFun, Ptr _ 
+      | Ptr LFun, Ptr _
       | Ptr _, Ptr LFun -> Some s
       | Ptr (Loc cl), Ptr (Lvar j)
       | Ptr (Lvar j), Ptr (Loc cl) ->
-          begin match lookup_loc s j with 
+          begin match lookup_loc s j with
           | Some cl' when cl' = cl -> Some s
           | Some _                 -> None
           | None                   -> Some {s with locs = (j,cl) :: s.locs}
           end
-      
-      | App (c1, t1s), App (c2, t2s) 
+
+      | App (c1, t1s), App (c2, t2s)
         when c1 = c2 && List.length t1s = List.length t2s ->
           Misc.maybe_fold unifyt s (List.combine t1s t2s)
-      
-      | (t1, t2) when t1 = t2 -> 
+
+      | (t1, t2) when t1 = t2 ->
           Some s
       | _        -> None
-   
+
     let empty_sub = {vars = []; locs = []}
-   
+
     let unifyWith s ats cts =
       let _ = asserts (List.length ats = List.length cts) "ERROR: unify sorts" in
-      List.combine ats cts 
-      |> Misc.maybe_fold unifyt s 
-      (* >> (fun so -> Printf.printf "unify: [%s] ~ [%s] = %s \n" 
+      List.combine ats cts
+      |> Misc.maybe_fold unifyt s
+      (* >> (fun so -> Printf.printf "unify: [%s] ~ [%s] = %s \n"
                       (String.concat "; " (List.map to_string ats))
                       (String.concat "; " (List.map to_string cts))
                       (match so with None -> "NONE" | Some s -> sub_to_string s))
@@ -276,7 +279,7 @@
 
     let unify = unifyWith empty_sub
 
-    let apply s = 
+    let apply s =
       map begin fun t -> match t with
           | Var i        -> (match lookup_var s i with Some t' -> t' | _ -> t)
           | Ptr (Lvar j) -> (match lookup_loc s j with Some l -> Ptr (Loc l) | _ -> t)
@@ -284,30 +287,30 @@
       end
 
     let rec fold f acc t = match t with
-      | Var _ | Int | Real | Bool | Obj | Num | Ptr _ 
-        -> f acc t 
-      | Func (_, ts) | App (_, ts) 
-        -> List.fold_left (fold f) (f acc t) ts 
-      
-    let vars_of_t = fold begin fun acc -> function 
-      | Var i -> i :: acc 
+      | Var _ | Int | Real | Bool | Obj | Num | Ptr _
+        -> f acc t
+      | Func (_, ts) | App (_, ts)
+        -> List.fold_left (fold f) (f acc t) ts
+
+    let vars_of_t = fold begin fun acc -> function
+      | Var i -> i :: acc
       | _     -> acc
     end []
-    
-    let locs_of_t = fold begin fun acc -> function 
-      | Ptr (Loc l) -> l :: acc 
+
+    let locs_of_t = fold begin fun acc -> function
+      | Ptr (Loc l) -> l :: acc
       | _           -> acc
     end []
-    
+
     let subst_locs_vars lim = map begin function
       | Ptr (Loc l) when SM.mem l lim -> Var (SM.find l lim)
       | t                             -> t
     end
 
     (* API *)
-    let generalize ts = 
+    let generalize ts =
       let locs = ts |> Misc.flap locs_of_t |> Misc.sort_and_compact       in
-      let idx  = ts |> Misc.flap vars_of_t |> Misc.list_max (-1) |> (+) 1 in 
+      let idx  = ts |> Misc.flap vars_of_t |> Misc.list_max (-1) |> (+) 1 in
       let lim  = Misc.index_from idx locs |>: Misc.swap |> SM.of_list     in
       List.map (subst_locs_vars lim) ts
 
@@ -320,42 +323,42 @@
 
   end
 
-module Symbol = 
-  struct 
+module Symbol =
+  struct
     type t = string
-    
+
     let mk_wild =
       let t,_ = Misc.mk_int_factory () in
       t <+> string_of_int <+> (^) "~A"
-    
+
     let is_wild_fresh s = s = "_"
     let is_wild_any   s = s.[0] = '~'
     let is_wild_pre   s = s.[0] = '@'
     let is_wild s       = is_wild_fresh s || is_wild_any s || is_wild_pre s
 
-    let is_safe s = 
+    let is_safe s =
       let re = Str.regexp "[A-Za-z '~' '_' '\'' '@' ][0-9 a-z A-Z '_' '@' '\'' '.' '#']*$" in
       Str.string_match re s 0
-    
-    let of_string, to_string = 
+
+    let of_string, to_string =
       let of_t = Hashtbl.create 117 in
       let to_t = Hashtbl.create 117 in
       let bind = fun s sy -> Hashtbl.replace of_t s sy; Hashtbl.replace to_t sy s in
       let f,_  = Misc.mk_string_factory "FIXPOINTSYMBOL_" in
-      ((fun s -> 
+      ((fun s ->
         if is_wild_fresh s then mk_wild () else
         if is_safe s then s else
            try Hashtbl.find of_t s with Not_found ->
              let sy = f () in
              let _  = bind s sy in sy),
        (fun sy -> try Hashtbl.find to_t sy with Not_found -> sy))
-                   
+
     let to_string = fun s -> s (* if is_safe s then s else "'" ^ s ^ "'" *)
 
     let suffix = fun s suff -> of_string ((to_string s) ^ suff)
 
     let print fmt s =
-      to_string s |> Format.fprintf fmt "%s" 
+      to_string s |> Format.fprintf fmt "%s"
 
     let vvprefix = "VV_"
     let vvsuffix = function
@@ -372,26 +375,26 @@
     let is_value_variable = (=) vvprefix
     let value_variable _  = vvprefix
 
-    module SMap = Misc.EMap (struct type t = string 
-                                    let compare i1 i2 = compare i1 i2 
+    module SMap = Misc.EMap (struct type t = string
+                                    let compare i1 i2 = compare i1 i2
                                     let print         = print         end)
 
     module SSet = Misc.ESet (struct type t = string
                                     let compare i1 i2 = compare i1 i2 end)
 
-   (* let sm_length m = 
+   (* let sm_length m =
       SMap.fold (fun _ _ i -> i+1) m 0
 
-    let sm_filter f sm = 
-      SMap.fold begin fun x y sm -> 
-        if f x y then SMap.add x y sm else sm 
-    end sm SMap.empty 
+    let sm_filter f sm =
+      SMap.fold begin fun x y sm ->
+        if f x y then SMap.add x y sm else sm
+    end sm SMap.empty
 
     let sm_to_list sm =
       SMap.fold (fun x y acc -> (x,y)::acc) sm []
-    
-    let sm_of_list xs = 
-      List.fold_left (fun sm (k,v) -> SMap.add k v sm) SMap.empty xs 
+
+    let sm_of_list xs =
+      List.fold_left (fun sm (k,v) -> SMap.add k v sm) SMap.empty xs
    *)
 
   end
@@ -399,8 +402,8 @@
 module Constant =
   struct
 
-    type t = Int  of int 
-           | Real of float 
+    type t = Int  of int
+           | Real of float
            | Lit  of string * Sort.t
 
     let to_string = function
@@ -411,34 +414,34 @@
     let print fmt s =
       to_string s |> Format.fprintf fmt "%s"
   end
- 
 
+
 type tag  = int
 
 type brel = Eq    (* equal                  *)
           | Ne    (* not-equal              *)
-          | Gt    (* greater than           *) 
+          | Gt    (* greater than           *)
           | Ge    (* greater than or equal  *)
           | Lt    (* less than              *)
           | Le    (* less than or equal     *)
-          | Ueq   (* unsorted-equality      *) 
+          | Ueq   (* unsorted-equality      *)
           | Une   (* unsorted-disequality   *)
 
 type bop  = Plus | Minus | Times | Div | Mod  (* NOTE: For "Mod" 2nd expr should be a constant or a var *)
 
-type expr = expr_int * tag 
-    
+type expr = expr_int * tag
+
 and expr_int =
   | Con  of Constant.t
   | Var  of Symbol.t
   | App  of Symbol.t * expr list
-  | Bin  of expr * bop * expr  
+  | Bin  of expr * bop * expr
   | Ite  of pred * expr * expr
-  | Fld  of Symbol.t * expr             (* NOTE: Fld (s, e) == App ("field"^s,[e]) *) 
-  | Cst  of expr * Sort.t 
+  | Fld  of Symbol.t * expr             (* NOTE: Fld (s, e) == App ("field"^s,[e]) *)
+  | Cst  of expr * Sort.t
   | Bot
   | MExp of expr list
-  | MBin of expr * bop list * expr 
+  | MBin of expr * bop list * expr
 
 and pred = pred_int * tag
 
@@ -451,15 +454,15 @@
   | Imp   of pred * pred
   | Iff   of pred * pred
   | Bexp  of expr
-  | Atom  of expr * brel * expr 
+  | Atom  of expr * brel * expr
   | MAtom of expr * brel list * expr
   | Forall of ((Symbol.t * Sort.t) list) * pred
 
-let list_hash b xs = 
+let list_hash b xs =
   List.fold_left (fun v (_,id) -> 2*v + id) b xs
 
 module Hashcons (X : sig type t
-                         val sub_equal : t -> t -> bool 
+                         val sub_equal : t -> t -> bool
                          val hash : t -> int end) = struct
 
   module HashStruct = struct
@@ -469,11 +472,11 @@
   end
 
   module Hash = Weak.Make(HashStruct)
-  
-  let wrap = 
+
+  let wrap =
     let tab = Hash.create 251 in
     let ctr = ref 0 in
-    fun e -> 
+    fun e ->
       let res = Hash.merge tab (e, !ctr) in
       let _   = if snd res = !ctr then incr ctr in
       res
@@ -486,14 +489,14 @@
   type t = expr_int
   let sub_equal e1 e2 =
     match e1, e2 with
-      | Con c1, Con c2 -> 
+      | Con c1, Con c2 ->
           c1 = c2
-      | MExp es1, MExp es2 -> 
+      | MExp es1, MExp es2 ->
           es1 = es2
-      | Var x1, Var x2 -> 
+      | Var x1, Var x2 ->
           x1 = x2
       | App (s1, e1s), App (s2, e2s) ->
-	  (s1 = s2) && 
+	  (s1 = s2) &&
           (try List.for_all2 (==) e1s e2s with _ -> false)
       | Bin (e1, op1, e1'), Bin (e2, op2, e2') ->
           op1 = op2 && e1 == e2 && e1' == e2'
@@ -505,27 +508,27 @@
           s1 = s2 && e1 == e2
       | Cst (e1, s1), Cst (e2, s2) ->
           s1 = s2 && e1 == e2
-      | _ -> 
+      | _ ->
           false
-  
+
   let hash = function
-    | Con (Constant.Int x) -> 
+    | Con (Constant.Int x) ->
         x
-    | Con (Constant.Real x) -> 
+    | Con (Constant.Real x) ->
         64 + int_of_float x
-    | Con (Constant.Lit (s,_)) -> 
+    | Con (Constant.Lit (s,_)) ->
         32 + Hashtbl.hash s
     | MExp es ->
-        list_hash 6 es 
-    | Var x -> 
+        list_hash 6 es
+    | Var x ->
         Hashtbl.hash x
-    | App (s, es) -> 
-        list_hash ((Hashtbl.hash s) + 1) es 
-    | Bin ((_,id1), op, (_,id2)) -> 
-        (Hashtbl.hash op) + 1 + (2 * id1) + id2 
-    | MBin ((_,id1), op::_ , (_,id2)) -> 
-        (Hashtbl.hash op) + 1 + (2 * id1) + id2 
-    | Ite ((_,id1), (_,id2), (_,id3)) -> 
+    | App (s, es) ->
+        list_hash ((Hashtbl.hash s) + 1) es
+    | Bin ((_,id1), op, (_,id2)) ->
+        (Hashtbl.hash op) + 1 + (2 * id1) + id2
+    | MBin ((_,id1), op::_ , (_,id2)) ->
+        (Hashtbl.hash op) + 1 + (2 * id1) + id2
+    | Ite ((_,id1), (_,id2), (_,id3)) ->
         32 + (4 * id1) + (2 * id2) + id3
     | Fld (s, (_,id)) ->
         (Hashtbl.hash s) + 12 + id
@@ -536,47 +539,47 @@
     | _ -> assertf "pattern error in A.pred hash"
 
 end
-  
+
 module ExprHashcons = Hashcons(ExprHashconsStruct)
 
 module PredHashconsStruct = struct
-  
+
   type t = pred_int
-  
+
   let sub_equal p1 p2 =
     match p1, p2 with
-      | True, True | False, False -> 
+      | True, True | False, False ->
           true
-      | And p1s, And p2s  | Or  p1s, Or p2s -> 
+      | And p1s, And p2s  | Or  p1s, Or p2s ->
           (try List.for_all2 (==) p1s p2s with _ -> false)
-      | Not p1, Not p2 -> 
+      | Not p1, Not p2 ->
           p1 == p2
-      | Imp (p1, p1'), Imp (p2, p2') -> 
+      | Imp (p1, p1'), Imp (p2, p2') ->
           p1 == p2 && p1' == p2'
       | Iff (p1,p1'), Iff (p2,p2') ->
           p1 == p2 && p1' == p2'
-      | Bexp e1, Bexp e2 -> 
+      | Bexp e1, Bexp e2 ->
           e1 == e2
       | Atom (e1, r1, e1'), Atom (e2, r2, e2') ->
           r1 = r2 && e1 == e2 && e1' == e2'
       | MAtom (e1, r1, e1'), MAtom (e2, r2, e2') ->
           r1 = r2 && e1 == e2 && e1' == e2'
-      | Forall(q1s,p1), Forall(q2s,p2) -> 
+      | Forall(q1s,p1), Forall(q2s,p2) ->
           q1s = q2s && p1 == p2
-      | _ -> 
+      | _ ->
           false
- 
+
  let hash = function
-   | True -> 
+   | True ->
        0
-   | False -> 
+   | False ->
        1
-   | And ps -> 
+   | And ps ->
        list_hash 2 ps
-   | Or ps -> 
+   | Or ps ->
        list_hash 3 ps
-   | Not (_,id) -> 
-       8 + id 
+   | Not (_,id) ->
+       8 + id
    | Imp ((_,id1), (_,id2)) ->
        20 + (2 * id1) + id2
    | Iff ((_,id1), (_,id2)) ->
@@ -587,15 +590,15 @@
        36 + (Hashtbl.hash r) + (2 * id1) + id2
    | MAtom ((_,id1), r, (_,id2)) ->
        42 + (Hashtbl.hash r) + (2 * id1) + id2
-   | Forall(qs,(_,id)) -> 
+   | Forall(qs,(_,id)) ->
        50 + (2 * (Hashtbl.hash qs)) + id
 end
-  
+
 module PredHashcons = Hashcons(PredHashconsStruct)
 
 let ewr = ExprHashcons.wrap
 let euw = ExprHashcons.unwrap
-let pwr = PredHashcons.wrap 
+let pwr = PredHashcons.wrap
 let puw = PredHashcons.unwrap
 
 (* Constructors: Expressions *)
@@ -612,20 +615,20 @@
 let eModExp = fun (e, m) -> ewr (Bin (e, Mod, m))
 let eVar = fun s -> ewr (Var s)
 let eApp = fun (s, es) -> ewr (App (s, es))
-let eBin = fun (e1, op, e2) -> ewr (Bin (e1, op, e2)) 
+let eBin = fun (e1, op, e2) -> ewr (Bin (e1, op, e2))
 
-let eMBin = fun (e1, ops, e2) -> ewr (MBin (e1, ops, e2)) 
+let eMBin = fun (e1, ops, e2) -> ewr (MBin (e1, ops, e2))
 let eIte = fun (ip,te,ee) -> ewr (Ite(ip,te,ee))
 let eFld = fun (s,e) -> ewr (Fld (s,e))
 let eCst = fun (e,t) -> ewr (Cst (e, t))
 
-let eTim = function 
-  | (Con (Constant.Int n1), _), (Con (Constant.Int n2), _) -> 
+let eTim = function
+  | (Con (Constant.Int n1), _), (Con (Constant.Int n2), _) ->
       ewr (Con (Constant.Int (n1 * n2)))
-  | (Con (Constant.Int 1), _), e2 -> 
-      e2 
-  | (Con (Constant.Int (-1)), _), e2 -> 
-      eBin (zero, Minus, e2) 
+  | (Con (Constant.Int 1), _), e2 ->
+      e2
+  | (Con (Constant.Int (-1)), _), e2 ->
+      eBin (zero, Minus, e2)
   | (e1, e2) -> eBin (e1, Times, e2)
 
 
@@ -650,8 +653,8 @@
 let pUequal = fun (e1,e2) -> pAtom (e1, Ueq, e2)
 
 
-let pAnd   = fun ps -> match Misc.flap conjuncts ps with 
-                       | []  -> pTrue 
+let pAnd   = fun ps -> match Misc.flap conjuncts ps with
+                       | []  -> pTrue
                        | [p] -> p
                        | ps  -> pwr (And (Misc.flap conjuncts ps))
 
@@ -669,14 +672,14 @@
   let hash (_,x) = x
 end)
 
-let bop_to_string = function 
+let bop_to_string = function
   | Plus  -> "+"
   | Minus -> "-"
   | Times -> "*"
   | Div   -> "/"
-  | Mod   -> "mod" 
+  | Mod   -> "mod"
 
-let brel_to_string = function 
+let brel_to_string = function
   | Eq  -> "="
   | Ne  -> "!="
   | Gt  -> ">"
@@ -686,179 +689,179 @@
   | Ueq -> "~~"
   | Une -> "!~"
 
-let print_brel ppf r = 
+let print_brel ppf r =
   F.fprintf ppf "%s" (brel_to_string r)
 
-let print_binding ppf (s,t) = 
+let print_binding ppf (s,t) =
   F.fprintf ppf "%a:%a" Symbol.print s Sort.print t
 
-let bind_to_string  (s,t) = 
+let bind_to_string  (s,t) =
   Printf.sprintf "%s:%s" (Symbol.to_string s) (Sort.to_string t)
 
 let rec print_expr ppf e = match euw e with
-  | Con c -> 
-      F.fprintf ppf "%a" Constant.print c 
-  | MExp es -> 
+  | Con c ->
+      F.fprintf ppf "%a" Constant.print c
+  | MExp es ->
       F.fprintf ppf "[%a]" (Misc.pprint_many false " ; " print_expr) es
-  | Var s -> 
+  | Var s ->
       F.fprintf ppf "%a" Symbol.print s
-  | App (s, es) -> 
-      F.fprintf ppf "%a([%a])" 
+  | App (s, es) ->
+      F.fprintf ppf "%a([%a])"
         Symbol.print s
         (Misc.pprint_many false "; " print_expr) es
   | Bin (e1, op, e2) ->
-      F.fprintf ppf "(%a %s %a)" 
-        print_expr e1 
-        (bop_to_string op) 
+      F.fprintf ppf "(%a %s %a)"
+        print_expr e1
+        (bop_to_string op)
         print_expr e2
   | MBin (e1, ops, e2) ->
-      F.fprintf ppf "(%a [%s] %a)" 
-        print_expr e1 
+      F.fprintf ppf "(%a [%s] %a)"
+        print_expr e1
         (ops |>: bop_to_string |> String.concat " ; ")
         print_expr e2
-  
-  | Ite (ip, te, ee) -> 
-      F.fprintf ppf "if %a then %a else %a" 
-        print_pred ip 
+
+  | Ite (ip, te, ee) ->
+      F.fprintf ppf "if %a then %a else %a"
+        print_pred ip
         print_expr te
         print_expr ee
-  
+
   (* DEPRECATED TO HELP HS Parser
-  | Ite(ip,te,ee) -> 
-      F.fprintf ppf "(%a ? %a : %a)" 
-        print_pred ip 
+  | Ite(ip,te,ee) ->
+      F.fprintf ppf "(%a ? %a : %a)"
+        print_pred ip
         print_expr te
         print_expr ee
-  *)     
+  *)
 
-  | Fld(s, e) -> 
-      F.fprintf ppf "%a.%s" print_expr e s 
+  | Fld(s, e) ->
+      F.fprintf ppf "%a.%s" print_expr e s
   | Cst(e,t) ->
-      F.fprintf ppf "(%a : %a)" 
-        print_expr e 
+      F.fprintf ppf "(%a : %a)"
+        print_expr e
         Sort.print t
   | Bot ->
-      F.fprintf ppf "_|_" 
+      F.fprintf ppf "_|_"
 
 and print_pred ppf p = match puw p with
-  | True -> 
+  | True ->
       F.fprintf ppf "true"
-  | False -> 
+  | False ->
       F.fprintf ppf "false"
   | Bexp (App (s, es), _) ->
       F.fprintf ppf "%a(%a)" Symbol.print s (Misc.pprint_many false ", " print_expr) es
   | Bexp e ->
       F.fprintf ppf "(Bexp %a)" print_expr e
-  | Not p -> 
+  | Not p ->
       F.fprintf ppf "(~ (%a))" print_pred p
-  | Imp (p1, p2) -> 
-      F.fprintf ppf "(%a => %a)" print_pred p1 print_pred p2 
+  | Imp (p1, p2) ->
+      F.fprintf ppf "(%a => %a)" print_pred p1 print_pred p2
   | Iff (p1, p2) ->
-      F.fprintf ppf "(%a <=> %a)" print_pred p1 print_pred p2 
+      F.fprintf ppf "(%a <=> %a)" print_pred p1 print_pred p2
   | And ps -> begin match ps with [] -> F.fprintf ppf "true" | _ ->
       F.fprintf ppf "&& %a" (Misc.pprint_many_brackets true print_pred) ps
     end
-  | Or ps -> begin match ps with [] -> F.fprintf ppf "false" | _ -> 
+  | Or ps -> begin match ps with [] -> F.fprintf ppf "false" | _ ->
       F.fprintf ppf "|| %a" (Misc.pprint_many_brackets true print_pred) ps
     end
 
   | Atom (e1, r, e2) ->
       (* F.fprintf ppf "@[(%a %s %a)@]" *)
       F.fprintf ppf "(%a %s %a)"
-        print_expr e1 
-        (brel_to_string r) 
+        print_expr e1
+        (brel_to_string r)
         print_expr e2
   | MAtom (e1, rs, e2) ->
-      F.fprintf ppf "(%a [%a] %a)" 
+      F.fprintf ppf "(%a [%a] %a)"
       (* F.fprintf ppf "@[(%a [%a] %a)@]"  *)
-        print_expr e1 
+        print_expr e1
         (Misc.pprint_many false " ; " print_brel) rs
         print_expr e2
-  | Forall (qs, p) -> 
-      F.fprintf ppf "forall [%a] . %a" 
+  | Forall (qs, p) ->
+      F.fprintf ppf "forall [%a] . %a"
         (Misc.pprint_many false "; " print_binding) qs
         print_pred p
-  
-let rec expr_to_string e = 
+
+let rec expr_to_string e =
   match euw e with
-  | Con c -> 
+  | Con c ->
       Constant.to_string c
-  | MExp es -> 
+  | MExp es ->
       Printf.sprintf "[%s]" (es |>: expr_to_string |> String.concat " ; ")
-  | Var s -> 
+  | Var s ->
       Symbol.to_string s
   | App (s, es) ->
-      Printf.sprintf "%s([%s])" 
+      Printf.sprintf "%s([%s])"
         (Symbol.to_string s)
         (es |> List.map expr_to_string |> String.concat "; ")
   | Bin (e1, op, e2) ->
-      Printf.sprintf "(%s %s %s)" 
+      Printf.sprintf "(%s %s %s)"
         (expr_to_string e1) (bop_to_string op) (expr_to_string e2)
   | MBin (e1, ops, e2) ->
-      Printf.sprintf "(%s [%s] %s)" 
-        (expr_to_string e1) 
+      Printf.sprintf "(%s [%s] %s)"
+        (expr_to_string e1)
         (ops |> List.map bop_to_string |> String.concat "; ")
         (expr_to_string e2)
-  | Ite(ip,te,ee) -> 
-      Printf.sprintf "(%s ? %s : %s)" 
+  | Ite(ip,te,ee) ->
+      Printf.sprintf "(%s ? %s : %s)"
         (pred_to_string ip) (expr_to_string te) (expr_to_string ee)
-  | Fld(s,e) -> 
-      Printf.sprintf "%s.%s" (expr_to_string e) s 
+  | Fld(s,e) ->
+      Printf.sprintf "%s.%s" (expr_to_string e) s
   | Cst(e,t) ->
       Printf.sprintf "(%s : %s)" (expr_to_string e) (Sort.to_string t)
   | Bot ->
-      Printf.sprintf "_|_" 
+      Printf.sprintf "_|_"
 
 
-and pred_to_string p = 
+and pred_to_string p =
   match puw p with
-    | True -> 
+    | True ->
         "true"
-    | False -> 
+    | False ->
         "false"
     | Bexp e ->
         Printf.sprintf "(Bexp %s)" (expr_to_string e)
-    | Not p -> 
-        Printf.sprintf "(~ (%s))" (pred_to_string p) 
-    | Imp (p1, p2) -> 
+    | Not p ->
+        Printf.sprintf "(~ (%s))" (pred_to_string p)
+    | Imp (p1, p2) ->
         Printf.sprintf "(%s => %s)" (pred_to_string p1) (pred_to_string p2)
     | Iff (p1, p2) ->
         Printf.sprintf "(%s <=> %s)" (pred_to_string p1) (pred_to_string p2)
-    | And ps -> 
+    | And ps ->
         Printf.sprintf "&& [%s]" (List.map pred_to_string ps |> String.concat " ; ")
-    | Or ps -> 
+    | Or ps ->
         Printf.sprintf "|| [%s]" (List.map pred_to_string ps |> String.concat ";")
     | Atom (e1, r, e2) ->
-        Printf.sprintf "(%s %s %s)" 
+        Printf.sprintf "(%s %s %s)"
         (expr_to_string e1) (brel_to_string r) (expr_to_string e2)
     | MAtom (e1, rs, e2) ->
-        Printf.sprintf "(%s [%s] %s)" 
+        Printf.sprintf "(%s [%s] %s)"
         (expr_to_string e1)
-        (List.map brel_to_string rs |> String.concat " ; ") 
+        (List.map brel_to_string rs |> String.concat " ; ")
         (expr_to_string e2)
-    | Forall (qs,p) -> 
-        Printf.sprintf "forall [%s] . %s" 
+    | Forall (qs,p) ->
+        Printf.sprintf "forall [%s] . %s"
         (List.map bind_to_string qs |> String.concat "; ") (pred_to_string p)
 
 let rec pred_map hp he fp fe p =
   let rec pm p =
     try PredHash.find hp p with Not_found -> begin
-      let p' = 
+      let p' =
         match puw p with
-        | True | False as p1 -> 
+        | True | False as p1 ->
             p1
-        | And ps -> 
-            And (List.map pm ps)  
-        | Or ps -> 
-            Or (List.map pm ps)  
-        | Not p -> 
-            Not (pm p) 
-        | Imp (p1, p2) -> 
+        | And ps ->
+            And (List.map pm ps)
+        | Or ps ->
+            Or (List.map pm ps)
+        | Not p ->
+            Not (pm p)
+        | Imp (p1, p2) ->
             Imp (pm p1, pm p2)
         | Iff (p1, p2) ->
             Iff (pm p1, pm p2)
         | Bexp e ->
-            Bexp (expr_map hp he fp fe e) 
+            Bexp (expr_map hp he fp fe e)
         | Atom (e1, r, e2) ->
             Atom (expr_map hp he fp fe e1, r, expr_map hp he fp fe e2)
         | MAtom (e1, rs, e2) ->
@@ -866,19 +869,19 @@
         | Forall (qs, p) ->
             Forall (qs, pm p) in
       let rv = fp (pwr p') in
-      let _  = PredHash.add hp p rv in 
+      let _  = PredHash.add hp p rv in
       rv
-    end in pm p 
+    end in pm p
 
 and expr_map hp he fp fe e =
   let rec em e =
     try ExprHash.find he e with Not_found -> begin
-      let e' = 
+      let e' =
         match euw e with
-        | Con _ | Var _ | Bot as e1 -> 
+        | Con _ | Var _ | Bot as e1 ->
             e1
         | MExp es ->
-            MExp (List.map em es) 
+            MExp (List.map em es)
         | App (f, es) ->
             App (f, List.map em es)
         | Bin (e1, op, e2) ->
@@ -886,11 +889,11 @@
         | MBin (e1, ops, e2) ->
             MBin (em e1, ops, em e2)
         | Ite (ip, te, ee) ->
-            Ite (pred_map hp he fp fe ip, em te, em ee) 
-        | Fld (s, e1) -> 
-            Fld (s, em e1) 
-        | Cst (e1, t) -> 
-            Cst (em e1, t) 
+            Ite (pred_map hp he fp fe ip, em te, em ee)
+        | Fld (s, e1) ->
+            Fld (s, em e1)
+        | Cst (e1, t) ->
+            Cst (em e1, t)
       in
       let rv = fe (ewr e') in
       let _  = ExprHash.add he e rv in
@@ -913,50 +916,50 @@
 
 and expr_iter fp fe ew =
   begin match puw ew with
-    | Con _ | Var _ | Bot -> 
+    | Con _ | Var _ | Bot ->
         ()
     | MExp es ->
         List.iter (expr_iter fp fe) es
-    | App (_, es)  -> 
+    | App (_, es)  ->
         List.iter (expr_iter fp fe) es
-    | Bin (e1, _, e2)  -> 
+    | Bin (e1, _, e2)  ->
         expr_iter fp fe e1; expr_iter fp fe e2
-    | MBin (e1, _, e2)  -> 
+    | MBin (e1, _, e2)  ->
         expr_iter fp fe e1; expr_iter fp fe e2
-    | Ite (ip, te, ee) -> 
+    | Ite (ip, te, ee) ->
         pred_iter fp fe ip; expr_iter fp fe te; expr_iter fp fe ee
-    | Fld (_, e1) | Cst (e1, _) -> 
+    | Fld (_, e1) | Cst (e1, _) ->
         expr_iter fp fe e1
   end;
   fe ew
 
 let esub x e = function
   | (Var y), _ when x = y -> e
-  | _ as e1 -> e1 
+  | _ as e1 -> e1
 
 let expr_subst hp he e x e' =
-  expr_map hp he id (esub x e') e 
+  expr_map hp he id (esub x e') e
 
 let pred_subst hp he p x e' =
-  pred_map hp he id (esub x e') p 
+  pred_map hp he id (esub x e') p
 
-module Expression = 
+module Expression =
   struct
-      
-    module Hash   = ExprHash 
-      
+
+    module Hash   = ExprHash
+
     let to_string = expr_to_string
 
     (* let print     = fun fmt e -> Format.pp_print_string fmt (to_string e)
      *)
     let print = print_expr
-    
+
     let show      = print Format.std_formatter
 
     let map fp fe e =
       let hp = PredHash.create 251 in
-      let he = ExprHash.create 251 in 
-      expr_map hp he fp fe e 
+      let he = ExprHash.create 251 in
+      expr_map hp he fp fe e
 
     let iter fp fe e =
       expr_iter fp fe e
@@ -969,8 +972,8 @@
 
     let support e =
       let xs = ref Symbol.SSet.empty in
-      iter un begin function 
-        | (Var x), _ 
+      iter un begin function
+        | (Var x), _
         | (App (x,_)),_ -> xs := Symbol.SSet.add x !xs
         | _               -> ()
       end e;
@@ -980,26 +983,26 @@
 
     let has_bot p =
       let r = ref false in
-      iter un begin function 
+      iter un begin function
         | Bot, _ -> r := true
         | _      -> ()
-      end p; 
+      end p;
       !r
 
   end
-    
+
 module Predicate = struct
-  module Hash = PredHash 
-	
+  module Hash = PredHash
+
   let to_string = pred_to_string
   let print     = print_pred
   let show      = print Format.std_formatter
-			
+
   let map fp fe p =
 	let hp = PredHash.create 251 in
-	let he = ExprHash.create 251 in 
+	let he = ExprHash.create 251 in
     pred_map hp he fp fe p
-	
+
   let iter fp fe p =
     pred_iter fp fe p
 
@@ -1011,35 +1014,35 @@
 
   let support p =
     let xs = ref Symbol.SSet.empty in
-    iter un begin function 
-      | (Var x), _ 
+    iter un begin function
+      | (Var x), _
       | (App (x,_)),_ -> xs := Symbol.SSet.add x !xs;
       | _               -> ()
-    end p; 
+    end p;
     Symbol.SSet.elements !xs |> List.sort compare
 
   (*
   let size p =
 	let c = ref 0           in
     let f = fun _ -> incr c in
-    let _ = iter f f p      in 
+    let _ = iter f f p      in
     !c
 
   let size p =
 	let c = ref 0                    in
-    let _ = iter (fun _ -> incr c) p in 
+    let _ = iter (fun _ -> incr c) p in
     !c
   *)
-  
+
   let unwrap = puw
 
-  let is_contra = 
+  let is_contra =
     let t = PredHash.create 17 in
     let _ = [pFalse; pNot pTrue; pAtom (zero, Eq, one); pAtom (one, Eq, zero)]
-            |> List.iter (fun p-> PredHash.replace t p ()) in 
-    fun p -> PredHash.mem t p 
-   
+            |> List.iter (fun p-> PredHash.replace t p ()) in
+    fun p -> PredHash.mem t p
 
+
   let rec is_tauto  = function
     | Atom(e1, Eq,  e2), _ -> snd e1 == snd e2
     | Atom(e1, Ueq, e2), _ -> snd e1 == snd e2
@@ -1051,15 +1054,15 @@
 
   let has_bot p =
     let r = ref false in
-    iter un begin function 
+    iter un begin function
       | Bot, _ -> r := true
       | _      -> ()
-    end p; 
+    end p;
     !r
 
   end
 
-let print_stats _ = 
+let print_stats _ =
   Printf.printf "Ast Stats. [none] \n"
 
 
@@ -1071,30 +1074,30 @@
   | Bin (_, Div, _), _ -> true
   | _                  -> false
 
-let pull_divisor = function 
-  | Bin (_, Div, (Con (Constant.Int i),_)), _ -> i 
+let pull_divisor = function
+  | Bin (_, Div, (Con (Constant.Int i),_)), _ -> i
   | _ -> 1
 
 let calc_cm e1 e2 =
-    pull_divisor e1 * pull_divisor e2 
+    pull_divisor e1 * pull_divisor e2
 
-let rec apply_mult m = function 
+let rec apply_mult m = function
   | Bin (e, Div,  (Con (Constant.Int d),_)), _ ->
       let _   = assert ((m/d) * d = m) in
-      eTim ((eCon (Constant.Int (m/d))), e)  
+      eTim ((eCon (Constant.Int (m/d))), e)
   | Bin (e1, op, e2), _ ->
       eBin (apply_mult m e1, op, apply_mult m e2)
-  | Con (Constant.Int i), _ -> 
+  | Con (Constant.Int i), _ ->
       eCon (Constant.Int (i*m))
-  | e -> 
+  | e ->
       eTim (eCon (Constant.Int m), e)
 
-let rec pred_isdiv = function 
-  | True,_ | False,_ -> 
+let rec pred_isdiv = function
+  | True,_ | False,_ ->
       false
-  | And ps,_ | Or ps,_ -> 
+  | And ps,_ | Or ps,_ ->
       List.exists pred_isdiv ps
-  | Not p, _ | Forall (_, p), _ -> 
+  | Not p, _ | Forall (_, p), _ ->
       pred_isdiv p
   | Imp (p1, p2), _ ->
       pred_isdiv p1 || pred_isdiv p2
@@ -1102,29 +1105,29 @@
       pred_isdiv p1 || pred_isdiv p2
   | Bexp e, _ ->
       expr_isdiv e
-  | Atom (e1, _, e2), _ -> 
+  | Atom (e1, _, e2), _ ->
       expr_isdiv e1 || expr_isdiv e2
   | _ -> failwith "Unexpected: pred_isdiv"
 
 let bound m e e1 e2 =
   pAnd [pAtom (apply_mult m e, Gt, apply_mult m e2);
-        pAtom(apply_mult m e, Le, apply_mult m e1)] 
+        pAtom(apply_mult m e, Le, apply_mult m e1)]
 
 let rec fixdiv = function
-  | p when not (pred_isdiv p) -> 
+  | p when not (pred_isdiv p) ->
       p
   | Atom ((Var _,_) as e, Eq, e1), _ | Atom ((Con _, _) as e, Eq, e1), _ ->
       bound (calc_cm e e1) e e1 (eBin (e1, Minus, one))
   | And ps, _ ->
-      pAnd (List.map fixdiv ps) 
+      pAnd (List.map fixdiv ps)
   | Or ps, _ ->
       pOr (List.map fixdiv ps)
   | Imp (p1, p2), _ ->
       pImp (fixdiv p1, fixdiv p2)
   | Iff (p1, p2), _ ->
       pIff (fixdiv p1, fixdiv p2)
-  | Not p, _ -> 
-      pNot (fixdiv p) 
+  | Not p, _ ->
+      pNot (fixdiv p)
   | p -> p
 
 (***************************************************************************)
@@ -1139,66 +1142,66 @@
   | 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,_,_) -> 
+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 
+                   end
   | None        -> None
 
 
-let rec sortcheck_expr g f e = 
+let rec sortcheck_expr g f e =
   match euw e with
-  | Bot   -> 
+  | Bot   ->
       None
-  | Con (Constant.Int _) -> 
-      Some Sort.Int 
-  | Con (Constant.Real _) -> 
-      Some Sort.Real 
+  | Con (Constant.Int _) ->
+      Some Sort.Int
+  | Con (Constant.Real _) ->
+      Some Sort.Real
   | Con (Constant.Lit (_, t)) ->
-      Some t 
+      Some t
   | Var s ->
       sortcheck_sym f s
-  | Bin (e1, op, e2) -> 
+  | Bin (e1, op, e2) ->
       sortcheck_op g f (e1, op, e2)
-  | Ite (p, e1, e2) -> 
-      if sortcheck_pred g f p then 
+  | Ite (p, e1, e2) ->
+      if sortcheck_pred g f p then
         match Misc.map_pair (sortcheck_expr g f) (e1, e2) with
-        | (Some t1, Some t2) when t1 = t2 -> Some t1 
+        | (Some t1, Some t2) when t1 = t2 -> Some t1
         | _ -> None
       else None
-  
+
   | Cst (e1, t) ->
       begin match euw e1 with
         | App (uf, es) -> sortcheck_app g f (Some t) uf es
         | _            ->
             match sortcheck_expr g f e1 with
               | Some t1 when Sort.compat t t1 -> Some t
-              | _                             -> None 
+              | _                             -> None
       end
 
   | App (uf, es) ->
       sortcheck_app g f None uf es
-    
+
   | _ -> assertf "Ast.sortcheck_expr: unhandled expr = %s" (Expression.to_string e)
 
 (* TODO: OMG! 5 levels of matching!!!!! *)
 and sortcheck_app_sub g f so_expected uf es =
   let yikes uf = F.printf "sortcheck_app_sub: unknown sym = %s \n" (Symbol.to_string uf) in
   sortcheck_sym f uf
-  |> function None -> (yikes uf; None) | Some t -> 
-       Sort.func_of_t t 
-       |> function None -> None | Some (tyArity, i_ts, o_t) -> 
-              let _  = asserts (List.length es = List.length i_ts) 
+  |> function None -> (yikes uf; None) | Some t ->
+       Sort.func_of_t t
+       |> function None -> None | Some (tyArity, i_ts, o_t) ->
+              let _  = asserts (List.length es = List.length i_ts)
                          "ERROR: uf arg-arity error: uf=%s" uf in
               let e_ts = es |> List.map (sortcheck_expr g f) |> Misc.map_partial id in
-                if List.length e_ts <> List.length i_ts then 
-                  None 
+                if List.length e_ts <> List.length i_ts then
+                  None
                 else
                   match Sort.unify e_ts i_ts with
                     | None   -> None
@@ -1211,10 +1214,10 @@
                                   | None    -> None
                                   | Some s' -> Some (s', Sort.apply s' t)
 
-and sortcheck_app g f so_expected uf es = 
-  sortcheck_app_sub g f so_expected uf es 
-  |> Misc.maybe_map snd 
-  (* >> begin function 
+and sortcheck_app g f so_expected uf es =
+  sortcheck_app_sub g f so_expected uf es
+  |> Misc.maybe_map snd
+  (* >> begin function
        | Some t -> Format.printf "sortcheck_app: e = %s , t = %s \n"
                      (expr_to_string (eApp (uf, es))) (Sort.to_string t)
        | None   -> Format.printf "sortcheck_app: e = %s FAILS\n"
@@ -1224,33 +1227,33 @@
 
 
 and sortcheck_op g f (e1, op, e2) =
-(* DEBUGGING   
-  let (s1, s2) = Misc.map_pair (sortcheck_expr g f) (e1, e2) in 
-  let _ = match (s1, s2) with 
-    | (Some t1, Some t2) -> F.printf "sortcheck_op : \n%s - %s\n" (Sort.to_string t1) (Sort.to_string t2) 
-    | (_, Some t2) -> F.printf "sortcheck_op1 : \n - %s\n" (Sort.to_string t2) 
-    | (Some t1, _) -> F.printf "sortcheck_op2 : \n%s \n" (Sort.to_string t1) 
-    | (_, _) -> F.printf "sortcheck_op3 : \n" 
+(* DEBUGGING
+  let (s1, s2) = Misc.map_pair (sortcheck_expr g f) (e1, e2) in
+  let _ = match (s1, s2) with
+    | (Some t1, Some t2) -> F.printf "sortcheck_op : \n%s - %s\n" (Sort.to_string t1) (Sort.to_string t2)
+    | (_, Some t2) -> F.printf "sortcheck_op1 : \n - %s\n" (Sort.to_string t2)
+    | (Some t1, _) -> F.printf "sortcheck_op2 : \n%s \n" (Sort.to_string t1)
+    | (_, _) -> F.printf "sortcheck_op3 : \n"
     in *)
   match Misc.map_pair (sortcheck_expr g f) (e1, e2) with
-  | (Some Sort.Int, Some Sort.Int) 
+  | (Some Sort.Int, Some Sort.Int)
   -> Some Sort.Int
 
-  | (Some Sort.Real, Some Sort.Real) 
+  | (Some Sort.Real, Some Sort.Real)
   -> Some Sort.Real
- 
+
   (* only allow when language is Haskell *)
-  | (Some (Sort.Ptr l), Some (Sort.Ptr l')) 
+  | (Some (Sort.Ptr l), Some (Sort.Ptr l'))
   when (l = l' && sortcheck_loc f l = Some Sort.Num)
  -> Some (Sort.Ptr l)
- 
+
   (* only allow when language is C *)
-  | (Some (Sort.Ptr s), Some Sort.Int) 
-  | (Some Sort.Int, Some (Sort.Ptr s)) 
+  | (Some (Sort.Ptr s), Some Sort.Int)
+  | (Some Sort.Int, Some (Sort.Ptr s))
   -> Some (Sort.Ptr s)
 
   (* only allow when language is C *)
-  | (Some (Sort.Ptr s), Some (Sort.Ptr s')) 
+  | (Some (Sort.Ptr s), Some (Sort.Ptr s'))
   when op = Minus && s = s'
   -> Some Sort.Int
 
@@ -1266,15 +1269,20 @@
   | _ , Some Sort.Int,     Some (Sort.Ptr l)
   | _ , Some (Sort.Ptr l), Some Sort.Int
     -> (sortcheck_loc f l = Some Sort.Num)
-  | _ , Some (Sort.Ptr l1), Some (Sort.Ptr l2) 
-    when (sortcheck_loc f l1 = Some Sort.Num) 
-      && (sortcheck_loc f l2 = Some Sort.Num)
-    -> true
+  | _ , Some (Sort.Ptr l1), Some (Sort.Ptr l2)
+    when ((sortcheck_loc f l1 = Some Sort.Num)
+      &&  (sortcheck_loc f l2 = Some Sort.Num))
+      || ((sortcheck_loc f l1 = Some Sort.Frac)
+      &&  (sortcheck_loc f l2 = Some Sort.Frac))
+    -> true   
+  | _ , Some Sort.Real,     Some (Sort.Ptr l)
+  | _ , Some (Sort.Ptr l), Some Sort.Real
+    -> sortcheck_loc f l = Some Sort.Frac
   | Eq, Some t1, Some t2
   | Ne, Some t1, Some t2
     -> t1 = t2
-  | Ueq, Some (Sort.App (_,_)), Some (Sort.App (_,_)) 
-  | Une, Some (Sort.App (_,_)), Some (Sort.App (_,_)) 
+  | Ueq, Some (Sort.App (_,_)), Some (Sort.App (_,_))
+  | Une, Some (Sort.App (_,_)), Some (Sort.App (_,_))
     -> true
   | _ , Some (Sort.App (tc,_)), _
     when (g tc) (* tc is an interpreted tycon *)
@@ -1285,34 +1293,37 @@
 
 and sortcheck_pred g f p =
   match puw p with
-    | True  
-    | False -> 
-        true 
-    | Bexp e ->
+    | True
+    | False ->
+        true
+    | Bexp e ->  
         sortcheck_expr g f e = Some Sort.Bool 
-    | Not p -> 
+    | Not p ->
         sortcheck_pred g f p
-    | Imp (p1, p2) | Iff (p1, p2) -> 
+    | Imp (p1, p2) | Iff (p1, p2) ->
         List.for_all (sortcheck_pred g f) [p1; p2]
-    | And ps  
+    | And ps
     | Or ps ->
         List.for_all (sortcheck_pred g f) ps
-    
-    | Atom (e1, Ueq, e2) 
-      when !Constants.ueq_all_sorts 
-      -> (not (None = sortcheck_expr g f e1)) && 
-         (not (None = sortcheck_expr g f e2)) 
-    
-    | Atom ((Con (Constant.Int(0)),_), _, e) 
-    | Atom (e, _, (Con (Constant.Int(0)),_)) 
+
+    | Atom (e1, Ueq, e2)
+      when !Constants.ueq_all_sorts
+      -> (not (None = sortcheck_expr g f e1)) &&
+         (not (None = sortcheck_expr g f e2))
+
+    | Atom ((Con (Constant.Int(0)),_), _, e)
+    | Atom (e, _, (Con (Constant.Int(0)),_))
       when not (!Constants.strictsortcheck)
       -> not (None = sortcheck_expr g f e)
-    
-    | Atom ((Var x, _) , Eq, (App (uf, es), _))
-    | Atom ((App (uf, es), _), Eq, (Var x, _))
-      -> begin match sortcheck_sym f x with 
-         | None    -> false 
-         | Some tx -> not (None = sortcheck_app g f (Some tx) uf es)
+
+    | Atom (((Con _, _) as e) ,  Eq, (App (uf, es), _))
+    | Atom ((App (uf, es), _), Eq, ((Con _, _) as e))
+    | Atom (((Var _, _) as e) ,  Eq, (App (uf, es), _))
+    | Atom ((App (uf, es), _), Eq, ((Var _, _) as e))
+           (* -> begin match sortcheck_sym f x with *)
+      -> begin match sortcheck_expr g f e with
+         | None   -> false
+         | Some t -> not (None = sortcheck_app g f (Some t) uf es)
          end
 
     | Atom (((App (uf1, e1s), _) as e1), Eq, ((App (uf2, e2s), _) as e2))
@@ -1320,9 +1331,9 @@
          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, 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) 
+               | (Some t1, None)    -> not (None = sortcheck_app g f (Some t1) uf2 e2s)
          end
 
     | Atom (e1, r, e2) ->
@@ -1335,7 +1346,7 @@
 
 (* and sortcheck_pred f p =
   sortcheck_pred' f p
-  >> (fun b -> if not b then F.eprintf "WARNING: Malformed Lhs Pred (%a)\n" Predicate.print p) 
+  >> (fun b -> if not b then F.eprintf "WARNING: Malformed Lhs Pred (%a)\n" Predicate.print p)
  *)
 
 let opt_to_string p = function
@@ -1344,11 +1355,11 @@
 
 
 (* API *)
-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) 
+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
           (*
@@ -1356,7 +1367,7 @@
                       (expr_to_string (eApp (uf, es)))
                       n
                       (Sort.sub_to_string s)
-                      (Sort.to_string t)         
+                      (Sort.to_string t)
                       (opt_to_string Sort.to_string tExp)
           in
              assertf "%s" msg
@@ -1365,7 +1376,7 @@
 
 
 (*
-let sortcheck_pred f p = 
+let sortcheck_pred f p =
   sortcheck_pred f p
   >> (fun b -> ignore <| F.printf "sortcheck_pred: p = %a, res = %b\n"
   Predicate.print p b)
@@ -1379,7 +1390,7 @@
 
 let rec remove_bot pol ((p, _) as pred) =
   match p with
-  | Not p  -> 
+  | Not p  ->
       pNot (remove_bot (not pol) p)
   | Imp (p, q) ->
       pImp (remove_bot (not pol) p, remove_bot pol q)
@@ -1387,31 +1398,31 @@
       pForall (qs, remove_bot pol p)
   | And ps ->
       ps |> List.map (remove_bot pol) |> pAnd
-  | Or ps -> 
+  | Or ps ->
       ps |> List.map (remove_bot pol) |> pOr
   | Bexp e when Expression.has_bot e ->
       pred_of_bool pol
-  | Atom (e1, _, e2) when Expression.has_bot e1 || Expression.has_bot e2 -> 
+  | Atom (e1, _, e2) when Expression.has_bot e1 || Expression.has_bot e2 ->
       pred_of_bool pol
-  | _ -> 
+  | _ ->
       pred
 
-let remove_bot p = 
-  if Predicate.has_bot p 
-  then remove_bot true p 
+let remove_bot p =
+  if Predicate.has_bot p
+  then remove_bot true p
   else p
 
 let symm_brel = function
-  | Eq  -> Eq 
-  | Ueq -> Ueq 
-  | Ne  -> Ne 
-  | Une -> Une 
+  | Eq  -> Eq
+  | Ueq -> Ueq
+  | Ne  -> Ne
+  | Une -> Une
   | Gt  -> Lt
   | Ge  -> Le
   | Lt  -> Gt
   | Le  -> Ge
 
-let neg_brel = function 
+let neg_brel = function
   | Eq  -> Ne
   | Ueq -> Une
   | Ne  -> Eq
@@ -1423,30 +1434,30 @@
 
 let rec push_neg ?(neg=false) ((p, _) as pred) =
   match p with
-    | True   -> 
+    | True   ->
         if neg then pFalse else pred
-    | False  -> 
+    | False  ->
         if neg then pTrue else pred
-    | Bexp _ -> 
+    | Bexp _ ->
         if neg then pNot pred else pred
-    | Not p  -> 
+    | Not p  ->
         push_neg ~neg:(not neg) p
-    | Imp (p, q) -> 
+    | Imp (p, q) ->
 	if neg then pAnd [push_neg p; push_neg ~neg:true q]
 	else pImp (push_neg p, push_neg q)
     | Iff (p, q) ->
         if neg then pIff (p, push_neg ~neg:true q)
         else pIff (push_neg p, push_neg q)
-    | Forall (qs, p) -> 
+    | Forall (qs, p) ->
 	let pred' = pForall (qs, push_neg ~neg:false p) in
 	if neg then pNot pred' else pred'
-    | And ps -> 
-        List.map (push_neg ~neg:neg) ps 
+    | And ps ->
+        List.map (push_neg ~neg:neg) ps
         |> if neg then pOr else pAnd
-    | Or ps -> 
-        List.map (push_neg ~neg:neg) ps 
+    | Or ps ->
+        List.map (push_neg ~neg:neg) ps
         |> if neg then pAnd else pOr
-    | Atom (e1, brel, e2) -> 
+    | Atom (e1, brel, e2) ->
         if neg then pAtom (e1, neg_brel brel, e2) else pred
     | _ -> failwith "Unexpected: push_neg"
 
@@ -1454,15 +1465,15 @@
 let rec simplify_pred ((p, _) as pred) =
   match p with
     | Not p -> pNot (simplify_pred p)
-    | Imp (p, q) -> pImp (simplify_pred p, simplify_pred q) 
+    | Imp (p, q) -> pImp (simplify_pred p, simplify_pred q)
     | Forall (qs, p) -> pForall (qs, simplify_pred p)
-    | And ps -> ps |> List.map simplify_pred 
-                   |> List.filter (not <.> Predicate.is_tauto) 
+    | And ps -> ps |> List.map simplify_pred
+                   |> List.filter (not <.> Predicate.is_tauto)
                    |> (function | []  -> pTrue
                                 | [p] -> p
                                 | _ when List.exists Predicate.is_contra ps -> pFalse
                                 | _   -> pAnd ps)
-    | Or ps -> ps |> List.map simplify_pred 
+    | Or ps -> ps |> List.map simplify_pred
                   |> List.filter (not <.> Predicate.is_contra)
                   |> (function []  -> pFalse
                              | [p] -> p
@@ -1477,13 +1488,13 @@
 module Subst = struct
 
   type t = expr Symbol.SMap.t
- 
-  let valid xes = 
-    xes |> List.split 
+
+  let valid xes =
+    xes |> List.split
         |> Misc.app_snd (Misc.flap Expression.support)
         |> Misc.uncurry Misc.disjoint
-            
-    
+
+
   let extend s (x, e) =
     let s = Symbol.SMap.map (esub x e) s in
       if Symbol.SMap.mem x s then
@@ -1495,18 +1506,18 @@
 
   let empty     = Symbol.SMap.empty
   let is_empty  = Symbol.SMap.is_empty
-  let to_list   = Symbol.SMap.to_list   
+  let to_list   = Symbol.SMap.to_list
   let apply     = Misc.flip Symbol.SMap.maybe_find
   let of_list   = fun xes -> List.fold_left extend empty xes
   let simultaneous_of_list = Symbol.SMap.of_list
-  let compose s t = 
+  let compose s t =
     let s' = Symbol.SMap.fold (fun x e s -> Symbol.SMap.map (esub x e) s) t s
     in Symbol.SMap.fold (fun x e s -> if Symbol.SMap.mem x s
                                          then s else Symbol.SMap.add x e s)
                         t s'
   let print_sub = fun ppf (x,e) -> F.fprintf ppf "[%a:=%a]" Symbol.print x Expression.print e
   let print     = fun ppf -> to_list <+> F.fprintf ppf "%a" (Misc.pprint_many false "" print_sub)
-      
+
 (* fun s1 s2 -> Symbol.SMap.fold (fun x e s -> extend s (x, e)) s2 s1 *)
 (*   let apply     = Misc.flip Symbol.SMap.maybe_find *)
 
@@ -1518,25 +1529,25 @@
 (**************************************************************************)
 
 module Horn = struct
-  
+
   type pr = string * string list
   type gd = C of pred | K of pr
-  type t  = pr * gd list 
+  type t  = pr * gd list
 
-  let print_pr ppf (x, xs) = 
-    Format.fprintf ppf "%s(%s)" x (String.concat "," xs) 
-    
-  let print_gd ppf = function 
+  let print_pr ppf (x, xs) =
+    Format.fprintf ppf "%s(%s)" x (String.concat "," xs)
+
+  let print_gd ppf = function
     | C p -> Predicate.print ppf p
-    | K x -> print_pr ppf x 
+    | K x -> print_pr ppf x
 
-  let print ppf (hd, gds) = 
-    Format.fprintf ppf "%a :- %a." 
-      print_pr hd 
+  let print ppf (hd, gds) =
+    Format.fprintf ppf "%a :- %a."
+      print_pr hd
       (Misc.pprint_many false "," print_gd) gds
 
-  let support_pr = snd 
-  let support_gd = function K pr -> support_pr pr | C p  -> p |> Predicate.support |> List.map Symbol.to_string 
+  let support_pr = snd
+  let support_gd = function K pr -> support_pr pr | C p  -> p |> Predicate.support |> List.map Symbol.to_string
   let support    = fun (hd, gds) -> (support_pr hd) ++ (Misc.flap support_gd gds)
 end
 
@@ -1544,11 +1555,11 @@
 let simplify_pred = remove_bot <+> simplify_pred
 
 
-let esub_su su e = match e with 
+let esub_su su e = match e with
   | ((Var y), _) -> Misc.maybe_default (Subst.apply su y) e
   | _            -> e
 
-(* ORIG 
+(* ORIG
    let substs_pred   = fun p su -> su |> Subst.to_list |> Predicate.substs p |> simplify_pred
 *)
 
@@ -1560,10 +1571,10 @@
 (****************************************************************************)
 
 
-exception DoesNotUnify 
+exception DoesNotUnify
 
-let rec pUnify (p1, p2) = 
-  let res = 
+let rec pUnify (p1, p2) =
+  let res =
     match p1, p2 with
   | (Atom (e1, r1, e1'), _), (Atom (e2, r2, e2'), _) when r1 = r2 ->
       let s1       = eUnify (e1, e2) in
@@ -1576,22 +1587,22 @@
       pUnify (p1, p2)
   | (Imp (p1, p1'), _), (Imp (p2, p2'), _) ->
       psUnify ([p1; p1'], [p2; p2'])
-  
-  | (And p1s, _), (And p2s, _) 
-  | (Or p1s, _), (Or p2s, _) 
+
+  | (And p1s, _), (And p2s, _)
+  | (Or p1s, _), (Or p2s, _)
     when List.length p1s = List.length p2s ->
       psUnify (p1s, p2s)
   | _, _ -> raise DoesNotUnify
   in
-  let _ = if mydebug then 
-          (Format.printf "pUnify: p1 is %a, p2 is %a, subst = %a \n" 
+  let _ = if mydebug then
+          (Format.printf "pUnify: p1 is %a, p2 is %a, subst = %a \n"
           Predicate.print p1 Predicate.print p2 Subst.print (Subst.of_list res)) in
   res
 
 and psUnify (p1s, p2s) =
   let _ = asserts (List.length p1s = List.length p2s) "psUnify" in
   List.fold_left2 begin fun s p1 p2 ->
-    (p1, p2) 
+    (p1, p2)
     |> Misc.map_pair (fun p -> Predicate.substs p s)
     |> pUnify
     |> (fun s' -> s' ++ s)
@@ -1614,22 +1625,22 @@
       esUnify (e1s, e2s)
   | e, (Var x, _) | (Var x, _), e when Symbol.is_wild x ->
       [(x, e)]
-  | _, _ -> raise DoesNotUnify 
+  | _, _ -> raise DoesNotUnify
 
 and esUnify (e1s, e2s) =
   let _ = asserts (List.length e1s = List.length e2s) "esUnify" in
   List.fold_left2 begin fun s e1 e2 ->
-    (e1, e2) 
+    (e1, e2)
     |> Misc.map_pair (fun e -> Expression.substs e s)
     |> eUnify
     |> (fun s' -> s' ++ s)
   end [] e1s e2s
 
 (* API *)
-let unify_pred p1 p2 = try pUnify (p1, p2) |> Subst.of_list |> some with DoesNotUnify -> None 
+let unify_pred p1 p2 = try pUnify (p1, p2) |> Subst.of_list |> some with DoesNotUnify -> None
 let into_of_expr = function Con (Constant.Int i), _  -> Some i | _ -> None
 
-let symm_pred = function 
+let symm_pred = function
   | Atom (e1, r, e2), _ -> pAtom (e2, symm_brel r, e1)
   | p                   -> p
 
@@ -1637,11 +1648,11 @@
 let rec expr_subst hp he e x e' =
   let rec esub e =
     try ExprHash.find he e with Not_found -> begin
-      let rv = 
+      let rv =
         match euw e with
         | Var y when x = y ->
-            e' 
-        | Con _ | Var _ -> 
+            e'
+        | Con _ | Var _ ->
             e
         | App (s, es) ->
             App (s, List.map esub es) |> ewr
@@ -1652,7 +1663,7 @@
         | Fld (s, e1) ->
             Fld (s, esub e1) |> ewr in
       let _  = ExprHash.add he e rv in
-      rv 
+      rv
     end in esub e
 
 and pred_subst hp he e x e' =
@@ -1671,7 +1682,7 @@
       | Atom (_) -> e
       | Leq(x,y) -> pwr (Leq(expr_subst h he x v vv, expr_subst h he y v vv))
   in s e
-}}} *)  
+}}} *)
 (** {{{
       let rec support pred =
         let h = Hash.create 251 in
@@ -1687,14 +1698,14 @@
           and s1 exp =
             match euw exp with
                 Constant(_) -> ()
-              | Application (func, args) -> 
+              | Application (func, args) ->
                   add func; List.iter s args
               | Variable(sym) -> add sym
               | Sum(args) -> List.iter s args
               | Coeff(c,t) -> s t
               | Ite _ -> failwith "ite not supported"
           in s exp in
-          
+
         let rec s exp =
           try Hash.find h exp with
               Not_found -> Hash.add h exp (); s1 exp
@@ -1710,32 +1721,32 @@
             | Leq (x,y) -> se x; se y
             | Atom (s) -> ()
         in s pred; List.rev !res
-        
+
       let h = PredHash.create 251 in
         let rec ip p =
           let _ = f p in
           if not (PredHash.mem h p) then begin
             let _ = PredHash.add h p () in
             match puw p with
-            | And ps | Or ps -> 
+            | And ps | Or ps ->
                 List.iter ip plist
-            | Not p  | Forall (_,p) -> 
-                ip p 
-            | Imp (p1, p2) -> 
+            | Not p  | Forall (_,p) ->
+                ip p
+            | Imp (p1, p2) ->
                 ip p1; ip p2
             | _ -> ()
           end in
-        ip p 
+        ip p
    }}} *)
 (* {{{
-  
+
       (* Translate predicate to a satisfiability-equivalent predicate without Ite *)
-      
+
       let temp_ctr = ref 0
       let new_temp () =
 	let n = "$$$" ^ (string_of_int !temp_ctr) in
 	  (temp_ctr := !temp_ctr + 1; n)
-	  
+
       let elim_ite sp =
 	let cnsts = ref [] in
 	let he = Expression.Hash.create 251 in
@@ -1746,7 +1757,7 @@
 	and te1 e =
 	  match euw e with
 	      Constant(c) -> e
-	    | Application (func, args) -> 
+	    | Application (func, args) ->
 		ewr (Application (func, List.map te args))
 	    | Variable(v) -> ewr (Variable(v))
 	    | Sum(args) -> ewr (Sum(List.map te args))
@@ -1760,7 +1771,7 @@
 		    cnsts := pwr (Or [i; pwr (Equality(temp,(ev)))]) :: (!cnsts);
 		    temp
 		  end
-	and tp p = 
+	and tp p =
 	  try Hash.find hp p
 	  with Not_found -> (let foo = tp1 p in Hash.add hp p foo; foo)
 	and tp1 p =
diff --git a/external/fixpoint/ast.mli b/external/fixpoint/ast.mli
--- a/external/fixpoint/ast.mli
+++ b/external/fixpoint/ast.mli
@@ -53,6 +53,7 @@
     val to_string   : t -> string
     val print       : Format.formatter -> t -> unit
     val t_num       : t
+    val t_frac      : t
     val t_obj       : t
     val t_bool      : t
     val t_int       : t
diff --git a/external/fixpoint/fixLex.mll b/external/fixpoint/fixLex.mll
--- a/external/fixpoint/fixLex.mll
+++ b/external/fixpoint/fixLex.mll
@@ -131,6 +131,7 @@
   | "mod"               { MOD }
   | "obj"               { OBJ }
   | "num"               { NUM }
+  | "frac"              { FRAC }
   | "int"               { INT }
   | "real"              { REAL }
   | "ptr"               { PTR }
diff --git a/external/fixpoint/fixParse.mly b/external/fixpoint/fixParse.mly
--- a/external/fixpoint/fixParse.mly
+++ b/external/fixpoint/fixParse.mly
@@ -71,7 +71,7 @@
 %token TIMES 
 %token DIV 
 %token QM DOT ASGN
-%token OBJ REAL INT NUM PTR LFUN BOOL UNINT FUNC LIT
+%token OBJ REAL INT NUM PTR LFUN BOOL UNINT FUNC LIT FRAC
 %token SRT AXM CON CST WF SOL QUL KUT BIND ADP DDP
 %token ENV GRD LHS RHS REF
 
@@ -172,6 +172,7 @@
   | PTR LPAREN Id RPAREN                { So.t_ptr (So.Loc $3) }
   | OBJ                                 { So.t_obj } 
   | NUM                                 { So.t_num } 
+  | FRAC                                { So.t_frac } 
   | TVAR LPAREN Num RPAREN              { So.t_generic $3 }
   | FUNC LPAREN sorts RPAREN            { So.t_func 0 $3  }
   | FUNC LPAREN Num COMMA sorts RPAREN  { So.t_func $3 $5 }
diff --git a/external/fixpoint/fixpoint.native-i386-linux b/external/fixpoint/fixpoint.native-i386-linux
Binary files a/external/fixpoint/fixpoint.native-i386-linux 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
# file too large to diff: external/fixpoint/fixpoint.native-i686-w64-mingw32
diff --git a/external/fixpoint/fixpoint.native-x86_64-darwin b/external/fixpoint/fixpoint.native-x86_64-darwin
# 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
# file too large to diff: external/fixpoint/fixpoint.native-x86_64-linux
diff --git a/external/fixpoint/predAbs.ml b/external/fixpoint/predAbs.ml
--- a/external/fixpoint/predAbs.ml
+++ b/external/fixpoint/predAbs.ml
@@ -690,64 +690,6 @@
   let (ch, me) = refine me c in
   (ch, {me with seen = IS.add (C.id_of_t c) me.seen})
 
-(* LAZYINST 
-let refine me c  =
-  let lps        = lazy (get_lhs me c)                                     in
-  let (_,_,ra2s) as r = C.rhs_of_t c                                       in
-  let (ins, rcs) = BS.time "rhs_cands" (Misc.flap (rhs_cands me lps)) ra2s in
-  if rcs = [] then 
-    let _ = me.stat_emptyRHS += 1 in
-    (false, me)
-  else if BS.time "lhs_contra" (List.exists P.is_contra) (Lazy.force lps) then 
-    let _ = me.stat_unsatLHS += 1               in
-    let _ = me.stat_umatches += List.length rcs in
-    (ch, me)
-  else
-    let lps     = Lazy.force lps                                      in
-    let rcs     = List.filter (fun (_,p) -> not (P.is_contra p)) rcs  in
-    let lt      = PH.create 17                                        in
-    let _       = List.iter (fun p -> PH.add lt p ()) lps             in
-    let (x1,x2) = List.partition (fun (_,p) -> PH.mem lt p) rcs       in
-    let _       = me.stat_matches += (List.length x1)                 in
-    let kqs1    = List.map fst x1                                     in
-    (if C.is_simple c 
-     then (ignore(me.stat_simple_refines += 1); kqs1) 
-     else let senv = C.senv_of_t c in
-          let vv   = C.vv_of_t c   in
-          let t    = C.sort_of_t c in
-          kqs1 ++ (BS.time "check tp" (check_tp me senv vv t lps) x2))
-    |> p_update me (get_rhs_kvars c)
-    |> (fun (ch', z) -> (ch || ch', z))
-
-let refine me c =
-  let (_,_,ra2s) as r2 = C.rhs_of_t c in
-  let k2s = r2 |> C.kvars_of_reft |> List.map snd in
-  let rcs = BS.time "rhs_cands" (Misc.flap (rhs_cands me c)) ra2s in
-  if rcs  = [] then
-    let _ = me.stat_emptyRHS += 1 in
-    (false, me)
-  else
-    let lps = BS.time "preds_of_lhs" (C.preds_of_lhs (read me)) c in
-    if BS.time "lhs_contra" (List.exists P.is_contra) lps then 
-    let _ = me.stat_unsatLHS += 1 in
-    let _ = me.stat_umatches += List.length rcs in
-    (false, me)
-  else 
-    let rcs     = List.filter (fun (_,p) -> not (P.is_contra p)) rcs in
-    let lt      = PH.create 17 in
-    let _       = List.iter (fun p -> PH.add lt p ()) lps in
-    let (x1,x2) = List.partition (fun (_,p) -> PH.mem lt p) rcs in
-    let _       = me.stat_matches += (List.length x1) in
-    let kqs1    = List.map fst x1 in
-    (if C.is_simple c 
-     then (ignore(me.stat_simple_refines += 1); kqs1) 
-     else let senv = C.senv_of_t c in
-          let vv   = C.vv_of_t c   in
-          let t    = C.sort_of_t c in
-          kqs1 ++ (BS.time "check tp" (check_tp me senv vv t lps) x2))
-    |> p_update me k2s
-*)
-
 let refine me c = 
   let me      = me |> (!Co.cex <?> cx_iter c)     in
   let (b, me) = refine me c                       in
diff --git a/external/ocamlgraph/src/dot_lexer.ml b/external/ocamlgraph/src/dot_lexer.ml
new file mode 100644
--- /dev/null
+++ b/external/ocamlgraph/src/dot_lexer.ml
@@ -0,0 +1,386 @@
+# 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
new file mode 100644
--- /dev/null
+++ b/external/ocamlgraph/src/dot_parser.ml
@@ -0,0 +1,551 @@
+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;;
+# 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"
+
+# 37 "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 } )
+# 199 "src/dot_parser.ml"
+               : Dot_ast.file))
+; (fun __caml_parser_env ->
+    Obj.repr(
+# 53 "src/dot_parser.mly"
+                ( false )
+# 205 "src/dot_parser.ml"
+               : 'strict_opt))
+; (fun __caml_parser_env ->
+    Obj.repr(
+# 54 "src/dot_parser.mly"
+                ( true )
+# 211 "src/dot_parser.ml"
+               : 'strict_opt))
+; (fun __caml_parser_env ->
+    Obj.repr(
+# 58 "src/dot_parser.mly"
+          ( false )
+# 217 "src/dot_parser.ml"
+               : 'graph_or_digraph))
+; (fun __caml_parser_env ->
+    Obj.repr(
+# 59 "src/dot_parser.mly"
+          ( true )
+# 223 "src/dot_parser.ml"
+               : 'graph_or_digraph))
+; (fun __caml_parser_env ->
+    Obj.repr(
+# 63 "src/dot_parser.mly"
+                ( [] )
+# 229 "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 )
+# 236 "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] )
+# 244 "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 )
+# 253 "src/dot_parser.ml"
+               : 'list1_stmt))
+; (fun __caml_parser_env ->
+    Obj.repr(
+# 73 "src/dot_parser.mly"
+                ( () )
+# 259 "src/dot_parser.ml"
+               : 'semicolon_opt))
+; (fun __caml_parser_env ->
+    Obj.repr(
+# 74 "src/dot_parser.mly"
+                ( () )
+# 265 "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 )
+# 272 "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 )
+# 279 "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 )
+# 286 "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) )
+# 294 "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 )
+# 301 "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) )
+# 309 "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) )
+# 318 "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 )
+# 325 "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 )
+# 332 "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 )
+# 339 "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 )
+# 347 "src/dot_parser.ml"
+               : 'edge_rhs))
+; (fun __caml_parser_env ->
+    Obj.repr(
+# 104 "src/dot_parser.mly"
+                ( [] )
+# 353 "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 )
+# 361 "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 )
+# 368 "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 )
+# 375 "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 )
+# 383 "src/dot_parser.ml"
+               : 'node_id))
+; (fun __caml_parser_env ->
+    Obj.repr(
+# 118 "src/dot_parser.mly"
+                ( None )
+# 389 "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 )
+# 396 "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) )
+# 404 "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) )
+# 415 "src/dot_parser.ml"
+               : 'port))
+; (fun __caml_parser_env ->
+    Obj.repr(
+# 133 "src/dot_parser.mly"
+                ( [] )
+# 421 "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 )
+# 428 "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] )
+# 435 "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 )
+# 443 "src/dot_parser.ml"
+               : 'attr_list))
+; (fun __caml_parser_env ->
+    Obj.repr(
+# 143 "src/dot_parser.mly"
+                ( None )
+# 449 "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 )
+# 456 "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] )
+# 464 "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 )
+# 473 "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 )
+# 480 "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 )
+# 488 "src/dot_parser.ml"
+               : 'equality))
+; (fun __caml_parser_env ->
+    Obj.repr(
+# 158 "src/dot_parser.mly"
+                ( () )
+# 494 "src/dot_parser.ml"
+               : 'comma_opt))
+; (fun __caml_parser_env ->
+    Obj.repr(
+# 159 "src/dot_parser.mly"
+                ( () )
+# 500 "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 )
+# 507 "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) )
+# 515 "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) )
+# 522 "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) )
+# 529 "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
new file mode 100644
--- /dev/null
+++ b/external/ocamlgraph/src/dot_parser.mli
@@ -0,0 +1,21 @@
+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
new file mode 100644
--- /dev/null
+++ b/external/ocamlgraph/src/gml.ml
@@ -0,0 +1,670 @@
+# 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
new file mode 100644
--- /dev/null
+++ b/external/ocamlgraph/src/version.ml
@@ -0,0 +1,2 @@
+let version = "0.99b"
+let date = "Fri Mar 27 20:20:48 UTC 2015"
diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal
--- a/liquid-fixpoint.cabal
+++ b/liquid-fixpoint.cabal
@@ -1,5 +1,5 @@
 name:                liquid-fixpoint
-version:             0.2.3.1
+version:             0.2.3.2
 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
diff --git a/src/Language/Fixpoint/Bitvector.hs b/src/Language/Fixpoint/Bitvector.hs
--- a/src/Language/Fixpoint/Bitvector.hs
+++ b/src/Language/Fixpoint/Bitvector.hs
@@ -1,20 +1,20 @@
-{-# LANGUAGE DeriveGeneric             #-}
-{-# LANGUAGE DeriveDataTypeable        #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveGeneric      #-}
 
 module Language.Fixpoint.Bitvector
        ( -- * Constructor
          Bv (..)
-       
-         -- * Sizes 
+
+         -- * Sizes
        , BvSize (..)
 
          -- * Operators
        , BvOp (..)
 
          -- * BitVector Sort Constructor
-       , mkSort 
+       , mkSort
 
-         -- * BitVector Expression Constructor 
+         -- * BitVector Expression Constructor
        , eOp
 
          -- * BitVector Type Constructor
@@ -22,14 +22,14 @@
 
        ) where
 
-import qualified Data.Text as T
-import Language.Fixpoint.Types
-import Language.Fixpoint.Names
-import GHC.Generics         (Generic)
-import Data.Typeable        (Typeable)
-import Data.Generics        (Data)
+import           Data.Generics           (Data)
+import qualified Data.Text               as T
+import           Data.Typeable           (Typeable)
+import           GHC.Generics            (Generic)
+import           Language.Fixpoint.Names
+import           Language.Fixpoint.Types
 
-data Bv     = Bv BvSize String 
+data Bv     = Bv BvSize String
 
 data BvSize = S32   | S64
               deriving (Eq, Ord, Show, Data, Typeable, Generic)
@@ -60,12 +60,11 @@
 opName BvOr  = dummyLoc bvOrName
 
 sizeSort     = (`FApp` [fObj $ dummyLoc $ symbol "obj"]) . sizeTC
-sizeTC       = symbolFTycon . dummyLoc . sizeName 
+sizeTC       = symbolFTycon . dummyLoc . sizeName
 sizeName S32 = size32Name
 sizeName S64 = size64Name
 
 bvTyCon      = symbolFTycon $ dummyLoc bitVecName
 
--- s32TyCon     = symbolFTycon $ dummyLoc size32Name 
+-- s32TyCon     = symbolFTycon $ dummyLoc size32Name
 -- s64TyCon     = symbolFTycon $ dummyLoc size64Name
-
diff --git a/src/Language/Fixpoint/Config.hs b/src/Language/Fixpoint/Config.hs
--- a/src/Language/Fixpoint/Config.hs
+++ b/src/Language/Fixpoint/Config.hs
@@ -1,7 +1,7 @@
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE DeriveGeneric             #-}
 {-# LANGUAGE DeriveDataTypeable        #-}
+{-# LANGUAGE DeriveGeneric             #-}
 {-# LANGUAGE FlexibleInstances         #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE UndecidableInstances      #-}
 
 
@@ -11,17 +11,17 @@
   , SMTSolver (..)
   , GenQualifierSort (..)
   , UeqAllSorts (..)
-  , withTarget 
+  , withTarget
   , withUEqAllSorts
-) where  
-  
-import Language.Fixpoint.Files
-import System.FilePath       
-import System.Console.CmdArgs.Default
-import Data.Typeable        (Typeable)
-import Data.Generics        (Data)
+) where
 
+import           Data.Generics                  (Data)
+import           Data.Typeable                  (Typeable)
+import           Language.Fixpoint.Files
+import           System.Console.CmdArgs.Default
+import           System.FilePath
 
+
 class Command a  where
   command :: a -> String
 
@@ -29,11 +29,11 @@
 -- Configuration Options -----------------------------------------------
 ------------------------------------------------------------------------
 
-withTarget        :: Config -> FilePath -> Config 
+withTarget        :: Config -> FilePath -> Config
 withTarget cfg fq = cfg { inFile = fq } { outFile = fq `withExt` Out }
 
-data Config 
-  = Config { 
+data Config
+  = Config {
       inFile      :: FilePath         -- target fq-file
     , outFile     :: FilePath         -- output file
     , solver      :: SMTSolver        -- which SMT solver to use
@@ -46,24 +46,24 @@
 instance Default Config where
   def = Config "" def def def def def def
 
-instance Command Config where 
-  command c =  command (genSorts c)    
-            ++ command (ueqAllSorts c) 
-            ++ command (solver c) 
-            ++ " -out " 
+instance Command Config where
+  command c =  command (genSorts c)
+            ++ command (ueqAllSorts c)
+            ++ command (solver c)
+            ++ " -out "
             ++ (outFile c) ++ " " ++ (inFile c)
 
 ---------------------------------------------------------------------------------------
--- newtype OFilePath = O FilePath 
+-- newtype OFilePath = O FilePath
 --     deriving (Eq, Data,Typeable,Show)
--- 
--- instance Default OFilePath where 
+--
+-- instance Default OFilePath where
 --   def = O "out"
--- 
--- instance Command OFilePath where 
+--
+-- instance Command OFilePath where
 --   command (O s) = " -out " ++ s
 
-newtype GenQualifierSort = GQS Bool 
+newtype GenQualifierSort = GQS Bool
     deriving (Eq, Data,Typeable,Show)
 
 instance Default GenQualifierSort where
@@ -71,9 +71,9 @@
 
 instance Command GenQualifierSort where
   command (GQS True)  = ""
-  command (GQS False) = "-no-gen-qual-sorts" 
+  command (GQS False) = "-no-gen-qual-sorts"
 
-newtype UeqAllSorts = UAS Bool 
+newtype UeqAllSorts = UAS Bool
     deriving (Eq, Data,Typeable,Show)
 
 instance Default UeqAllSorts where
@@ -81,7 +81,7 @@
 
 instance Command UeqAllSorts where
   command (UAS True)  = " -ueq-all-sorts "
-  command (UAS False) = "" 
+  command (UAS False) = ""
 
 withUEqAllSorts c b = c { ueqAllSorts = UAS b }
 
@@ -90,13 +90,13 @@
 data SMTSolver = Z3 | Cvc4 | Mathsat | Z3mem
                  deriving (Eq,Data,Typeable)
 
-instance Command SMTSolver where 
+instance Command SMTSolver where
   command s = " -smtsolver " ++ show s
 
 instance Default SMTSolver where
   def = Z3
 
-instance Show SMTSolver where 
+instance Show SMTSolver where
   show Z3      = "z3"
   show Cvc4    = "cvc4"
   show Mathsat = "mathsat"
@@ -109,6 +109,4 @@
 smtSolver other     = error $ "ERROR: unsupported SMT Solver = " ++ other
 
 -- defaultSolver       :: Maybe SMTSolver -> SMTSolver
--- defaultSolver       = fromMaybe Z3 
-
-
+-- defaultSolver       = fromMaybe Z3
diff --git a/src/Language/Fixpoint/Errors.hs b/src/Language/Fixpoint/Errors.hs
--- a/src/Language/Fixpoint/Errors.hs
+++ b/src/Language/Fixpoint/Errors.hs
@@ -1,7 +1,7 @@
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE FlexibleInstances         #-}
 {-# LANGUAGE DeriveDataTypeable        #-}
 {-# LANGUAGE DeriveGeneric             #-}
+{-# LANGUAGE FlexibleInstances         #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
 
 module Language.Fixpoint.Errors (
   -- * Concrete Location Type
@@ -29,52 +29,52 @@
 
   ) where
 
-import System.FilePath 
-import Text.PrettyPrint.HughesPJ
-import Text.Parsec.Pos                   
-import Data.Typeable
-import Data.Generics        (Data)
-import Text.Printf 
-import Data.Hashable
-import Control.Exception
-import qualified Control.Monad.Error as E 
-import Language.Fixpoint.PrettyPrint
-import Language.Fixpoint.Types
-import GHC.Generics         (Generic)
+import           Control.Exception
+import qualified Control.Monad.Error           as E
+import           Data.Generics                 (Data)
+import           Data.Hashable
+import           Data.Typeable
+import           GHC.Generics                  (Generic)
+import           Language.Fixpoint.PrettyPrint
+import           Language.Fixpoint.Types
+import           System.FilePath
+import           Text.Parsec.Pos
+import           Text.PrettyPrint.HughesPJ
+import           Text.Printf
 
 -----------------------------------------------------------------------
 -- | A Reusable SrcSpan Type ------------------------------------------
 -----------------------------------------------------------------------
 
-data SrcSpan = SS { sp_start :: !SourcePos, sp_stop :: !SourcePos} 
+data SrcSpan = SS { sp_start :: !SourcePos, sp_stop :: !SourcePos}
                  deriving (Eq, Ord, Show, Data, Typeable, Generic)
 
 instance PPrint SrcSpan where
   pprint = ppSrcSpan
 
 -- ppSrcSpan_short z = parens
---                   $ text (printf "file %s: (%d, %d) - (%d, %d)" (takeFileName f) l c l' c')  
---   where 
+--                   $ text (printf "file %s: (%d, %d) - (%d, %d)" (takeFileName f) l c l' c')
+--   where
 --     (f,l ,c )     = sourcePosElts $ sp_start z
 --     (_,l',c')     = sourcePosElts $ sp_stop  z
 
 
-ppSrcSpan z       = text (printf "%s:%d:%d-%d:%d" f l c l' c')  
-                -- parens $ text (printf "file %s: (%d, %d) - (%d, %d)" (takeFileName f) l c l' c')  
-  where 
+ppSrcSpan z       = text (printf "%s:%d:%d-%d:%d" f l c l' c')
+                -- parens $ text (printf "file %s: (%d, %d) - (%d, %d)" (takeFileName f) l c l' c')
+  where
     (f,l ,c )     = sourcePosElts $ sp_start z
     (_,l',c')     = sourcePosElts $ sp_stop  z
 
 sourcePosElts s = (src, line, col)
-  where 
-    src         = sourceName   s 
+  where
+    src         = sourceName   s
     line        = sourceLine   s
-    col         = sourceColumn s 
+    col         = sourceColumn s
 
-instance Hashable SourcePos where 
+instance Hashable SourcePos where
   hashWithSalt i   = hashWithSalt i . sourcePosElts
 
-instance Hashable SrcSpan where 
+instance Hashable SrcSpan where
   hashWithSalt i z = hashWithSalt i (sp_start z, sp_stop z)
 
 
@@ -94,8 +94,8 @@
 
 instance PPrint Error where
   pprint (Error l msg) = ppSrcSpan l <> text (": Error: " ++ msg)
-                         -- text $ printf "%s\n  %s\n" (showpp l) msg 
-                         
+                         -- text $ printf "%s\n  %s\n" (showpp l) msg
+
 instance Fixpoint Error where
   toFix = pprint
 
@@ -103,15 +103,15 @@
 
 instance E.Error Error where
   strMsg = Error dummySpan
- 
-dummySpan = SS l l  
+
+dummySpan = SS l l
   where l = initialPos ""
 
 
 ---------------------------------------------------------------------
 catMessage :: Error -> String -> Error
 ---------------------------------------------------------------------
-catMessage err msg = err {errMsg = msg ++ errMsg err} 
+catMessage err msg = err {errMsg = msg ++ errMsg err}
 
 ---------------------------------------------------------------------
 catError :: Error -> Error -> Error
@@ -129,4 +129,3 @@
 die :: Error -> a
 ---------------------------------------------------------------------
 die = throw
-
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
@@ -29,11 +29,11 @@
 
 ) where
 
-import qualified Control.Exception            as Ex
-import           Control.Monad -- .State
-import           Data.Functor                 ((<$>))
-import           Data.List                    hiding (find)
-import           Data.Maybe                   (fromMaybe)
+import qualified Control.Exception      as Ex
+import           Control.Monad
+import           Data.Functor           ((<$>))
+import           Data.List              hiding (find)
+import           Data.Maybe             (fromMaybe)
 import           System.Directory
 import           System.Environment
 import           System.FilePath
@@ -63,11 +63,11 @@
 data Ext = Cgi    -- ^ Constraint Generation Information
          | Fq     -- ^ Input to constraint solving (fixpoint)
          | Out    -- ^ Output from constraint solving (fixpoint)
-         | Html   -- ^ HTML file with inferred type annotations 
-         | Annot  -- ^ Text file with inferred types 
-         | Vim    -- ^ Vim annotation file 
-         | Hs     -- ^ Haskell source 
-         | LHs    -- ^ Literate Haskell source 
+         | Html   -- ^ HTML file with inferred type annotations
+         | Annot  -- ^ Text file with inferred types
+         | Vim    -- ^ Vim annotation file
+         | Hs     -- ^ Haskell source
+         | LHs    -- ^ Literate Haskell source
          | Js     -- ^ JavaScript source
          | Ts     -- ^ Typescript source
          | Spec   -- ^ Spec file (e.g. include/Prelude.spec)
@@ -108,7 +108,7 @@
     go Saved  = ".bak"
     go Cache  = ".err"
     go Smt2   = ".smt2"
-    go _      = errorstar $ "extMap: Unknown extension " ++ show e
+    -- go _      = errorstar $ "extMap: Unknown extension " ++ show e
 
 withExt         :: FilePath -> Ext -> FilePath
 withExt f ext   =  replaceExtension f (extMap ext)
@@ -121,8 +121,8 @@
     ext         = extMap e
 
 tempDirectory   :: FilePath -> FilePath
-tempDirectory f 
-  | isTmp dir   = dir 
+tempDirectory f
+  | isTmp dir   = dir
   | otherwise   = dir </> tmpDirName
   where
     dir         = takeDirectory f
@@ -141,7 +141,7 @@
   case explode modName of
     [] -> errorstar $ "malformed module name: " ++ modName
     ws -> extFileNameR ext $ foldr1 (</>) ws
-  where 
+  where
     explode = words . map (\c -> if c == '.' then ' ' else c)
 
 copyFiles :: [FilePath] -> FilePath -> IO ()
diff --git a/src/Language/Fixpoint/Interface.hs b/src/Language/Fixpoint/Interface.hs
--- a/src/Language/Fixpoint/Interface.hs
+++ b/src/Language/Fixpoint/Interface.hs
@@ -1,72 +1,73 @@
 module Language.Fixpoint.Interface (
-    
+
     -- * Containing Constraints
     FInfo (..)
- 
+
     -- * Invoke Solver on Set of Constraints
   , solve
   , solveFile
 
     -- * Function to determine outcome
   , resultExit
- 
+
     -- * Validity Query
-  , checkValid 
+  , checkValid
 
 ) where
 
 {- Interfacing with Fixpoint Binary -}
 
-import Data.Hashable
-import Data.Monoid
-import Data.Functor
-import Data.List
-import qualified Data.HashMap.Strict as M
-import System.IO        (hPutStr, withFile, IOMode (..))
-import System.Exit
-import System.Directory (getTemporaryDirectory)
-import System.FilePath  ((</>))
-import Text.Printf
+import           Data.Functor
+import           Data.Hashable
+import qualified Data.HashMap.Strict              as M
+import           Data.List
+import           Data.Monoid
+import           System.Directory                 (getTemporaryDirectory)
+import           System.Exit
+import           System.FilePath                  ((</>))
+import           System.IO                        (IOMode (..), hPutStr,
+                                                   withFile)
+import           Text.Printf
 
-import Language.Fixpoint.Config
-import Language.Fixpoint.Types         hiding (kuts, lits)
-import Language.Fixpoint.Misc
-import Language.Fixpoint.Parse            (rr)
-import Language.Fixpoint.Files
-import Text.PrettyPrint.HughesPJ
-import System.Console.CmdArgs.Default
-import System.Console.CmdArgs.Verbosity
+import           Language.Fixpoint.Config
+import           Language.Fixpoint.Files
+import           Language.Fixpoint.Misc
+import           Language.Fixpoint.Parse          (rr)
+import           Language.Fixpoint.Types          hiding (kuts, lits)
+import           System.Console.CmdArgs.Default
+import           System.Console.CmdArgs.Verbosity
+import           Text.PrettyPrint.HughesPJ
 
 ---------------------------------------------------------------------------
 -- | One Shot validity query ----------------------------------------------
 ---------------------------------------------------------------------------
 
 ---------------------------------------------------------------------------
-checkValid :: (Hashable a) => a -> [(Symbol, Sort)] -> Pred -> IO (FixResult a) 
+checkValid :: (Hashable a) => a -> [(Symbol, Sort)] -> Pred -> IO (FixResult a)
 ---------------------------------------------------------------------------
-checkValid n xts p 
+checkValid n xts p
   = do file   <- (</> show (hash n)) <$> getTemporaryDirectory
        (r, _) <- solve def file [] $ validFInfo n xts p
-       return (sinfo <$> r)  
+       return (sinfo <$> r)
 
 validFInfo         :: a -> [(Symbol, Sort)] -> Pred -> FInfo a
 validFInfo l xts p = FI constrm [] benv emptySEnv [] ksEmpty []
-  where 
-    constrm        = M.singleton 0 $ validSubc l ibenv p 
+  where
+    constrm        = M.singleton 0 $ validSubc l ibenv p
     binds          = [(x, trueSortedReft t) | (x, t) <- xts]
     ibenv          = insertsIBindEnv bids emptyIBindEnv
     (bids, benv)   = foldlMap (\e (x,t) -> insertBindEnv x t e) emptyBindEnv binds
 
-validSubc         :: a -> IBindEnv -> Pred -> SubC a  
+validSubc         :: a -> IBindEnv -> Pred -> SubC a
 validSubc l env p = safeHead "Interface.validSubC" $ subC env PTrue lhs rhs i t l
-  where 
+  where
     lhs           = mempty
     rhs           = RR mempty (predReft p)
     i             = Just 0
     t             = []
 
-result         :: a -> Bool -> FixResult a    
-result _ True  = Safe 
+result         :: a -> Bool -> FixResult a
+result _ True  = Safe
 result x False = Unsafe [x]
 
 
@@ -75,25 +76,25 @@
 ---------------------------------------------------------------------------
 
 ---------------------------------------------------------------------------
-solve :: Config -> FilePath -> [FilePath] -> FInfo a 
+solve :: Config -> FilePath -> [FilePath] -> FInfo a
       -> IO (FixResult (SubC a), M.HashMap Symbol Pred)
 ---------------------------------------------------------------------------
 solve cfg fn hqs fi
   =   {-# SCC "Solve" #-}  execFq cfg fn hqs fi
-  >>= {-# SCC "exitFq" #-} exitFq fn (cm fi) 
-      
+  >>= {-# SCC "exitFq" #-} exitFq fn (cm fi)
+
 execFq cfg fn hqs fi
   = do copyFiles hqs fq
-       appendFile fq qstr 
+       appendFile fq qstr
        withFile fq AppendMode (\h -> {-# SCC "HPrintDump" #-} hPutStr h (render d))
        solveFile $ cfg `withTarget` fq
-    where 
+    where
        fq   = extFileName Fq fn
-       d    = {-# SCC "FixPointify" #-} toFixpoint fi 
+       d    = {-# SCC "FixPointify" #-} toFixpoint fi
        qstr = render ((vcat $ toFix <$> (quals fi)) $$ text "\n")
 
 ---------------------------------------------------------------------------
-solveFile :: Config -> IO ExitCode 
+solveFile :: Config -> IO ExitCode
 ---------------------------------------------------------------------------
 solveFile cfg
   = do fp  <- getFixpointPath
@@ -101,33 +102,32 @@
        v   <- (\b -> if b then "-v 1" else "") <$> isLoud
        ec  <- {-# SCC "sysCall:Fixpoint" #-} executeShellCommand "fixpoint" $ fixCommand cfg fp z3 v rf
        return ec
-  where realFlags =  "-no-uif-multiply " 
+  where realFlags =  "-no-uif-multiply "
                   ++ "-no-uif-divide "
         rf        = if (real cfg) then realFlags else ""
 
-fixCommand cfg fp z3 verbosity realFlags 
-  = printf "LD_LIBRARY_PATH=%s %s %s %s -notruekvars -refinesort -nosimple -strictsortcheck -sortedquals %s" 
+fixCommand cfg fp z3 verbosity realFlags
+  = printf "LD_LIBRARY_PATH=%s %s %s %s -notruekvars -refinesort -nosimple -strictsortcheck -sortedquals %s"
            z3 fp verbosity realFlags (command cfg)
 
-exitFq _ _ (ExitFailure n) | (n /= 1) 
+exitFq _ _ (ExitFailure n) | (n /= 1)
   = return (Crash [] "Unknown Error", M.empty)
-exitFq fn cm _ 
+exitFq fn cm _
   = do str <- {-# SCC "readOut" #-} readFile (extFileName Out fn)
        let (x, y) = parseFixpointOutput str -- {-# SCC "parseFixOut" #-} rr ({-# SCC "sanitizeFixpointOutput" #-} sanitizeFixpointOutput str)
-       return  $ (plugC cm x, y) 
+       return  $ (plugC cm x, y)
 
 parseFixpointOutput :: String -> (FixResult Integer, FixSolution)
 parseFixpointOutput str = {-# SCC "parseFixOut" #-} rr ({-# SCC "sanitizeFixpointOutput" #-} sanitizeFixpointOutput str)
 
 plugC = fmap . mlookup
 
-sanitizeFixpointOutput 
-  = unlines 
-  . filter (not . ("//"     `isPrefixOf`)) 
+sanitizeFixpointOutput
+  = unlines
+  . filter (not . ("//"     `isPrefixOf`))
   . chopAfter ("//QUALIFIERS" `isPrefixOf`)
   . lines
 
 resultExit Safe        = ExitSuccess
 resultExit (Unsafe _)  = ExitFailure 1
 resultExit _           = ExitFailure 2
-
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
@@ -1,55 +1,58 @@
-{-# LANGUAGE DeriveDataTypeable, TupleSections, NoMonomorphismRestriction, ScopedTypeVariables #-}
-{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE DeriveDataTypeable        #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE OverloadedStrings         #-}
+{-# LANGUAGE ScopedTypeVariables       #-}
+{-# LANGUAGE TupleSections             #-}
 
 module Language.Fixpoint.Misc where
 
-import Data.Traversable               (traverse)
-import Data.Hashable
-import qualified Control.Exception     as Ex
--- import qualified Data.HashSet        as S 
-import qualified Data.HashMap.Strict   as M
-import qualified Data.List             as L
-import qualified Data.ByteString       as B
-import qualified Data.Text             as T
-import Data.ByteString.Char8    (pack, unpack)
-import Control.Applicative      ((<$>))
-import Control.Monad            (forM_, (>=>))
-import Data.Maybe               (fromJust)
-import Data.Maybe               (catMaybes, fromMaybe)
+import qualified Control.Exception                as Ex
+import           Data.Hashable
+import           Data.Traversable                 (traverse)
+-- import qualified Data.HashSet        as S
+import           Control.Applicative              ((<$>))
+import           Control.Monad                    (forM_, (>=>))
+import qualified Data.ByteString                  as B
+import           Data.ByteString.Char8            (pack, unpack)
+import qualified Data.HashMap.Strict              as M
+import qualified Data.List                        as L
+import           Data.Maybe                       (fromJust)
+import           Data.Maybe                       (catMaybes, fromMaybe)
+import qualified Data.Text                        as T
 
-import System.Exit
-import System.Process           (system)
-import Debug.Trace              (trace)
-import Data.Data
-import System.Console.ANSI
-import System.Console.CmdArgs.Verbosity (whenLoud)
+import           Data.Data
+import           Debug.Trace                      (trace)
+import           System.Console.ANSI
+import           System.Console.CmdArgs.Verbosity (whenLoud)
+import           System.Exit
+import           System.Process                   (system)
 
-import Text.PrettyPrint.HughesPJ
+import           Text.PrettyPrint.HughesPJ
 
 -----------------------------------------------------------------------------------
 ------------ Support for Colored Logging ------------------------------------------
 -----------------------------------------------------------------------------------
 
-data Moods = Ok | Loud | Sad | Happy | Angry 
+data Moods = Ok | Loud | Sad | Happy | Angry
 
 moodColor Ok    = Black
-moodColor Loud  = Blue 
-moodColor Sad   = Magenta 
-moodColor Happy = Green 
-moodColor Angry = Red 
+moodColor Loud  = Blue
+moodColor Sad   = Magenta
+moodColor Happy = Green
+moodColor Angry = Red
 
 wrapStars msg = "\n**** " ++ msg ++ " " ++ replicate (74 - length msg) '*'
 
 wrapStarsWithOptStars True  msg = "\n**** " ++ msg ++ " " ++ replicate (74 - length msg) '*'
 wrapStarsWithOptStars False msg = wrapStars msg
 
--- withColor _ act = act  
+-- withColor _ act = act
 withColor c act
-   = do setSGR [ SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid c] 
+   = do setSGR [ SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid c]
         act
         setSGR [ Reset]
 
-colorStrLn c       = withColor (moodColor c) . putStrLn 
+colorStrLn c       = withColor (moodColor c) . putStrLn
 colorPhaseLn c msg = colorStrLn c . wrapStars .  (msg ++)
 startPhase c msg   = colorPhaseLn c "START: " msg >> colorStrLn Ok " "
 doneLine   c msg   = colorPhaseLn c "DONE:  " msg >> colorStrLn Ok " "
@@ -58,13 +61,13 @@
 startPhaseWithOptStars   v c msg = colorPhaseLnWithOptStars v c "START: " msg >> colorStrLn Ok " "
 doneLineWithOptStars     v c msg = colorPhaseLnWithOptStars v c "DONE:  " msg >> colorStrLn Ok " "
 
-donePhase c str 
-  = case lines str of 
+donePhase c str
+  = case lines str of
       (l:ls) -> doneLine c l >> forM_ ls (colorPhaseLn c "")
       _      -> return ()
 
-donePhaseWithOptStars v c str 
-  = case lines str of 
+donePhaseWithOptStars v c str
+  = case lines str of
       (l:ls) -> doneLineWithOptStars v c l >> forM_ ls (colorPhaseLnWithOptStars v c "")
       _      -> return ()
 
@@ -76,7 +79,7 @@
 unIntersperse x ys
   = case L.elemIndex x ys of
       Nothing -> [ys]
-      Just i  -> let (y, _:ys') = splitAt i ys 
+      Just i  -> let (y, _:ys') = splitAt i ys
                  in (y : unIntersperse x ys')
 
 (=>>) m f = m >>= (\x -> f x >> return x)
@@ -85,17 +88,17 @@
 
 repeats n  = concat . replicate n
 
-errorstar  = error . wrap (stars ++ "\n") (stars ++ "\n") 
-  where 
+errorstar  = error . wrap (stars ++ "\n") (stars ++ "\n")
+  where
     stars = repeats 3 $ wrapStars "ERROR"
 
-errortext  = errorstar . render 
+errortext  = errorstar . render
 
 putDocLn :: Doc -> IO ()
-putDocLn = putStrLn . render 
+putDocLn = putStrLn . render
 
 assertstar _   True  x = x
-assertstar msg False x = errorstar msg 
+assertstar msg False x = errorstar msg
 
 findWithDefaultL f ls d = fromMaybe d (L.find f ls)
 
@@ -124,21 +127,21 @@
 mapPair f (x, y) = (f x, f y)
 
 -- mlookup ::  (Show k, Hashable k) => M.HashMap k v -> k -> v
-mlookup m k 
+mlookup m k
   = case M.lookup k m of
       Just v  -> v
       Nothing -> errorstar $ "mlookup: unknown key " ++ show k
 
 
 mfromJust ::  String -> Maybe a -> a
-mfromJust _ (Just x) = x 
+mfromJust _ (Just x) = x
 mfromJust s Nothing  = errorstar $ "mfromJust: Nothing " ++ s
 
-boxStrCat ::  String -> [String] -> String 
-boxStrCat sep = ("[" ++) . (++ "]") . L.intercalate sep 
+boxStrCat ::  String -> [String] -> String
+boxStrCat sep = ("[" ++) . (++ "]") . L.intercalate sep
 
 tryIgnore :: String -> IO () -> IO ()
-tryIgnore s a = Ex.catch a $ \e -> 
+tryIgnore s a = Ex.catch a $ \e ->
                 do let err = show (e :: Ex.IOException)
                    whenLoud $ putStrLn ("Warning: Couldn't do " ++ s ++ ": " ++ err)
                    return ()
@@ -152,27 +155,27 @@
 -- inserts       ::  Hashable k => k -> v -> M.HashMap k [v] -> M.HashMap k [v]
 inserts k v m = M.insert k (v : M.lookupDefault [] k m) m
 
-concatMaps    = fmap sortNub . L.foldl' (M.unionWith (++)) M.empty 
+concatMaps    = fmap sortNub . L.foldl' (M.unionWith (++)) M.empty
 
 -- group         :: Hashable k => [(k, v)] -> M.HashMap k [v]
-group         = L.foldl' (\m (k, v) -> inserts k v m) M.empty 
+group         = L.foldl' (\m (k, v) -> inserts k v m) M.empty
 
 groupList     = M.toList . group
 
 -- groupMap      :: Hashable k => (a -> k) -> [a] -> M.HashMap k [a]
-groupMap f xs = L.foldl' (\m x -> inserts (f x) x m) M.empty xs 
+groupMap f xs = L.foldl' (\m x -> inserts (f x) x m) M.empty xs
 
 sortNub :: (Ord a) => [a] -> [a]
 sortNub = nubOrd . L.sort
-  where nubOrd (x:t@(y:_)) 
-          | x == y    = nubOrd t 
+  where nubOrd (x:t@(y:_))
+          | x == y    = nubOrd t
           | otherwise = x : nubOrd t
         nubOrd xs = xs
 
 
 sortDiff :: (Ord a) => [a] -> [a] -> [a]
 sortDiff x1s x2s                 = go (sortNub x1s) (sortNub x2s)
-  where go xs@(x:xs') ys@(y:ys') 
+  where go xs@(x:xs') ys@(y:ys')
           | x <  y               = x : go xs' ys
           | x == y               = go xs' ys'
           | otherwise            = go xs ys'
@@ -186,49 +189,49 @@
 distinct xs = length xs == length (sortNub xs)
 
 tr_reverse ::  [a] -> [a]
-tr_reverse      = L.foldl' (flip (:)) []  
+tr_reverse      = L.foldl' (flip (:)) []
 
 tr_foldr' ::  (a -> b -> b) -> b -> [a] -> b
-tr_foldr' f b   = L.foldl' (flip f) b . tr_reverse 
+tr_foldr' f b   = L.foldl' (flip f) b . tr_reverse
 
-safeZip msg xs ys 
-  | nxs == nys 
+safeZip msg xs ys
+  | nxs == nys
   = zip xs ys
-  | otherwise              
+  | otherwise
   = errorstar $ "safeZip called on non-eq-sized lists (nxs = " ++ show nxs ++ ", nys = " ++ show nys ++ ") : " ++ msg
   where nxs = length xs
         nys = length ys
 
--- eqLen = on (==) length 
+-- eqLen = on (==) length
 
-safeZipWith msg f xs ys 
-  | nxs == nys 
+safeZipWith msg f xs ys
+  | nxs == nys
   = zipWith f xs ys
-  | otherwise              
+  | otherwise
   = errorstar $ "safeZipWith called on non-eq-sized lists (nxs = " ++ show nxs ++ ", nys = " ++ show nys ++ ") : " ++ msg
     where nxs = length xs
           nys = length ys
 
--- safe0ZipWith msg f xs ys 
---   | length xs == length ys 
+-- safe0ZipWith msg f xs ys
+--   | length xs == length ys
 --   = zipWith f xs ys
 -- safe0ZipWith _ _ [] _
 --   = []
 -- safe0ZipWith _ _ _ []
 --   = []
--- safe0ZipWith msg _ xs ys 
+-- safe0ZipWith msg _ xs ys
 --   = errorstar $ "safeZipWith called on non-eq-sized lists (nxs = " ++ show nxs ++ ", nys = " ++ show nys ++ ") : " ++ msg
 --     where nxs = length xs
 --           nys = length ys
 
 
 -- safeFromList :: (Hashable k, Show k, Show a) => String -> [(k, a)] -> M.HashMap k a
-safeFromList msg = L.foldl' safeAdd M.empty 
-  where safeAdd m (k, v) 
+safeFromList msg = L.foldl' safeAdd M.empty
+  where safeAdd m (k, v)
           | k `M.member` m = errorstar $ msg ++ "Duplicate key " ++ show k ++ "maps to: \n" ++ (show v) ++ "\n and \n" ++ show (m M.! k)
           | otherwise      = M.insert k v m
 
-safeUnion msg m1 m2 = 
+safeUnion msg m1 m2 =
   case L.find (`M.member` m1) (M.keys m2) of
     Just k  -> errorstar $ "safeUnion with common key = " ++ show k ++ " " ++ msg
     Nothing -> M.union m1 m2
@@ -244,57 +247,57 @@
 
 
 -- memoIndex :: (Hashable b) => (a -> Maybe b) -> [a] -> [Maybe Int]
-memoIndex f = snd . L.mapAccumL foo M.empty 
-  where 
+memoIndex f = snd . L.mapAccumL foo M.empty
+  where
   foo memo z =
-    case f z of 
+    case f z of
       Nothing -> (memo, Nothing)
-      Just k  -> case k `M.lookup` memo of 
+      Just k  -> case k `M.lookup` memo of
                    Just i  -> (memo, Just i)
                    Nothing -> (M.insert k (M.size memo) memo, Just (M.size memo))
 
 checkFail ::  [Char] -> (a -> Bool) -> a -> a
-checkFail msg f x 
+checkFail msg f x
   | f x
   = x
   | otherwise
   = errorstar $ "Check-Failure: " ++ msg
 
 chopAfter ::  (a -> Bool) -> [a] -> [a]
-chopAfter f xs 
+chopAfter f xs
   = case L.findIndex f xs of
       Just n  -> take n xs
       Nothing -> xs
 
-chopPrefix p xs 
+chopPrefix p xs
   | p `L.isPrefixOf` xs
   = Just $ drop (length p) xs
-  | otherwise 
+  | otherwise
   = Nothing
 
 firstElem ::  (Eq a) => [(a, t)] -> [a] -> Maybe Int
-firstElem seps str 
-  = case catMaybes [ L.elemIndex c str | (c, _) <- seps ] of 
+firstElem seps str
+  = case catMaybes [ L.elemIndex c str | (c, _) <- seps ] of
       [] -> Nothing
-      is -> Just $ minimum is 
+      is -> Just $ minimum is
 
 chopAlt ::  (Eq a) => [(a, a)] -> [a] -> [[a]]
-chopAlt seps    = go 
+chopAlt seps    = go
   where go  s   = maybe [s] (go' s) (firstElem seps s)
-        go' s i = let (s0, s1@(c:_)) = splitAt i s 
-                      (Just c')      = lookup c seps 
+        go' s i = let (s0, s1@(c:_)) = splitAt i s
+                      (Just c')      = lookup c seps
                   in case L.elemIndex c' s1 of
                        Nothing -> [s1]
-                       Just i' -> let (s2, s3) = splitAt (i' + 1) s1 in 
+                       Just i' -> let (s2, s3) = splitAt (i' + 1) s1 in
                                   s0 : s2 : go s3
 
 firstElems ::  [(B.ByteString, B.ByteString)] -> B.ByteString -> Maybe (Int, B.ByteString, (B.ByteString, B.ByteString))
-firstElems seps str 
-  = case splitters seps str of 
+firstElems seps str
+  = case splitters seps str of
       [] -> Nothing
-      is -> Just $ L.minimumBy (\x y -> compare (fst3 x) (fst3 y)) is 
+      is -> Just $ L.minimumBy (\x y -> compare (fst3 x) (fst3 y)) is
 
-splitters seps str 
+splitters seps str
   = [(i, c', z) | (c, c') <- seps
                 , let z   = B.breakSubstring c str
                 , let i   = B.length (fst z)
@@ -302,25 +305,25 @@
 
 
 bchopAlts :: [(B.ByteString, B.ByteString)] -> B.ByteString -> [B.ByteString]
-bchopAlts seps  = go 
-  where 
+bchopAlts seps  = go
+  where
     go  s                 = maybe [s] (go' s) (firstElems seps s)
     go' s (i,c',(s0, s1)) = if (B.length s2 == B.length s1) then [B.concat [s0,s1]] else (s0 : s2' : go s3')
                             where (s2, s3) = B.breakSubstring c' s1
                                   s2'      = B.append s2 c'
-                                  s3'      = B.drop (B.length c') s3 
+                                  s3'      = B.drop (B.length c') s3
 
 chopAlts seps str = unpack <$> bchopAlts [(pack c, pack c') | (c, c') <- seps] (pack str)
 
 findFirst ::  Monad m => (t -> m [a]) -> [t] -> m (Maybe a)
 findFirst _ []     = return Nothing
 findFirst f (x:xs) = do r <- f x
-                        case r of 
+                        case r of
                           y:_ -> return (Just y)
                           []  -> findFirst f xs
 
 testM f x = do b <- f x
-               return $ if b then [x] else [] 
+               return $ if b then [x] else []
 
 -- unions :: (Hashable a) => [S.HashSet a] -> S.HashSet a
 -- unions = foldl' S.union S.empty
@@ -332,35 +335,35 @@
     strip = T.stripPrefix "(" >=> T.stripSuffix ")"
 
 ifM :: (Monad m) => m Bool -> m a -> m a -> m a
-ifM bm xm ym 
+ifM bm xm ym
   = do b <- bm
        if b then xm else ym
 
-executeShellCommand phase cmd 
-  = do whenLoud $ putStrLn $ "EXEC: " ++ cmd 
+executeShellCommand phase cmd
+  = do whenLoud $ putStrLn $ "EXEC: " ++ cmd
        Ex.bracket_ (startPhase Loud phase) (donePhase Loud phase) $ system cmd
 
-executeShellCommandWithOptStars v phase cmd 
-  = do whenLoud $ putStrLn $ "EXEC: " ++ cmd 
+executeShellCommandWithOptStars v phase cmd
+  = do whenLoud $ putStrLn $ "EXEC: " ++ cmd
        Ex.bracket_ (startPhaseWithOptStars v Loud phase) (donePhaseWithOptStars v Loud phase) $ system cmd
 
 checkExitCode _   (ExitSuccess)   = return ()
-checkExitCode cmd (ExitFailure n) = errorstar $ "cmd: " ++ cmd ++ " failure code " ++ show n 
+checkExitCode cmd (ExitFailure n) = errorstar $ "cmd: " ++ cmd ++ " failure code " ++ show n
 
 hashMapToAscList    ::  Ord a => M.HashMap a b -> [(a, b)]
 hashMapToAscList    = L.sortBy (\x y -> compare (fst x) (fst y)) . M.toList
 
 hashMapMapWithKey   :: (k -> v1 -> v2) -> M.HashMap k v1 -> M.HashMap k v2
-hashMapMapWithKey f = fromJust . M.traverseWithKey (\k v -> Just (f k v)) 
+hashMapMapWithKey f = fromJust . M.traverseWithKey (\k v -> Just (f k v))
 
 hashMapMapKeys      :: (Eq k, Hashable k) => (t -> k) -> M.HashMap t v -> M.HashMap k v
-hashMapMapKeys f    = M.fromList . fmap (mapFst f) . M.toList 
+hashMapMapKeys f    = M.fromList . fmap (mapFst f) . M.toList
 
 
 applyNonNull def _ [] = def
 applyNonNull _   f xs = f xs
 
-concatMapM f = fmap concat . mapM f 
+concatMapM f = fmap concat . mapM f
 
 
 
@@ -374,13 +377,13 @@
 
 foldlMap           :: (a -> b -> (c, a)) -> a -> [b] -> ([c], a)
 foldlMap f b xs    = (reverse zs, res)
-  where 
+  where
     (zs, res)      = L.foldl' ff ([], b) xs
     ff (ys, acc) x = let (y, acc') = f acc x in (y:ys, acc')
 
 mapEither           :: (a -> Either b c) -> [a] -> ([b], [c])
-mapEither f         = go [] [] 
-  where 
+mapEither f         = go [] []
+  where
     go ls rs []     = (reverse ls, reverse rs)
     go ls rs (x:xs) = case f x of
                         Left l  -> go (l:ls) rs  xs
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
@@ -1,12 +1,12 @@
-{-# LANGUAGE ScopedTypeVariables        #-}
-{-# LANGUAGE OverloadedStrings          #-}
-{-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE DeriveDataTypeable         #-}
+{-# LANGUAGE DeriveGeneric              #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE OverloadedStrings          #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
 {-# LANGUAGE StandaloneDeriving         #-}
 {-# LANGUAGE TypeSynonymInstances       #-}
-{-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE ViewPatterns               #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 
 -- | This module contains Haskell variables representing globally visible names.
 --   Rather than have strings floating around the system, all constant names
@@ -32,7 +32,7 @@
   , qualifySymbol
   , suffixSymbol
 
-  -- * Hardwired global names 
+  -- * Hardwired global names
   , dummyName
   , preludeName
   , boolConName
@@ -48,23 +48,23 @@
   , prims
 ) where
 
-import GHC.Generics         (Generic)
-import Data.Char
-import Data.String
-import Data.Typeable        (Typeable)
-import Data.Generics        (Data)
-import Data.Text                (Text)
-import qualified Data.Text      as T
-import Data.Monoid
-import Data.Interned
-import Data.Interned.Internal.Text
-import Data.Interned.Text
-import Data.Hashable
-import qualified Data.HashSet        as S
-import Control.Applicative
-import Control.DeepSeq
+import           Control.Applicative
+import           Control.DeepSeq
+import           Data.Char
+import           Data.Generics               (Data)
+import           Data.Hashable
+import qualified Data.HashSet                as S
+import           Data.Interned
+import           Data.Interned.Internal.Text
+import           Data.Interned.Text
+import           Data.Monoid
+import           Data.String
+import           Data.Text                   (Text)
+import qualified Data.Text                   as T
+import           Data.Typeable               (Typeable)
+import           GHC.Generics                (Generic)
 
-import Language.Fixpoint.Misc   (errorstar, stripParens, mapSnd)
+import           Language.Fixpoint.Misc      (errorstar, mapSnd, stripParens)
 
 ---------------------------------------------------------------
 ---------------------------- Symbols --------------------------
@@ -251,7 +251,7 @@
 vvName       = "VV"
 symSepName   = '#'
 
-size32Name   = "Size32" :: Symbol 
+size32Name   = "Size32" :: Symbol
 size64Name   = "Size64" :: Symbol
 bitVecName   = "BitVec" :: Symbol
 bvOrName     = "bvor"   :: Symbol
@@ -278,17 +278,17 @@
         , size32Name
         , size64Name
         , bitVecName
-        , bvOrName 
+        , bvOrName
         , bvAndName
-        , "FAppTy" 
+        , "FAppTy"
         ]
 
 -- dropModuleNames []  = []
--- dropModuleNames s  
---   | s == tupConName = tupConName 
+-- dropModuleNames s
+--   | s == tupConName = tupConName
 --   | otherwise       = safeLast msg $ words $ dotWhite `fmap` stripParens s
---   where 
---     msg             = "dropModuleNames: " ++ s 
+--   where
+--     msg             = "dropModuleNames: " ++ s
 --     dotWhite '.'    = ' '
 --     dotWhite c      = c
 
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
@@ -1,21 +1,26 @@
-{-# LANGUAGE NoMonomorphismRestriction, FlexibleInstances, UndecidableInstances, TypeSynonymInstances, TupleSections #-}
+{-# LANGUAGE FlexibleContexts          #-}
+{-# LANGUAGE FlexibleInstances         #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE TupleSections             #-}
+{-# LANGUAGE TypeSynonymInstances      #-}
+{-# LANGUAGE UndecidableInstances      #-}
 
 module Language.Fixpoint.Parse (
-  
-  -- * Top Level Class for Parseable Values  
+
+  -- * Top Level Class for Parseable Values
     Inputable (..)
-  
-  -- * Top Level Class for Parseable Values  
+
+  -- * Top Level Class for Parseable Values
   , Parser
 
   -- * Lexer to add new tokens
-  , lexer 
+  , lexer
 
   -- * Some Important keyword and parsers
   , reserved, reservedOp
   , parens  , brackets, angles, braces
-  , semi    , comma     
-  , colon   , dcolon 
+  , semi    , comma
+  , colon   , dcolon
   , whiteSpace
   , blanks
 
@@ -49,35 +54,35 @@
   , freshIntP
 
   -- * Parsing Function
-  , doParse' 
+  , doParse'
   , parseFromFile
-  , remainderP 
+  , remainderP
   ) where
 
-import Control.Applicative ((<*>), (<$>), (<*))
-import Control.Monad
-import Text.Parsec
-import Text.Parsec.Expr
-import Text.Parsec.Pos
-import Text.Parsec.Language
-import Text.Parsec.String hiding (Parser, parseFromFile)
-import Text.Printf  (printf)
-import qualified Text.Parsec.Token as Token
-import qualified Data.HashMap.Strict as M
-import qualified Data.HashSet as S
-import Data.Text (Text)
-import qualified Data.Text as T
+import           Control.Applicative         ((<$>), (<*), (<*>))
+import           Control.Monad
+import qualified Data.HashMap.Strict         as M
+import qualified Data.HashSet                as S
+import           Data.Text                   (Text)
+import qualified Data.Text                   as T
+import           Text.Parsec
+import           Text.Parsec.Expr
+import           Text.Parsec.Language
+import           Text.Parsec.Pos
+import           Text.Parsec.String          hiding (Parser, parseFromFile)
+import qualified Text.Parsec.Token           as Token
+import           Text.Printf                 (printf)
 
-import Data.Char (isLower, toUpper)
-import Language.Fixpoint.Misc hiding (dcolon)
-import Language.Fixpoint.Types
-import Language.Fixpoint.Bitvector
-import Language.Fixpoint.Errors
-import Language.Fixpoint.SmtLib2
+import           Data.Char                   (isLower, toUpper)
+import           Language.Fixpoint.Bitvector
+import           Language.Fixpoint.Errors
+import           Language.Fixpoint.Misc      hiding (dcolon)
+import           Language.Fixpoint.SmtLib2
+import           Language.Fixpoint.Types
 
-import Data.Maybe(maybe, fromJust)
+import           Data.Maybe                  (fromJust, maybe)
 
-import Data.Monoid (mempty)
+import           Data.Monoid                 (mempty)
 
 type Parser = Parsec String Integer
 
@@ -87,7 +92,7 @@
   emptyDef { Token.commentStart    = "/* "
            , Token.commentEnd      = " */"
            , Token.commentLine     = "--"
-           , Token.identStart      = satisfy (\_ -> False) 
+           , Token.identStart      = satisfy (\_ -> False)
            , Token.identLetter     = satisfy (\_ -> False)
            , Token.reservedNames   = [ "SAT"
                                      , "UNSAT"
@@ -112,10 +117,10 @@
                                      ]
            , Token.reservedOpNames = [ "+", "-", "*", "/", "\\"
                                      , "<", ">", "<=", ">=", "=", "!=" , "/="
-                                     , "mod", "and", "or" 
+                                     , "mod", "and", "or"
                                   --, "is"
                                      , "&&", "||"
-                                     , "~", "=>", "<=>"
+                                     , "~", "=>", "==>", "<=>"
                                      , "->"
                                      , ":="
                                      , "&", "^", "<<", ">>", "--"
@@ -143,14 +148,14 @@
 
 blanks  = many (satisfy (`elem` [' ', '\t']))
 
-integer = posInteger 
-  
+integer = posInteger
+
 --  try (char '-' >> (negate <$> posInteger))
 --       <|> posInteger
 
 posInteger = toI <$> (many1 digit <* spaces)
   where
-    toI :: String -> Integer 
+    toI :: String -> Integer
     toI = read
 
 ----------------------------------------------------------------
@@ -163,7 +168,7 @@
 -- FIXME: we (LH) rely on this parser being dumb and *not* consuming trailing
 -- whitespace, in order to avoid some parsers spanning multiple lines..
 condIdP  :: [Char] -> (String -> Bool) -> Parser Symbol
-condIdP chars f 
+condIdP chars f
   = do c  <- letter
        cs <- many (satisfy (`elem` chars))
        blanks
@@ -175,7 +180,7 @@
 lowerIdP :: Parser Symbol
 lowerIdP = condIdP symChars (isLower . head)
 
-locLowerIdP = locParserP lowerIdP 
+locLowerIdP = locParserP lowerIdP
 locUpperIdP = locParserP upperIdP
 
 symbolP :: Parser Symbol
@@ -188,7 +193,7 @@
 symconstP = SL . T.pack <$> stringLiteral
 
 expr0P :: Parser Expr
-expr0P 
+expr0P
   =  (fastIfP EIte exprP)
  <|> (ESym <$> symconstP)
  <|> (ECon <$> constantP)
@@ -203,65 +208,65 @@
   where t = symbolText cs
 --  <|> try (parens $ condP EIte exprP)
 
-fastIfP f bodyP 
-  = do reserved "if" 
+fastIfP f bodyP
+  = do reserved "if"
        p <- predP
        reserved "then"
-       b1 <- bodyP 
+       b1 <- bodyP
        reserved "else"
-       b2 <- bodyP 
+       b2 <- bodyP
        return $ f p b1 b2
 
 
 expr1P :: Parser Expr
-expr1P 
-  =  try funAppP 
- <|> expr0P 
+expr1P
+  =  try funAppP
+ <|> expr0P
 
-exprP :: Parser Expr 
+exprP :: Parser Expr
 exprP = buildExpressionParser bops expr1P
 
 funAppP            =  (try litP) <|> (try exprFunSpacesP) <|> (try exprFunSemisP) <|> exprFunCommasP
-  where 
-    exprFunSpacesP = liftM2 EApp funSymbolP (sepBy1 expr0P blanks) 
+  where
+    exprFunSpacesP = liftM2 EApp funSymbolP (sepBy1 expr0P blanks)
     exprFunCommasP = liftM2 EApp funSymbolP (parens        $ sepBy exprP comma)
     exprFunSemisP  = liftM2 EApp funSymbolP (parenBrackets $ sepBy exprP semi)
     funSymbolP     = locParserP symbolP
 
 
 -- | BitVector literal: lit "#x00000001" (BitVec (Size32 obj))
-litP = do reserved "lit" 
+litP = do reserved "lit"
           l <- stringLiteral
           s <- try (bvSortP "Size32" S32) <|> bvSortP "Size64" S64
           return $ ECon $ L (T.pack l) (mkSort s)
-  where 
+  where
     bvSortP ss s = do parens (reserved "BitVec" >> parens (reserved ss >> reserved "obj"))
                       return s
 
 
--- ORIG exprP :: Parser Expr 
+-- ORIG exprP :: Parser Expr
 -- ORIG exprP =  expr2P <|> lexprP
--- 
--- ORIG lexprP :: Parser Expr 
--- ORIG lexprP   
+--
+-- ORIG lexprP :: Parser Expr
+-- ORIG lexprP
 -- ORIG   =  try (parens exprP)
 -- ORIG  <|> try (parens exprCastP)
 -- ORIG  <|> try (parens $ condP EIte exprP)
 -- ORIG  <|> try exprFunP
 -- ORIG  <|> try (liftM (EVar . stringSymbol) upperIdP)
--- ORIG  <|> liftM expr symbolP 
+-- ORIG  <|> liftM expr symbolP
 -- ORIG  <|> liftM ECon constantP
 -- ORIG  <|> liftM ESym symconstP
 -- ORIG  <|> (reserved "_|_" >> return EBot)
--- ORIG 
+-- ORIG
 -- ORIG exprFunP           =  (try exprFunSpacesP) <|> (try exprFunSemisP) <|> exprFunCommasP
--- ORIG   where 
--- ORIG     exprFunSpacesP = parens $ liftM2 EApp funSymbolP (sepBy exprP spaces) 
+-- ORIG   where
+-- ORIG     exprFunSpacesP = parens $ liftM2 EApp funSymbolP (sepBy exprP spaces)
 -- ORIG     exprFunCommasP = liftM2 EApp funSymbolP (parens        $ sepBy exprP comma)
 -- ORIG     exprFunSemisP  = liftM2 EApp funSymbolP (parenBrackets $ sepBy exprP semi)
 -- ORIG     funSymbolP     = locParserP symbolP -- liftM stringSymbol lowerIdP
 
-parenBrackets  = parens . brackets 
+parenBrackets  = parens . brackets
 
 -- ORIG expr2P = buildExpressionParser bops lexprP
 
@@ -275,11 +280,11 @@
        , [ Infix  (reservedOp "mod"  >> return (EBin Mod  )) AssocLeft]
        ]
 
-eMinus = EBin Minus (expr (0 :: Integer)) 
+eMinus = EBin Minus (expr (0 :: Integer))
 
 
 exprCastP
-  = do e  <- exprP 
+  = do e  <- exprP
        ((try dcolon) <|> colon)
        so <- sortP
        return $ ECst e so
@@ -305,10 +310,10 @@
 falseP = reserved "false" >> return PFalse
 
 pred0P :: Parser Pred
-pred0P =  trueP 
-      <|> falseP 
+pred0P =  trueP
+      <|> falseP
       <|> try (fastIfP pIte predP)
-      <|> try predrP 
+      <|> try predrP
       <|> try (parens predP)
       <|> try (liftM PBexp funAppP)
       <|> try (reservedOp "&&" >> liftM PAnd predsP)
@@ -327,11 +332,12 @@
        , [Infix  (reservedOp "&&"   >> return (\x y -> PAnd [x,y])) AssocRight]
        , [Infix  (reservedOp "||"   >> return (\x y -> POr  [x,y])) AssocRight]
        , [Infix  (reservedOp "=>"   >> return PImp) AssocRight]
+       , [Infix  (reservedOp "==>"  >> return PImp) AssocRight]
        , [Infix  (reservedOp "<=>"  >> return PIff) AssocRight]]
-       
+
 predrP = do e1    <- exprP
             r     <- brelP
-            e2    <- exprP 
+            e2    <- exprP
             return $ r e1 e2
 
 brelP ::  Parser (Expr -> Expr -> Pred)
@@ -346,28 +352,28 @@
      <|> (reservedOp ">"  >> return (PAtom Gt))
      <|> (reservedOp ">=" >> return (PAtom Ge))
 
-condP f bodyP 
+condP f bodyP
    =   try (condIteP f bodyP)
    <|> (condQmP f bodyP)
 
-condI = condIteP EIte 
+condI = condIteP EIte
 
 
-condIteP f bodyP 
-  = do reserved "if" 
+condIteP f bodyP
+  = do reserved "if"
        p <- predP
        reserved "then"
-       b1 <- bodyP 
+       b1 <- bodyP
        reserved "else"
-       b2 <- bodyP 
+       b2 <- bodyP
        return $ f p b1 b2
 
-condQmP f bodyP 
-  = do p  <- predP 
+condQmP f bodyP
+  = do p  <- predP
        reserved "?"
-       b1 <- bodyP 
+       b1 <- bodyP
        colon
-       b2 <- bodyP 
+       b2 <- bodyP
        return $ f p b1 b2
 
 ----------------------------------------------------------------------------------
@@ -381,7 +387,7 @@
   <|> (symbolFTycon   <$> locUpperIdP)
 
 refasP :: Parser [Refa]
-refasP  =  (try (brackets $ sepBy (RConc <$> predP) semi)) 
+refasP  =  (try (brackets $ sepBy (RConc <$> predP) semi))
        <|> liftM ((:[]) . RConc) predP
 
 refBindP :: Parser Symbol -> Parser [Refa] -> Parser (Reft -> a) -> Parser a
@@ -405,8 +411,8 @@
 
 -- qualifierP = mkQual <$> upperIdP <*> parens $ sepBy1 sortBindP comma <*> predP
 
-qualifierP = do pos    <- getPosition 
-                n      <- upperIdP 
+qualifierP = do pos    <- getPosition
+                n      <- upperIdP
                 params <- parens $ sepBy1 sortBindP comma
                 _      <- colon
                 body   <- predP
@@ -415,13 +421,13 @@
 sortBindP  = (,) <$> symbolP <* colon <*> sortP
 
 mkQual n xts p pos = Q n ((vv, t) : yts) (subst su p) pos
-  where 
+  where
     (vv,t):zts     = xts
     yts            = mapFst mkParam <$> zts
-    su             = mkSubst $ zipWith (\(z,_) (y,_) -> (z, eVar y)) zts yts 
-                       
+    su             = mkSubst $ zipWith (\(z,_) (y,_) -> (z, eVar y)) zts yts
+
 mkParam s      = symbol ('~' `T.cons` toUpper c `T.cons` cs)
-  where 
+  where
     Just (c,cs)= T.uncons $ symbolText s
 
 ---------------------------------------------------------------------
@@ -442,7 +448,7 @@
     <|> IBind <$> (reserved "bind"        >> intP) <*> symbolP <*> (colon >> sortedReftP)
 
 sortedReftP :: Parser SortedReft
-sortedReftP = refP (RR <$> (sortP <* spaces)) 
+sortedReftP = refP (RR <$> (sortP <* spaces))
 
 wfCP :: Parser (WfC ())
 wfCP = do reserved "env"
@@ -452,25 +458,25 @@
           return $ wfC env r Nothing ()
 
 subCP :: Parser (SubC ())
-subCP = do reserved "env" 
-           env <- envP 
+subCP = do reserved "env"
+           env <- envP
            reserved "grd"
            grd <- predP
            reserved "lhs"
-           lhs <- sortedReftP 
+           lhs <- sortedReftP
            reserved "rhs"
-           rhs <- sortedReftP 
+           rhs <- sortedReftP
            reserved "id"
            i   <- (integer <* spaces)
            tag <- tagP
-           return $ safeHead "subCP" $ subC env grd lhs rhs (Just i) tag () 
+           return $ safeHead "subCP" $ subC env grd lhs rhs (Just i) tag ()
 
 tagP  :: Parser [Int]
 tagP  =  try (reserved "tag" >> spaces >> (brackets $ sepBy intP semi))
      <|> (return [])
 
 envP  :: Parser IBindEnv
-envP  = do binds <- brackets $ sepBy (intP <* spaces) semi 
+envP  = do binds <- brackets $ sepBy (intP <* spaces) semi
            return $ insertsIBindEnv binds emptyIBindEnv
 
 intP :: Parser Int
@@ -478,24 +484,24 @@
 
 defsFInfo :: [Def a] -> FInfo a
 defsFInfo defs = FI cm ws bs gs lts kts qs
-  where 
+  where
     cm     = M.fromList       [(cid c, c)       | Cst c       <- defs]
     ws     =                  [w                | Wfc w       <- defs]
     bs     = rawBindEnv       [(n, x, r)        | IBind n x r <- defs]
     gs     = fromListSEnv     [(x, RR t mempty) | Con x t     <- defs]
     lts    =                  [(x, t)           | Con x t     <- defs, notFun t]
-    kts    = KS $ S.fromList  [k                | Kut k       <- defs]     
+    kts    = KS $ S.fromList  [k                | Kut k       <- defs]
     qs     =                  [q                | Qul q       <- defs]
     cid    = fromJust . sid
-    notFun = not . isFunctionSortedReft . (`RR` trueReft) 
+    notFun = not . isFunctionSortedReft . (`RR` trueReft)
 ---------------------------------------------------------------------
 -- | Interacting with Fixpoint --------------------------------------
 ---------------------------------------------------------------------
 
 fixResultP :: Parser a -> Parser (FixResult a)
-fixResultP pp 
+fixResultP pp
   =  (reserved "SAT"   >> return Safe)
- <|> (reserved "UNSAT" >> Unsafe <$> (brackets $ sepBy pp comma))  
+ <|> (reserved "UNSAT" >> Unsafe <$> (brackets $ sepBy pp comma))
  <|> (reserved "CRASH" >> crashP pp)
 
 crashP pp
@@ -503,41 +509,41 @@
        msg <- many anyChar
        return $ Crash [i] msg
 
-predSolP 
-  = parens $ (predP  <* (comma >> iQualP)) 
-    
+predSolP
+  = parens $ (predP  <* (comma >> iQualP))
 
+
 iQualP
   = upperIdP >> (parens $ sepBy symbolP comma)
 
 solution1P
-  = do reserved "solution:" 
-       k  <- symbolP 
-       reserved ":=" 
+  = do reserved "solution:"
+       k  <- symbolP
+       reserved ":="
        ps <- brackets $ sepBy predSolP semi
        return (k, simplify $ PAnd ps)
 
 solutionP :: Parser (M.HashMap Symbol Pred)
-solutionP 
+solutionP
   = M.fromList <$> sepBy solution1P whiteSpace
 
-solutionFileP 
+solutionFileP
   = liftM2 (,) (fixResultP integer) solutionP
 
 ------------------------------------------------------------------------
 
-remainderP p  
+remainderP p
   = do res <- p
        str <- getInput
-       pos <- getPosition 
-       return (res, str, pos) 
+       pos <- getPosition
+       return (res, str, pos)
 
 doParse' parser f s
   = case runParser (remainderP (whiteSpace >> parser)) 0 f s of
-      Left e            -> die $ err (errorSpan e) $ printf "parseError %s\n when parsing from %s\n" (show e) f 
+      Left e            -> die $ err (errorSpan e) $ printf "parseError %s\n when parsing from %s\n" (show e) f
       Right (r, "", _)  -> r
       Right (_, rem, l) -> die $ err (SS l l) $ printf "doParse has leftover when parsing: %s\nfrom file %s\n" rem f
-    
+
 errorSpan e = SS l l where l = errorPos e
 
 parseFromFile :: Parser b -> SourceName -> IO b
@@ -554,7 +560,7 @@
 
 commandsP = sepBy commandP semi
 
-commandP 
+commandP
   =  (reserved "var"      >> cmdVarP)
  <|> (reserved "push"     >> return Push)
  <|> (reserved "pop"      >> return Pop)
@@ -562,8 +568,8 @@
  <|> (reserved "assert"   >> (Assert Nothing <$> predP))
  <|> (reserved "distinct" >> (Distinct <$> (brackets $ sepBy exprP comma)))
 
-cmdVarP 
-  = do x <- bindP 
+cmdVarP
+  = do x <- bindP
        t <- sortP
        return $ Declare x [] t
 
@@ -576,19 +582,19 @@
   rr  :: String -> a
   rr' :: String -> String -> a
   rr' = \_ -> rr
-  rr  = rr' "" 
+  rr  = rr' ""
 
 instance Inputable Symbol where
   rr' = doParse' symbolP
 
 instance Inputable Constant where
-  rr' = doParse' constantP 
+  rr' = doParse' constantP
 
 instance Inputable Pred where
-  rr' = doParse' predP 
+  rr' = doParse' predP
 
 instance Inputable Expr where
-  rr' = doParse' exprP 
+  rr' = doParse' exprP
 
 instance Inputable [Refa] where
   rr' = doParse' refasP
@@ -597,13 +603,13 @@
   rr' = doParse' $ fixResultP integer
 
 instance Inputable (FixResult Integer, FixSolution) where
-  rr' = doParse' solutionFileP 
+  rr' = doParse' solutionFileP
 
 instance Inputable (FInfo ()) where
   rr' = doParse' fInfoP
 
 instance Inputable Command where
-  rr' = doParse' commandP 
+  rr' = doParse' commandP
 
 instance Inputable [Command] where
   rr' = doParse' commandsP
@@ -615,7 +621,7 @@
 
 -- A few tricky predicates for parsing
 -- myTest1 = "((((v >= 56320) && (v <= 57343)) => (((numchars a o ((i - o) + 1)) == (1 + (numchars a o ((i - o) - 1)))) && (((numchars a o (i - (o -1))) >= 0) && (((i - o) - 1) >= 0)))) && ((not (((v >= 56320) && (v <= 57343)))) => (((numchars a o ((i - o) + 1)) == (1 + (numchars a o (i - o)))) && ((numchars a o (i - o)) >= 0))))"
--- 
+--
 -- myTest2 = "len x = len y - 1"
 -- myTest3 = "len x y z = len a b c - 1"
 -- myTest4 = "len x y z = len a b (c - 1)"
@@ -651,7 +657,7 @@
 s9  = "v = x+y"
 s10 = "{v: Int | v = x + y}"
 
-s11 = "x:{v:Int | true } -> {v:Int | true }" 
+s11 = "x:{v:Int | true } -> {v:Int | true }"
 s12 = "y : {v:Int | true } -> {v:Int | v = x }"
 s13 = "x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x + y}"
 s14 = "x:{v:a  | true} -> y:{v:b | true } -> {v:a | (x < v && v < y) }"
@@ -661,24 +667,24 @@
 s18 = "x:a -> Bool"
 s20 = "forall a . x:Int -> Bool"
 
-s21 = "x:{v : GHC.Prim.Int# | true } -> {v : Int | true }" 
+s21 = "x:{v : GHC.Prim.Int# | true } -> {v : Int | true }"
 
 r0  = (rr s0) :: Pred
 r0' = (rr s0) :: [Refa]
 r1  = (rr s1) :: [Refa]
 
 
-e1, e2  :: Expr  
+e1, e2  :: Expr
 e1  = rr "(k_1 + k_2)"
-e2  = rr "k_1" 
+e2  = rr "k_1"
 
 o1, o2, o3 :: FixResult Integer
-o1  = rr "SAT " 
+o1  = rr "SAT "
 o2  = rr "UNSAT [1, 2, 9,10]"
-o3  = rr "UNSAT []" 
+o3  = rr "UNSAT []"
 
 -- sol1 = doParse solution1P "solution: k_5 := [0 <= VV_int]"
--- sol2 = doParse solution1P "solution: k_4 := [(0 <= VV_int)]" 
+-- sol2 = doParse solution1P "solution: k_4 := [(0 <= VV_int)]"
 
 b0, b1, b2, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13 :: BareType
 b0  = rr "Int"
@@ -701,7 +707,7 @@
 m1 = ["len :: [a] -> Int", "len (Nil) = 0", "len (Cons x xs) = 1 + len(xs)"]
 m2 = ["tog :: LL a -> Int", "tog (Nil) = 100", "tog (Cons y ys) = 200"]
 
-me1, me2 :: Measure.Measure BareType Symbol 
-me1 = (rr $ intercalate "\n" m1) 
+me1, me2 :: Measure.Measure BareType Symbol
+me1 = (rr $ intercalate "\n" m1)
 me2 = (rr $ intercalate "\n" m2)
 -}
diff --git a/src/Language/Fixpoint/PrettyPrint.hs b/src/Language/Fixpoint/PrettyPrint.hs
--- a/src/Language/Fixpoint/PrettyPrint.hs
+++ b/src/Language/Fixpoint/PrettyPrint.hs
@@ -1,15 +1,15 @@
-{-# LANGUAGE FlexibleContexts           #-}
-{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE FlexibleContexts  #-}
+{-# LANGUAGE FlexibleInstances #-}
 
 
 module Language.Fixpoint.PrettyPrint where
 
-import Text.PrettyPrint.HughesPJ
-import Language.Fixpoint.Types
-import Language.Fixpoint.Misc
-import Control.Applicative      ((<$>))
-import Text.Parsec
-import qualified Data.Text as T
+import           Control.Applicative       ((<$>))
+import qualified Data.Text                 as T
+import           Language.Fixpoint.Misc
+import           Language.Fixpoint.Types
+import           Text.Parsec
+import           Text.PrettyPrint.HughesPJ
 
 class PPrint a where
   pprint :: a -> Doc
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
@@ -1,12 +1,12 @@
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE DeriveGeneric             #-}
+{-# LANGUAGE BangPatterns              #-}
 {-# LANGUAGE DeriveDataTypeable        #-}
+{-# LANGUAGE DeriveGeneric             #-}
 {-# LANGUAGE FlexibleInstances         #-}
-{-# LANGUAGE UndecidableInstances      #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE OverloadedStrings         #-}
-{-# LANGUAGE RecordWildCards           #-}
-{-# LANGUAGE BangPatterns              #-}
 {-# LANGUAGE PatternGuards             #-}
+{-# LANGUAGE RecordWildCards           #-}
+{-# LANGUAGE UndecidableInstances      #-}
 
 -- | This module contains an SMTLIB2 interface for
 --   1. checking the validity, and,
@@ -40,28 +40,29 @@
     , smt_set_funs
     ) where
 
-import Language.Fixpoint.Config (SMTSolver (..))
-import Language.Fixpoint.Files
-import Language.Fixpoint.Types
+import           Language.Fixpoint.Config (SMTSolver (..))
+import           Language.Fixpoint.Files
+import           Language.Fixpoint.Types
 
-import Control.Monad
-import Data.Char
-import qualified Data.List as L
-import qualified Data.HashMap.Strict as M
-import Data.Monoid
-import Data.Text.Format
-import qualified Data.Text          as T
-import qualified Data.Text.IO       as TIO
-import qualified Data.Text.Lazy     as LT
-import qualified Data.Text.Lazy.IO  as LTIO
-import System.Directory
-import System.Exit
-import System.FilePath
-import System.Process
-import System.IO            (openFile, IOMode (..), Handle, hFlush, hClose)
-import Control.Applicative  ((<$>), (<|>), (*>), (<*))
+import           Control.Applicative      ((*>), (<$>), (<*), (<|>))
+import           Control.Monad
+import           Data.Char
+import qualified Data.HashMap.Strict      as M
+import qualified Data.List                as L
+import           Data.Monoid
+import qualified Data.Text                as T
+import           Data.Text.Format
+import qualified Data.Text.IO             as TIO
+import qualified Data.Text.Lazy           as LT
+import qualified Data.Text.Lazy.IO        as LTIO
+import           System.Directory
+import           System.Exit
+import           System.FilePath
+import           System.IO                (Handle, IOMode (..), hClose, hFlush,
+                                           openFile)
+import           System.Process
 
-import qualified Data.Attoparsec.Text as A
+import qualified Data.Attoparsec.Text     as A
 
 {- Usage:
 runFile f
@@ -104,10 +105,10 @@
                   deriving (Eq, Show)
 
 -- | Information about the external SMT process
-data Context      = Ctx { pId  :: ProcessHandle
-                        , cIn  :: Handle
-                        , cOut :: Handle
-                        , cLog :: Maybe Handle
+data Context      = Ctx { pId     :: ProcessHandle
+                        , cIn     :: Handle
+                        , cOut    :: Handle
+                        , cLog    :: Maybe Handle
                         , verbose :: Bool
                         }
 
@@ -123,7 +124,7 @@
 --------------------------------------------------------------------------
 command              :: Context -> Command -> IO Response
 --------------------------------------------------------------------------
-command me !cmd      = {-# SCC command #-} say me cmd >> hear me cmd
+command me !cmd      = {-# SCC "command" #-} say me cmd >> hear me cmd
   where
     say me               = smtWrite me . smt2
     hear me CheckSat     = smtRead me
@@ -136,7 +137,7 @@
 smtWrite me !s    = smtWriteRaw me s
 
 smtRead :: Context -> IO Response
-smtRead me = {-# SCC smtRead #-}
+smtRead me = {-# SCC "smtRead" #-}
     do ln  <- smtReadRaw me
        res <- A.parseWith (smtReadRaw me) responseP ln
        case A.eitherResult res of
@@ -147,19 +148,19 @@
              LTIO.putStrLn $ format "SMT Says: {}" (Only $ show r)
            return r
 
-responseP = {-# SCC responseP #-} A.char '(' *> sexpP
+responseP = {-# SCC "responseP" #-} A.char '(' *> sexpP
          <|> A.string "sat"     *> return Sat
          <|> A.string "unsat"   *> return Unsat
          <|> A.string "unknown" *> return Unknown
 
-sexpP = {-# SCC sexpP #-} A.string "error" *> (Error <$> errorP)
+sexpP = {-# SCC "sexpP" #-} A.string "error" *> (Error <$> errorP)
      <|> Values <$> valuesP
 
 errorP = A.skipSpace *> A.char '"' *> A.takeWhile1 (/='"') <* A.string "\")"
 
 valuesP = A.many1' pairP <* (A.char ')')
 
-pairP = {-# SCC pairP #-}
+pairP = {-# SCC "pairP" #-}
   do A.skipSpace
      A.char '('
      !x <- symbolP
@@ -168,9 +169,9 @@
      A.char ')'
      return (x,v)
 
-symbolP = {-# SCC symbolP #-} symbol <$> A.takeWhile1 (not . isSpace)
+symbolP = {-# SCC "symbolP" #-} symbol <$> A.takeWhile1 (not . isSpace)
 
-valueP = {-# SCC valueP #-} negativeP
+valueP = {-# SCC "valueP" #-} negativeP
       <|> A.takeWhile1 (\c -> not (c == ')' || isSpace c))
 
 negativeP
@@ -184,12 +185,12 @@
               ((x:y:[]),zs) -> (x,y) : pairs zs
 
 smtWriteRaw      :: Context -> LT.Text -> IO ()
-smtWriteRaw me !s = {-# SCC smtWriteRaw #-} do
+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)
+smtReadRaw me    = {-# SCC "smtReadRaw" #-} TIO.hGetLine (cIn me)
 
 hPutStrLnNow h !s   = LTIO.hPutStrLn h s >> hFlush h
 
@@ -239,13 +240,13 @@
 smtCmd Cvc4    = "cvc4 --incremental -L smtlib2"
 
 -- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...
-smtPreamble Z3 me 
+smtPreamble Z3 me
   = do smtWrite me "(get-info :version)"
        r <- (!!1) . T.splitOn "\"" <$> smtReadRaw me
        case T.words r of
          "4.3.2" : _  -> return $ z3_432_options ++ z3Preamble
          _            -> return $ z3_options ++ z3Preamble
-smtPreamble _  _  
+smtPreamble _  _
   = return smtlibPreamble
 
 smtFile :: FilePath
@@ -281,8 +282,8 @@
 bit  = "BitVec"
 sz32 = "Size32"
 sz64 = "Size64"
-             
 
+
 emp, add, cup, cap, mem, dif, sub, com :: Raw
 emp   = "smt_set_emp"
 add   = "smt_set_add"
@@ -294,19 +295,19 @@
 com   = "smt_set_com"
 sel   = "smt_map_sel"
 sto   = "smt_map_sto"
-        
+
 smt_set_funs :: M.HashMap Symbol Raw
 smt_set_funs = M.fromList [ ("Set_emp",emp),("Set_add",add),("Set_cup",cup)
                           , ("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 
+z3_432_options
   = [ "(set-option :auto-config false)"
     , "(set-option :model true)"
     , "(set-option :model.partial false)"
     , "(set-option :smt.mbqi false)" ]
-z3_options 
+z3_options
   = [ "(set-option :auto-config false)"
     , "(set-option :model true)"
     , "(set-option :model-partial false)"
@@ -382,7 +383,7 @@
 
 -- FIXME: this is probably too slow
 encode :: T.Text -> T.Text
-encode t = {-# SCC encode #-}
+encode t = {-# SCC "encode" #-}
   foldr (\(x,y) t -> T.replace x y t) t [("[", "ZM"), ("]", "ZN"), (":", "ZC")
                                         ,("(", "ZL"), (")", "ZR"), (",", "ZT")
                                         ,("|", "zb"), ("#", "zh"), ("\\","zr")
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
@@ -1,8 +1,9 @@
+{-# LANGUAGE FlexibleContexts #-}
 
 -- | This module has the functions that perform sort-checking, and related
 -- operations on Fixpoint expressions and predicates.
 
-module Language.Fixpoint.Sort  ( 
+module Language.Fixpoint.Sort  (
   -- * Checking Well-Formedness
     checkSorted
   , checkSortedReft
@@ -13,51 +14,51 @@
 
 
 
-import Language.Fixpoint.Types
-import Language.Fixpoint.Misc
-import Text.PrettyPrint.HughesPJ
-import Text.Printf
-import Control.Monad.Error (catchError, throwError)
-import Control.Monad
-import Control.Applicative
-import Data.Maybe           (fromMaybe, catMaybes)
-import qualified Data.HashMap.Strict as M
+import           Control.Applicative
+import           Control.Monad
+import           Control.Monad.Error       (catchError, throwError)
+import qualified Data.HashMap.Strict       as M
+import           Data.Maybe                (catMaybes, fromMaybe)
+import           Language.Fixpoint.Misc
+import           Language.Fixpoint.Types
+import           Text.PrettyPrint.HughesPJ
+import           Text.Printf
 
-import Debug.Trace          (trace)
+import           Debug.Trace               (trace)
 
 -- | Types used throughout checker
 
 type CheckM a = Either String a
 type Env      = Symbol -> SESearch Sort
-fProp         = FApp boolFTyCon [] 
--- fProp         = FApp propFTyCon [] 
+fProp         = FApp boolFTyCon []
+-- fProp         = FApp propFTyCon []
 
 -------------------------------------------------------------------------
 -- | Checking Refinements -----------------------------------------------
 -------------------------------------------------------------------------
 
 checkSortedReft :: SEnv SortedReft -> [Symbol] -> SortedReft -> Maybe Doc
-checkSortedReft env xs sr = applyNonNull Nothing error unknowns 
-  where 
-    error                 = Just . (text "Unknown symbols:" <+>) . toFix 
-    unknowns              = [ x | x <- syms sr, not (x `elem` v : xs), not (x `memberSEnv` env)]    
-    Reft (v,_)            = sr_reft sr 
+checkSortedReft env xs sr = applyNonNull Nothing error unknowns
+  where
+    error                 = Just . (text "Unknown symbols:" <+>) . toFix
+    unknowns              = [ x | x <- syms sr, not (x `elem` v : xs), not (x `memberSEnv` env)]
+    Reft (v,_)            = sr_reft sr
 
 checkSortedReftFull :: Checkable a => SEnv SortedReft -> a -> Maybe Doc
 checkSortedReftFull γ t
   = case check γ' t of
       Left err -> Just (text err)
       Right _  -> Nothing
-    where 
-      γ' = mapSEnv sr_sort γ  
+    where
+      γ' = mapSEnv sr_sort γ
 
 checkSortFull :: Checkable a => SEnv SortedReft -> Sort -> a -> Maybe Doc
 checkSortFull γ s t
   = case checkSort γ' s t of
       Left err -> Just (text err)
       Right _  -> Nothing
-    where 
-      γ' = mapSEnv sr_sort γ  
+    where
+      γ' = mapSEnv sr_sort γ
 
 checkSorted :: Checkable a => SEnv Sort -> a -> Maybe Doc
 checkSorted γ t
@@ -67,8 +68,8 @@
 
 pruneUnsortedReft :: SEnv Sort -> SortedReft -> SortedReft
 pruneUnsortedReft γ (RR s (Reft (v, ras)))
-  = RR s (Reft (v, catMaybes (go <$> ras))) 
-  where 
+  = RR s (Reft (v, catMaybes (go <$> ras)))
+  where
     go r = case checkRefa f r of
             Left war -> trace (wmsg war r) $ Nothing
             Right _  -> Just r
@@ -104,9 +105,9 @@
 
 checkEqSort s t
   | s == t    = return ()
-  | otherwise = throwError $ "Couldn't match expected type '" 
+  | otherwise = throwError $ "Couldn't match expected type '"
                            ++ show s ++ "'"
-                           ++ "\n\t\t with actual type '" 
+                           ++ "\n\t\t with actual type '"
                            ++ show t ++ "'"
 
 instance Checkable Pred where
@@ -115,17 +116,17 @@
 
 instance Checkable SortedReft where
   check γ (RR s (Reft (v, ras))) = mapM_ (check γ') ras
-   where γ' = insertSEnv v s γ  
+   where γ' = insertSEnv v s γ
 
 -------------------------------------------------------------------------
 -- | Checking Expressions -----------------------------------------------
 -------------------------------------------------------------------------
 
-checkExpr                  :: Env -> Expr -> CheckM Sort 
+checkExpr                  :: Env -> Expr -> CheckM Sort
 
 checkExpr _ EBot           = throwError "Type Error: Bot"
-checkExpr _ (ECon (I _))   = return FInt 
-checkExpr _ (ECon (R _))   = return FReal 
+checkExpr _ (ECon (I _))   = return FInt
+checkExpr _ (ECon (R _))   = return FReal
 checkExpr f (EVar x)       = checkSym f x
 checkExpr f (ENeg e)       = checkNeg f e
 checkExpr f (EBin o e1 e2) = checkOp f e1 o e2
@@ -136,8 +137,8 @@
 
 -- | Helper for checking symbol occurrences
 
-checkSym f x               
-  = case f x of 
+checkSym f x
+  = case f x of
      Found s -> return s
      Alts xs -> throwError $ errUnboundAlts x xs
 --   $ traceFix ("checkSym: x = " ++ showFix x) (f x)
@@ -146,17 +147,17 @@
 
 -- | Helper for checking if-then-else expressions
 
-checkIte f p e1 e2 
+checkIte f p e1 e2
   = do tp <- checkPred f p
        t1 <- checkExpr f e1
        t2 <- checkExpr f e2
        ((`apply` t1) <$> unify [t1] [t2]) `catchError` (\_ -> throwError $ errIte e1 e2 t1 t2)
 
--- | Helper for checking cast expressions 
+-- | Helper for checking cast expressions
 
-checkCst f t (EApp g es) 
+checkCst f t (EApp g es)
   = checkApp f (Just t) g es
-checkCst f t e           
+checkCst f t e
   = do t' <- checkExpr f e
        ((`apply` t) <$> unify [t] [t']) `catchError` (\_ -> throwError $ errCast e t' t)
 
@@ -164,7 +165,7 @@
   = snd <$> checkApp' f to g es
 
 -- | Helper for checking uninterpreted function applications
-checkApp' f to g es 
+checkApp' f to g es
   = do gt           <- checkLocSym f g
        (n, its, ot) <- sortFunction gt
        unless (length its == length es) $ throwError (errArgArity g its es)
@@ -188,15 +189,15 @@
    _        -> throwError $ printf "Operand has non-numeric type %s in %s"
                             (showFix t) (showFix e)
 
-checkOp f e1 o e2 
+checkOp f e1 o e2
   = do t1 <- checkExpr f e1
        t2 <- checkExpr f e2
        checkOpTy f (EBin o e1 e2) t1 t2
 
-checkOpTy f _ FReal FReal        
+checkOpTy f _ FReal FReal
   = return FReal
 
-checkOpTy f _ FInt FInt          
+checkOpTy f _ FInt FInt
   = return FInt
 
 checkOpTy f e t@(FObj l) t'@(FObj l')
@@ -207,7 +208,9 @@
   = throwError $ errOp e t t'
 
 checkFractional f l
-  = throwError $ errNonFractional l
+  = do t <- checkSym f l
+       unless (t == FFrac) (throwError $ errNonFractional l)
+       return ()
 
 checkNumeric f l
   = do t <- checkSym f l
@@ -218,13 +221,13 @@
 -- | Checking Predicates ------------------------------------------------
 -------------------------------------------------------------------------
 
-checkPred                  :: Env -> Pred -> CheckM () 
+checkPred                  :: Env -> Pred -> CheckM ()
 
 checkPred f PTrue          = return ()
 checkPred f PFalse         = return ()
-checkPred f (PBexp e)      = checkPredBExp f e 
+checkPred f (PBexp e)      = checkPredBExp f e
 checkPred f (PNot p)       = checkPred f p
-checkPred f (PImp p p')    = mapM_ (checkPred f) [p, p'] 
+checkPred f (PImp p p')    = mapM_ (checkPred f) [p, p']
 checkPred f (PIff p p')    = mapM_ (checkPred f) [p, p']
 checkPred f (PAnd ps)      = mapM_ (checkPred f) ps
 checkPred f (POr ps)       = mapM_ (checkPred f) ps
@@ -234,8 +237,8 @@
 checkPredBExp f e          = do t <- checkExpr f e
                                 unless (t == fProp) (throwError $ errBExp e t)
                                 return ()
-  
 
+
 -- | Checking Relations
 
 checkRel f Eq (EVar x) (EApp g es) = checkRelEqVar f x g es
@@ -245,12 +248,12 @@
                                         checkRelTy f (PAtom r e1 e2) r t1 t2
 
 checkRelTy :: (Fixpoint a) => Env -> a -> Brel -> Sort -> Sort -> CheckM ()
-checkRelTy f _ _ (FObj l) (FObj l') | l /= l' 
-  = (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) (FObj l') | l /= l'
+  = (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 FReal       = return ()
-checkRelTy f _ _ FReal (FObj l)    = (checkFractional f l) `catchError` (\_ -> throwError $ errNonFractional l) 
+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
@@ -270,7 +273,7 @@
 checkRelTy _ e _  t1 t2            = unless (t1 == t2)                 (throwError $ errRel e t1 t2)
 
 
--- | Special case for polymorphic singleton variable equality e.g. (x = Set_emp) 
+-- | Special case for polymorphic singleton variable equality e.g. (x = Set_emp)
 
 checkRelEqVar f x g es             = do tx <- checkSym f x
                                         _  <- checkApp f (Just tx) g es
@@ -297,32 +300,32 @@
 
 errUnify t1 t2       = printf "Cannot unify %s with %s" (showFix t1) (showFix t2)
 
-errUnifyMany ts ts'  = printf "Cannot unify types with different cardinalities %s and %s" 
+errUnifyMany ts ts'  = printf "Cannot unify types with different cardinalities %s and %s"
                          (showFix ts) (showFix ts')
 
-errRel e t1 t2       = printf "Invalid Relation %s with operand types %s and %s" 
+errRel e t1 t2       = printf "Invalid Relation %s with operand types %s and %s"
                          (showFix e) (showFix t1) (showFix t2)
 
 errBExp e t          = printf "BExp %s with non-propositional type %s" (showFix e) (showFix t)
 
-errOp e t t' 
-  | t == t'          = printf "Operands have non-numeric types %s in %s"  
+errOp e t t'
+  | t == t'          = printf "Operands have non-numeric types %s in %s"
                          (showFix t) (showFix e)
-  | otherwise        = printf "Operands have different types %s and %s in %s" 
+  | otherwise        = printf "Operands have different types %s and %s in %s"
                          (showFix t) (showFix t') (showFix e)
 
-errArgArity g its es = printf "Measure %s expects %d args but gets %d in %s" 
+errArgArity g its es = printf "Measure %s expects %d args but gets %d in %s"
                          (showFix g) (length its) (length es) (showFix (EApp g es))
 
-errIte e1 e2 t1 t2   = printf "Mismatched branches in Ite: then %s : %s, else %s : %s" 
-                         (showFix e1) (showFix t1) (showFix e2) (showFix t2) 
+errIte e1 e2 t1 t2   = printf "Mismatched branches in Ite: then %s : %s, else %s : %s"
+                         (showFix e1) (showFix t1) (showFix e2) (showFix t2)
 
-errCast e t' t       = printf "Cannot cast %s of sort %s to incompatible sort %s" 
+errCast e t' t       = printf "Cannot cast %s of sort %s to incompatible sort %s"
                          (showFix e) (showFix t') (showFix t)
 
 errUnbound x         = printf "Unbound Symbol %s" (showFix x)
-errUnboundAlts x xs  = printf "Unbound Symbol %s\n Perhaps you meant: %s" 
-                        (showFix x) 
+errUnboundAlts x xs  = printf "Unbound Symbol %s\n Perhaps you meant: %s"
+                        (showFix x)
                         (foldr1 (\w s -> w ++ ", " ++ s) (showFix <$> xs))
 
 errNonFunction t     = printf "Sort %s is not a function" (showFix t)
@@ -342,26 +345,26 @@
 
 unify                              = unifyMany (Th M.empty)
 
-unifyMany θ ts ts' 
+unifyMany θ ts ts'
   | length ts == length ts'        = foldM (uncurry . unify1) θ $ zip ts ts'
   | otherwise                      = throwError $ errUnifyMany ts ts'
 
 -- unify1 _ FNum _                    = Nothing
 unify1 θ (FVar i) t                = unifyVar θ i t
 unify1 θ t (FVar i)                = unifyVar θ i t
-unify1 θ (FApp c ts) (FApp c' ts')  
-  | c == c'                        = unifyMany θ ts ts' 
-unify1 θ t1 t2  
+unify1 θ (FApp c ts) (FApp c' ts')
+  | c == c'                        = unifyMany θ ts ts'
+unify1 θ t1 t2
   | t1 == t2                       = return θ
   | otherwise                      = throwError $ errUnify t1 t2
 
-unifyVar θ i t 
+unifyVar θ i t
   = case lookupVar i θ of
-      Just t' -> if t == t' then return θ else throwError (errUnify t t') 
-      Nothing -> return $ updateVar i t θ 
+      Just t' -> if t == t' then return θ else throwError (errUnify t t')
+      Nothing -> return $ updateVar i t θ
 
 -- | Sort Substitutions
-newtype TVSubst      = Th (M.HashMap Int Sort) 
+newtype TVSubst      = Th (M.HashMap Int Sort)
 
 -- | API for manipulating substitutions
 lookupVar i (Th m)   = M.lookup i m
@@ -384,10 +387,10 @@
 -- | Deconstruct a function-sort ---------------------------------------
 ------------------------------------------------------------------------
 
-sortFunction (FFunc n ts') = return (n, ts, t) 
-  where 
+sortFunction (FFunc n ts') = return (n, ts, t)
+  where
     ts                     = take numArgs ts'
     t                      = last ts'
     numArgs                = length ts' - 1
 
-sortFunction t             = throwError $ errNonFunction t 
+sortFunction t             = throwError $ errNonFunction t
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
@@ -1,13 +1,14 @@
-{-# LANGUAGE NoMonomorphismRestriction #-}
-{-# LANGUAGE DeriveGeneric             #-}
-{-# LANGUAGE DeriveDataTypeable        #-}
-{-# LANGUAGE DeriveTraversable         #-}
-{-# LANGUAGE DeriveFoldable            #-}
-{-# LANGUAGE FlexibleInstances         #-}
-{-# LANGUAGE UndecidableInstances      #-}
-{-# LANGUAGE OverloadedStrings         #-}
-{-# LANGUAGE StandaloneDeriving        #-}
+{-# LANGUAGE DeriveDataTypeable         #-}
+{-# LANGUAGE DeriveFoldable             #-}
+{-# LANGUAGE DeriveGeneric              #-}
+{-# LANGUAGE DeriveTraversable          #-}
+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE NoMonomorphismRestriction  #-}
+{-# LANGUAGE OverloadedStrings          #-}
+{-# LANGUAGE StandaloneDeriving         #-}
+{-# LANGUAGE UndecidableInstances       #-}
 
 
 -- | This module contains the data types, operations and serialization functions
@@ -56,7 +57,7 @@
 
   -- * Expressions and Predicates
   , SymConst (..)
-  , Constant (..) 
+  , Constant (..)
   , Bop (..), Brel (..)
   , Expr (..), Pred (..)
   , eVar
@@ -156,38 +157,39 @@
   , dummyLoc, dummyPos, dummyName, isDummy
   ) where
 
-import Debug.Trace          (trace)
+import           Debug.Trace               (trace)
 
-import GHC.Generics         (Generic)
-import Data.Typeable        (Typeable)
-import Data.Generics        (Data)
+import           Data.Generics             (Data)
+import           Data.Typeable             (Typeable)
+import           GHC.Generics              (Generic)
 
-import Data.Monoid hiding   ((<>))
-import Data.Functor
-import Data.Char            (ord, chr, isAlpha, isUpper, toLower)
-import Data.List            (nub, foldl', sort, stripPrefix, intersect)
-import Data.Hashable
-import qualified Data.Foldable as F
-import Data.Traversable
-import Data.Interned
-import Data.String
-import Data.Text (Text)
-import qualified Data.Text as T
+import           Data.Char                 (chr, isAlpha, isUpper, ord, toLower)
+import qualified Data.Foldable             as F
+import           Data.Functor
+import           Data.Hashable
+import           Data.Interned
+import           Data.List                 (foldl', intersect, nub, sort,
+                                            stripPrefix)
+import           Data.Monoid               hiding ((<>))
+import           Data.String
+import           Data.Text                 (Text)
+import qualified Data.Text                 as T
+import           Data.Traversable
 
-import Data.Maybe           (fromMaybe)
-import Text.Printf          (printf)
-import Control.DeepSeq
-import Control.Arrow        ((***))
-import Control.Exception    (assert)
+import           Control.Arrow             ((***))
+import           Control.DeepSeq
+import           Control.Exception         (assert)
+import           Data.Maybe                (fromMaybe)
+import           Text.Printf               (printf)
 
-import Language.Fixpoint.Misc
-import Text.PrettyPrint.HughesPJ
-import Text.Parsec.Pos
+import           Language.Fixpoint.Misc
+import           Text.Parsec.Pos
+import           Text.PrettyPrint.HughesPJ
 
-import qualified Data.HashMap.Strict as M
-import qualified Data.HashSet        as S
-import Data.Array            hiding (indices)
-import Language.Fixpoint.Names
+import           Data.Array                hiding (indices)
+import qualified Data.HashMap.Strict       as M
+import qualified Data.HashSet              as S
+import           Language.Fixpoint.Names
 
 class Fixpoint a where
   toFix    :: a -> Doc
@@ -340,7 +342,7 @@
 fObj :: LocSymbol -> Sort
 fObj = fTyconSort . TC
 
- 
+
 ----------------------------------------------------------------------
 ------------------------------- Sorts --------------------------------
 ----------------------------------------------------------------------
@@ -348,11 +350,12 @@
 data Sort = FInt
           | FReal
           | FNum                 -- ^ numeric kind for Num tyvars
+          | FFrac                -- ^ numeric kind for Fractional tyvars
           | FObj  Symbol         -- ^ uninterpreted type
           | FVar  !Int           -- ^ fixpoint type variable
           | FFunc !Int ![Sort]   -- ^ type-var arity, in-ts ++ [out-t]
           | FApp FTycon [Sort]   -- ^ constructed type
-	      deriving (Eq, Ord, Show, Data, Typeable, Generic)
+              deriving (Eq, Ord, Show, Data, Typeable, Generic)
 
 instance Hashable Sort
 
@@ -364,6 +367,7 @@
 toFix_sort (FVar i)     = text "@"   <> parens (toFix i)
 toFix_sort FInt         = text "int"
 toFix_sort FReal        = text "real"
+toFix_sort FFrac        = text "frac"
 toFix_sort (FObj x)     = toFix x
 toFix_sort FNum         = text "num"
 toFix_sort (FFunc n ts) = text "func" <> parens ((toFix n) <> (text ", ") <> (toFix ts))
@@ -415,7 +419,7 @@
 
 data Constant = I !Integer
               | R !Double
-              | L !Text !Sort 
+              | L !Text !Sort
               deriving (Eq, Ord, Show, Data, Typeable, Generic)
 
 data Brel = Eq | Ne | Gt | Ge | Lt | Le | Ueq | Une
@@ -423,7 +427,7 @@
 
 data Bop  = Plus | Minus | Times | Div | Mod
             deriving (Eq, Ord, Show, Data, Typeable, Generic)
-	      -- NOTE: For "Mod" 2nd expr should be a constant or a var *)
+              -- NOTE: For "Mod" 2nd expr should be a constant or a var *)
 
 data Expr = ESym !SymConst
           | ECon !Constant
@@ -446,8 +450,8 @@
 instance Fixpoint Constant where
   toFix (I i)   = toFix i
   toFix (R i)   = toFix i
-  toFix (L s t) = parens $ text "lit" <+> text "\"" <> toFix s <> text "\"" <+> toFix t   
-                    
+  toFix (L s t) = parens $ text "lit" <+> text "\"" <> toFix s <> text "\"" <+> toFix t
+
 instance Fixpoint SymConst where
   toFix  = toFix . encodeSymConst
 
@@ -609,7 +613,7 @@
 -- | Generalizing Symbol, Expression, Predicate into Classes -----------
 ------------------------------------------------------------------------
 
--- | Values that can be viewed as Constants 
+-- | Values that can be viewed as Constants
 
 -- | Values that can be viewed as Expressions
 
@@ -683,7 +687,7 @@
 instance Show Reft where
   show (Reft x) = render $ toFix x
 
-data SortedReft = RR { sr_sort :: !Sort, sr_reft :: !Reft } 
+data SortedReft = RR { sr_sort :: !Sort, sr_reft :: !Reft }
                   deriving (Eq, Show, Data, Typeable, Generic)
 
 isNonTrivialSortedReft (RR _ (Reft (_, ras)))
@@ -785,7 +789,7 @@
 
 instance (Fixpoint a) => Fixpoint (SEnv a) where
   toFix (SE e) = vcat $ map pprxt $ hashMapToAscList e
-	where pprxt (x, t) = toFix x <+> colon <> colon  <+> toFix t
+        where pprxt (x, t) = toFix x <+> colon <> colon  <+> toFix t
 
 instance Fixpoint (SEnv a) => Show (SEnv a) where
   show = render . toFix
@@ -827,7 +831,7 @@
 data FixResult a = Crash [a] String
                  | Safe
                  | Unsafe ![a]
-                 | UnknownError !String 
+                 | UnknownError !String
                    deriving (Show, Generic)
 
 type FixSolution = M.HashMap Symbol Pred
@@ -1151,7 +1155,7 @@
   rnf (I x)     = rnf x
   rnf (R x)     = rnf x
   rnf (L s t) = rnf s `seq` rnf t
-  
+
 instance NFData SymConst where
   rnf (SL x) = rnf x
 
@@ -1286,7 +1290,7 @@
   toFix = pprQual
 
 instance NFData Qualifier where
-  rnf (Q x1 x2 x3 _) = rnf x1 `seq` rnf x2 `seq` rnf x3 
+  rnf (Q x1 x2 x3 _) = rnf x1 `seq` rnf x2 `seq` rnf x3
 
 pprQual (Q n xts p l) = text "qualif" <+> text (symbolString n) <> parens args <> colon <+> toFix p <+> text "//" <+> toFix l
   where args = intersperse comma (toFix <$> xts)
@@ -1350,7 +1354,7 @@
   toReft  :: r -> Reft
   ofReft  :: Reft -> r
   params  :: r -> [Symbol]          -- ^ parameters for Reft, vv + others
-  
+
 instance Monoid Pred where
   mempty      = PTrue
   mappend p q = pAnd [p, q]
diff --git a/src/Language/Fixpoint/Visitor.hs b/src/Language/Fixpoint/Visitor.hs
--- a/src/Language/Fixpoint/Visitor.hs
+++ b/src/Language/Fixpoint/Visitor.hs
@@ -3,24 +3,24 @@
 module Language.Fixpoint.Visitor (
   -- * Visitor
      Visitor (..)
-     
+
   -- * Default Visitor
   , defaultVisitor
 
   -- * Transformers
   , trans
-            
+
   -- * Accumulators
   , fold
 
   ) where
 
+import           Control.Applicative       (Applicative (), (<$>), (<*>))
+import           Control.Exception         (throw)
+import           Control.Monad.Trans.State (State, modify, runState)
 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           Data.Traversable          (traverse)
+import           Language.Fixpoint.Misc    (mapSnd)
 import           Language.Fixpoint.Types
 
 
@@ -31,14 +31,14 @@
   , ctxPred :: ctx -> Pred -> ctx
 
   -- | Transforms can access current @ctx@
-  , txExpr  :: ctx -> Expr -> Expr 
-  , txPred  :: ctx -> Pred -> Pred 
+  , 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
 ---------------------------------------------------------------------------------
@@ -49,20 +49,20 @@
   , txPred     = \_ x -> x
   , accExpr    = \_ _ -> mempty
   , accPred    = \_ _ -> mempty
-  }           
+  }
 
 
-------------------------------------------------------------------------          
+------------------------------------------------------------------------
 
-fold         :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> a 
+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 
+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 
+type VisitM acc = State acc
 
 accum :: (Monoid a) => a -> VisitM a ()
 accum = modify . mappend
@@ -81,15 +81,15 @@
 
 instance Visitable Refa where
   visit v c (RConc p) = RConc <$> visit v c p
-  visit _ _ r         = return r 
+  visit _ _ r         = return r
 
 instance Visitable Reft where
-  visit v c (Reft (vv, ras)) = (Reft . (vv,)) <$> visitMany v c ras 
+  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 :: (Monoid a) => Visitor a ctx -> ctx -> Expr -> VisitM a Expr
 visitExpr v = vE
   where
     vP      = visitPred v
@@ -97,17 +97,17 @@
                                             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@(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 (EApp f es)    = EApp f     <$> (vE c <$$> es)
     step c (ENeg e)       = ENeg       <$> vE c e
     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 :: (Monoid a) => Visitor a ctx -> ctx -> Pred -> VisitM a Pred
 visitPred v = vP
   where
     vE     = visitExpr v
@@ -115,14 +115,13 @@
                                            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 (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 (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 (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
-