diff --git a/configure b/configure
--- a/configure
+++ b/configure
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 
 ROOTHOME=`pwd`
 GHCBIN=`which ghc`
diff --git a/external/fixpoint/Makefile b/external/fixpoint/Makefile
--- a/external/fixpoint/Makefile
+++ b/external/fixpoint/Makefile
@@ -3,7 +3,11 @@
 DIRS=-I misc
 OFLAGS=$(DIRS) $(IFLAGS) $(LFLAGS) $(CFLAGS)
 
-LIBS_=-libs unix,str,graph
+OCAMLC=ocamlc
+OCAMLOPT=ocamlopt
+OCAMLBUILD=ocamlbuild -ocamlc $(OCAMLC) -ocamlopt $(OCAMLOPT)
+
+LIBS_=-libs unix,str,graph,nums
 IFLAGS_=-lflags -I,$(OCAMLGRAPHHOME)
 LFLAGS_=-lflags -cclib,-L$(OCAMLLIB)
 
@@ -38,10 +42,14 @@
   SMTZ3SRC=smtZ3.nomem.ml
 endif
 
+ifdef CCOPT
+  CFLAGS+= -cflags -ccopt,-m32
+endif
+
 all: smtz3
 	ln -sf ../misc
-	ocamlbuild -r $(LIBS) $(OFLAGS) -tags thread fixpoint.native
-	ocamlbuild -r $(OFLAGS) fix.cmxa
+	$(OCAMLBUILD) -r $(LIBS) $(OFLAGS) -tags thread fixpoint.native
+	$(OCAMLBUILD) -r $(OFLAGS) fix.cmxa
 	rm -f fixpoint.native
 	cp _build/fixpoint.native .
 
diff --git a/external/fixpoint/ast.ml b/external/fixpoint/ast.ml
--- a/external/fixpoint/ast.ml
+++ b/external/fixpoint/ast.ml
@@ -165,7 +165,7 @@
     let is_int = function
       | Int -> true
       | _   -> false
-
+    
     let is_real = function
       | Real -> true
       | _    -> false
@@ -398,11 +398,15 @@
 
 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
-      | Int i -> string_of_int i
-      | Real i -> string_of_float i ^ "0"
+      | Int i     -> string_of_int i
+      | Real i    -> string_of_float i ^ "0"
+      | Lit (s,t) -> Printf.sprintf "(lit \"%s\" %s)" s (Sort.to_string t)
 
     let print fmt s =
       to_string s |> Format.fprintf fmt "%s"
@@ -509,6 +513,8 @@
         x
     | Con (Constant.Real x) -> 
         64 + int_of_float x
+    | Con (Constant.Lit (s,_)) -> 
+        32 + Hashtbl.hash s
     | MExp es ->
         list_hash 6 es 
     | Var x -> 
@@ -1154,6 +1160,8 @@
       Some Sort.Int 
   | Con (Constant.Real _) -> 
       Some Sort.Real 
+  | Con (Constant.Lit (_, t)) ->
+      Some t 
   | Var s ->
       sortcheck_sym f s
   | Bin (e1, op, e2) -> 
diff --git a/external/fixpoint/ast.mli b/external/fixpoint/ast.mli
--- a/external/fixpoint/ast.mli
+++ b/external/fixpoint/ast.mli
@@ -16,9 +16,6 @@
  * 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.
- *
  *)
 
 (**
@@ -55,7 +52,6 @@
 
     val to_string   : t -> string
     val print       : Format.formatter -> t -> unit
-   
     val t_num       : t
     val t_obj       : t
     val t_bool      : t
@@ -67,14 +63,14 @@
     val t_app       : tycon -> t list -> t
     (* val t_fptr      : t *)
    
-    val is_bool     : t -> bool
-    val is_int      : t -> bool
-    val is_real     : t -> bool
-    val is_func     : t -> bool
-    val is_kind     : t -> bool
-    val app_of_t    : t -> (tycon * t list) option 
-    val func_of_t   : t -> (int * t list * t) option
-    val ptr_of_t    : t -> loc option
+    val is_bool      : t -> bool
+    val is_int       : t -> bool
+    val is_real      : t -> bool
+    val is_func      : t -> bool
+    val is_kind      : t -> bool
+    val app_of_t     : t -> (tycon * t list) option 
+    val func_of_t    : t -> (int * t list * t) option
+    val ptr_of_t     : t -> loc option
  
     val compat      : t -> t -> bool
     val empty_sub   : sub
@@ -105,7 +101,10 @@
 
 module Constant :
   sig
-    type t = Int of int | Real of float
+    type t = Int  of int
+           | Real of float
+           | Lit  of string * Sort.t
+
     val to_string : t -> string
     val print : Format.formatter -> t -> unit
   end
diff --git a/external/fixpoint/fixLex.mll b/external/fixpoint/fixLex.mll
--- a/external/fixpoint/fixLex.mll
+++ b/external/fixpoint/fixLex.mll
@@ -47,13 +47,27 @@
    *)
   let safe_float_of_string s = 
     try float_of_string s with ex -> 
-      let _ = Printf.printf "safe_int_of_string crashes on: %s (error = %s)" s (Printexc.to_string ex) in
+      let _ = Printf.printf "safe_float_of_string crashes on: %s (error = %s)" s (Printexc.to_string ex) in
       raise ex
 
   let safe_int_of_string s = 
     try int_of_string s with ex -> 
       let _ = Printf.printf "safe_int_of_string crashes on: %s (error = %s)" s (Printexc.to_string ex) in
       raise ex
+
+  let string_suffix_from s n = String.sub s n (String.length s - n)
+
+  let snip_begin_end str =
+    let len = String.length str in
+		String.sub str 1 (len-2)
+                            
+  (* let safe_big_int_of_string s = 
+    try Big_int.big_int_of_string (string_suffix_from s 2) with ex -> 
+      let _ = Printf.printf "safe_big_int_of_string crashes on: %s (error = %s)" s (Printexc.to_string ex) in
+      raise ex
+   *)
+
+
 }
 
 let digit    = ['0'-'9' '-']
@@ -76,6 +90,7 @@
 			              token lexbuf
                           end 
                         }
+  | '_'                 { UNDERSCORE }
   | '['                 { LB }
   | ']'                 { RB }
   | '('			        { LPAREN }
@@ -121,6 +136,7 @@
   | "ptr"               { PTR }
   | "<fun>"             { LFUN }
   (* | "fptr"           { FPTR } *)
+  | "lit"               { LIT }
   | "bool"              { BOOL }
   | "uit"               { UNINT }
   | "func"              { FUNC }
@@ -142,13 +158,10 @@
   | "reft"              { REF }
   | "@"                 { TVAR } 
   | (digit)+'.'(digit)+	{ Real (safe_float_of_string (Lexing.lexeme lexbuf)) }
-  | (digit)+	        { Num (safe_int_of_string (Lexing.lexeme lexbuf)) }
-  | (alphlet)letdig*	{ Id    (Lexing.lexeme lexbuf) }
-  | '''[^''']*'''       { let str = Lexing.lexeme lexbuf in
-			              let len = String.length str in
-			              Id (String.sub str 1 (len-2)) 
-                        }
-  
+  | (digit)+	          { Num  (safe_int_of_string (Lexing.lexeme lexbuf)) }
+  | (alphlet)letdig*	  { Id    (Lexing.lexeme lexbuf) }
+  | '''[^''']*'''       { Id (snip_begin_end (Lexing.lexeme lexbuf)) }
+  | '"'[^''']*'"'       { StringLit (snip_begin_end (Lexing.lexeme lexbuf)) }
   | eof			{ EOF }
   | _			{ 
                           begin
diff --git a/external/fixpoint/fixParse.mly b/external/fixpoint/fixParse.mly
--- a/external/fixpoint/fixParse.mly
+++ b/external/fixpoint/fixParse.mly
@@ -53,12 +53,14 @@
 %}
 
 %token <string> Id
-%token <int> Num
-%token <float> Real
+%token <int>    Num
+%token <float>  Real
+%token <string> StringLit 
 %token TVAR 
 %token TAG ID 
 %token BEXP
 %token TRUE FALSE
+%token UNDERSCORE 
 %token LPAREN  RPAREN LB RB LC RC
 %token EQ NE GT GE LT LE UEQ UNE
 %token AND OR NOT NOTWORD IMPL IFF IFFWORD FORALL SEMI COMMA COLON MID
@@ -69,7 +71,7 @@
 %token TIMES 
 %token DIV 
 %token QM DOT ASGN
-%token OBJ REAL INT NUM PTR LFUN BOOL UNINT FUNC
+%token OBJ REAL INT NUM PTR LFUN BOOL UNINT FUNC LIT
 %token SRT AXM CON CST WF SOL QUL KUT BIND ADP DDP
 %token ENV GRD LHS RHS REF
 
@@ -311,6 +313,7 @@
   | Num                                   { (A.Constant.Int $1) }
   | MINUS Num                             { (A.Constant.Int (-1 * $2)) }
   | MINUS Real                            { (A.Constant.Real (-. $2)) }
+  | LIT StringLit sort                    { (A.Constant.Lit ($2, $3)) }
   ;
 
 cons:
@@ -324,13 +327,13 @@
   ;
 
 wf:
-    ENV env REF reft                              { C.make_wf $2 $4 None }
-  | ENV env REF reft ID Num                       { C.make_wf $2 $4 (Some $6) }
+    ENV env REF reft                      { C.make_wf $2 $4 None }
+  | ENV env REF reft ID Num               { C.make_wf $2 $4 (Some $6) }
   ;
 
 tagsne:
-  Num                                             { [$1] }
-  | Num SEMI tagsne                               { $1 :: $3 }
+  Num                                     { [$1] }
+  | Num SEMI tagsne                       { $1 :: $3 }
   ;
 
 tag: 
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/proverArch.ml b/external/fixpoint/proverArch.ml
--- a/external/fixpoint/proverArch.ml
+++ b/external/fixpoint/proverArch.ml
@@ -34,7 +34,7 @@
   val sort_name   : sortDef -> Ast.Sort.tycon
   val mk_thy_sort : sortDef -> context -> sort list -> sort
   val mk_thy_app  : appDef  -> context -> sort list -> ast list -> ast
-  val theories    : sortDef list * appDef list
+  val theories    : unit -> sortDef list * appDef list
 end
 
 module type SMTSOLVER = sig
@@ -64,6 +64,7 @@
   val mkIte     : context -> ast -> ast -> ast -> ast
   val mkInt     : context -> int -> sort -> ast
   val mkReal    : context -> float -> sort -> ast
+  val mkLit     : context -> string -> sort -> ast
   val mkTrue    : context -> ast
   val mkFalse   : context -> ast
   val mkNot     : context -> ast -> ast
@@ -74,8 +75,9 @@
   val mkRel     : context -> Ast.brel   -> ast -> ast -> ast 
 
   (* Conversions *)
-  val astString : context -> ast -> string
-
+  val astString     : context -> ast -> string
+  val sortString    : context -> sort -> string
+                                           
   (* Set Theory Operations *)
   val mkSetSort     : context -> sort   -> sort
   val mkEmptySet    : context -> sort -> ast
@@ -85,6 +87,21 @@
   val mkSetCap      : context -> ast -> ast -> ast
   val mkSetDif      : context -> ast -> ast -> ast
   val mkSetSub      : context -> ast -> ast -> ast
+
+  (* Map Theory Operations *)
+
+  val mkMapSort     : context -> sort -> sort -> sort
+  val mkMapSelect   : context -> ast -> ast -> ast
+  val mkMapStore    : context -> ast -> ast -> ast -> ast
+
+
+  (* BitVector Theory Operations *)
+  val mkSizeSort    : context -> int  -> sort 
+  val mkBitSort     : context -> sort -> sort 
+  val mkBitAnd      : context -> ast  -> ast -> ast 
+  val mkBitOr       : context -> ast  -> ast -> ast
+
+
 
   (* Constructors *)
   val mkContext      : (string * string) array -> context
diff --git a/external/fixpoint/smtLIB2.ml b/external/fixpoint/smtLIB2.ml
--- a/external/fixpoint/smtLIB2.ml
+++ b/external/fixpoint/smtLIB2.ml
@@ -106,6 +106,10 @@
 let sub = "smt_set_sub"
 let com = "smt_set_com"
 
+let map = "SMT_Map"
+let sel = "smt_map_sel"
+let sto = "smt_map_sto"
+
 (* 
    (define-fun smt_set_emp () Set ((as const Set) false))
    (define-fun smt_set_mem ((x Elt) (s Set)) Bool (select s x))
@@ -119,6 +123,18 @@
 
 let (++) = List.append
 
+(* array preamble *)
+let array_preamble _ = 
+  if not !Co.map_theory then [] else
+    [ spr "(define-sort %s () (Array %s %s))" 
+        map elt elt 
+    ; spr "(define-fun %s ((m %s) (k %s)) %s (select m k))"
+        sel map elt elt 
+    ; spr "(define-fun %s ((m %s) (k %s) (v %s)) %s (store m k v))"
+        sto map elt elt map
+    ]
+
+
 (* z3 specific *)
 let z3_preamble _  
  =  [ "(set-option :auto-config false)"
@@ -146,12 +162,13 @@
         dif set set set cap com
     ; spr "(define-fun %s ((s1 %s) (s2 %s)) Bool (= %s (%s s1 s2)))"
         sub set set emp dif 
-    ] 
+    ] ++ array_preamble ()
 
+
 (* cvc4 specific *)
 let cvc4_preamble _  
  =  if not !Co.set_theory then [] else
-    [ spr "(set-logic QF_UFNIRAFS)"
+    [ spr "(set-logic QF_AUFNIRAFS)"
     ; spr "(define-sort %s () Int)"
         elt
     ; spr "(define-sort %s () (Set %s))" 
@@ -168,15 +185,11 @@
         cap set set set
     ; spr "(declare-fun %s (%s) %s)"
         com set set
-    (* 
-    ; spr "(define-fun %s ((s %s)) %s ((_ map not) s))"
-        com set set
-     *)
     ; spr "(define-fun %s ((s1 %s) (s2 %s)) %s (setminus s1 s2))"
         dif set set set
     ; spr "(define-fun %s ((s1 %s) (s2 %s)) Bool (subset s1 s2))"
         sub set set
-    ] 
+    ] ++ array_preamble ()
 
 let smtlib_preamble 
   = [ spr "(set-logic QF_UFLIA)"
@@ -189,7 +202,9 @@
     ; spr "(declare-fun %s (%s %s) %s)"   dif set set set
     ; spr "(declare-fun %s (%s %s) Bool)" sub set set 
     ; spr "(declare-fun %s (%s %s) Bool)" mem elt set 
-   
+    ; spr "(declare-fun %s (%s %s) %s)"    sel map elt elt 
+    ; spr "(declare-fun %s (%s %s %s) %s)" sto map elt elt map 
+    
     (* HIDE? 
     ; spr "(assert (forall ((x %s)) (not (%s x %s))))" 
           elt mem emp
@@ -218,6 +233,16 @@
 let mkSetDif _ s t = spr "(%s %s %s)" dif s t
 let mkSetSub _ s t = spr "(%s %s %s)" sub s t
 
+let mkMapSort c k v    = map 
+let mkMapSelect c m k  = spr "(%s %s %s)"    sel m k 
+let mkMapStore c m k v = spr "(%s %s %s %s)" sto m k v
+
+let mkSizeSort _ n = spr "%d" n                          
+let mkBitSort _ s  = spr "(_ BitVec %s)" s 
+let mkBitAnd _ x y = spr "(bvand %s %s)" x y
+let mkBitOr  _ x y = spr "(bvor  %s %s)" x y
+
+
 (******************************************************************)
 (**************** SMT IO ******************************************)
 (** https://raw.github.com/ravichugh/djs/master/src/zzz.ml ********)
@@ -364,6 +389,7 @@
 
 let stringSymbol _ s = s
 let astString _ a    = a 
+let sortString _ s   = s 
 let isBool c a       = failwith "TODO:SMTLib2.isBool"
 let boundVar me i t  = failwith "TODO:SMTLib2.boundVar"
 
@@ -383,6 +409,9 @@
                      else spr "(- %d)" (abs i)
 let mkReal _ i _   = if i >= 0. then string_of_float i ^ "0" (* add trailing 0 for floats like 1. *)
                      else spr "(- %s)" (string_of_float (i *. -1.0) ^ "0")
+
+let mkLit _ l _    = l
+                       
 let mkTrue _       = "true"
 let mkFalse _      = "false" 
 
diff --git a/external/fixpoint/smtZ3.mem.ml b/external/fixpoint/smtZ3.mem.ml
--- a/external/fixpoint/smtZ3.mem.ml
+++ b/external/fixpoint/smtZ3.mem.ml
@@ -113,6 +113,12 @@
 let mkSetSub   = Z3.mk_set_subset 
 let mkContext  = Z3.mk_context_x 
 
+
+let mkMapSort   = fun _ _ _ -> failwith "TODO: smtZ3.mem : mkMapSort"
+let mkMapSelect = fun _ _ _ -> failwith "TODO: smtZ3.mem : mkMapSelect"
+let mkMapStore  = fun _ _ _ _ -> failwith "TODO: smtZ3.mem : mkMapStore"
+
+
 (*********************************************************)
 
 let z3push me =
diff --git a/external/fixpoint/smtZ3.ml b/external/fixpoint/smtZ3.ml
new file mode 100644
--- /dev/null
+++ b/external/fixpoint/smtZ3.ml
@@ -0,0 +1,93 @@
+(*
+ * Copyright © 2008 The Regents of the University of California. All rights reserved.
+ *
+ * Permission is hereby granted, without written agreement and without
+ * license or royalty fees, to use, copy, modify, and distribute this
+ * software and its documentation for any purpose, provided that the
+ * above copyright notice and the following two paragraphs appear in
+ * all copies of this software.
+ *
+ * IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY
+ * FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES
+ * ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN
+ * IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY
+ * OF SUCH DAMAGE.
+ *
+ * THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
+ * INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY
+ * AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS
+ * ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION
+ * TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
+ *)
+
+(********************************************************************************)
+(** DUMMY SMT-Z3 Solver (for non Z3MEM builds) **********************************)
+(********************************************************************************)
+
+let assertf = FixMisc.Ops.assertf
+let msg     = "This build is NOT linked against Z3. Please rebuild with Z3MEM=true. Only possible on linux"
+
+module SMTZ3 : ProverArch.SMTSOLVER = struct
+
+type context     = ()
+type symbol      = ()   
+type sort        = () 
+type ast         = () 
+type fun_decl    = ()  
+
+let var          _   = failwith msg 
+let boundVar     _   = failwith msg
+let stringSymbol _   = failwith msg
+let funcDecl     _   = failwith msg
+let isBool _         = failwith msg
+let isInt _          = failwith msg
+let mkAll _          = failwith msg
+let mkRel _          = failwith msg
+let mkApp _          = failwith msg  
+let mkMul _          = failwith msg
+let mkDiv _          = failwith msg
+let mkAdd _          = failwith msg
+let mkSub _          = failwith msg
+let mkMod _          = failwith msg
+let mkIte _          = failwith msg
+let mkInt _          = failwith msg  
+let mkLit _          = failwith msg  
+let mkReal _         = failwith msg  
+let mkTrue _         = failwith msg
+let mkFalse _        = failwith msg
+let mkNot _          = failwith msg
+let mkAnd _          = failwith msg 
+let mkOr _           = failwith msg 
+let mkImp _          = failwith msg 
+let mkIff _          = failwith msg
+let astString _      = failwith msg
+let sortString _     = failwith msg
+let mkIntSort _      = failwith msg
+let mkRealSort _     = failwith msg
+let mkBoolSort _     = failwith msg
+let mkSetSort _      = failwith msg
+let mkEmptySet _     = failwith msg
+let mkSetAdd _       = failwith msg
+let mkSetMem _       = failwith msg
+let mkSetCup _       = failwith msg
+let mkSetCap _       = failwith msg
+let mkSetDif _       = failwith msg
+let mkSetSub _       = failwith msg
+let mkMapSort _      = failwith msg
+let mkMapSelect _    = failwith msg
+let mkMapStore _     = failwith msg
+let mkSizeSort _     = failwith msg
+let mkBitSort _      = failwith msg
+let mkBitAnd _       = failwith msg
+let mkBitOr _        = failwith msg
+let mkContext _      = failwith msg
+let unsat _          = failwith msg  
+let assertAxiom _    = failwith msg
+let assertDistinct _ = failwith msg
+let bracket _        = failwith msg
+let assertPreds _    = failwith msg
+let valid _          = failwith msg 
+let contra _         = failwith msg
+let print_stats _    = failwith msg
+
+end
diff --git a/external/fixpoint/smtZ3.nomem.ml b/external/fixpoint/smtZ3.nomem.ml
--- a/external/fixpoint/smtZ3.nomem.ml
+++ b/external/fixpoint/smtZ3.nomem.ml
@@ -51,6 +51,7 @@
 let mkMod _          = failwith msg
 let mkIte _          = failwith msg
 let mkInt _          = failwith msg  
+let mkLit _          = failwith msg  
 let mkReal _         = failwith msg  
 let mkTrue _         = failwith msg
 let mkFalse _        = failwith msg
@@ -60,6 +61,7 @@
 let mkImp _          = failwith msg 
 let mkIff _          = failwith msg
 let astString _      = failwith msg
+let sortString _     = failwith msg
 let mkIntSort _      = failwith msg
 let mkRealSort _     = failwith msg
 let mkBoolSort _     = failwith msg
@@ -71,6 +73,13 @@
 let mkSetCap _       = failwith msg
 let mkSetDif _       = failwith msg
 let mkSetSub _       = failwith msg
+let mkMapSort _      = failwith msg
+let mkMapSelect _    = failwith msg
+let mkMapStore _     = failwith msg
+let mkSizeSort _     = failwith msg
+let mkBitSort _      = failwith msg
+let mkBitAnd _       = failwith msg
+let mkBitOr _        = failwith msg
 let mkContext _      = failwith msg
 let unsat _          = failwith msg  
 let assertAxiom _    = failwith msg
diff --git a/external/fixpoint/theories.ml b/external/fixpoint/theories.ml
--- a/external/fixpoint/theories.ml
+++ b/external/fixpoint/theories.ml
@@ -26,13 +26,16 @@
 open ProverArch
 open FixMisc.Ops
 
+(***************************************************************************)
+(********************* NAMES (independent of SMT) **************************)
+(***************************************************************************)
+
+(********************* Sets ************************************************)
+
 let set_tycon  = So.tycon "Set_Set"
 let t_set a    = So.t_app set_tycon [a]
 
 (* API *)
-let is_interp t = t = set_tycon
-
-(* API *)
 let emp0 = ( Sy.of_string "Set_empty"
            , So.t_func 1 [So.t_int; t_set (So.t_generic 0)] )
 
@@ -45,7 +48,6 @@
 let mem = ( Sy.of_string "Set_mem"
           , So.t_func 1 [So.t_generic 0; t_set (So.t_generic 0); So.t_bool] )
 
-
 let cup = ( Sy.of_string "Set_cup"
           , So.t_func 1 [t_set (So.t_generic 0); t_set (So.t_generic 0); t_set (So.t_generic 0)])
 
@@ -58,11 +60,58 @@
 let sub = ( Sy.of_string "Set_sub" 
           , So.t_func 1 [t_set (So.t_generic 0); t_set (So.t_generic 0); So.t_bool] )
 
+(********************* Maps ************************************************)
+
+let map_tycon  = So.tycon "Map_t"
+
+let t_map k v  = So.t_app map_tycon [k; v]
+
+let select     = let k = So.t_generic 0 in
+                 let v = So.t_generic 1 in
+                 ( Sy.of_string "Map_select"
+                 , So.t_func 2 [t_map k v; k; v] )
+
+let store      = let k = So.t_generic 0 in
+                 let v = So.t_generic 1 in
+                 ( Sy.of_string "Map_store"
+                 , So.t_func 2 [t_map k v; k; v; t_map k v] )
+
+
+
+(********************* Maps ************************************************)
+
+let bv_tycon     = So.tycon "BitVec"
+let sz32_tycon   = So.tycon "Size32"
+let sz64_tycon   = So.tycon "Size64"
+let t_bv a       = So.t_app bv_tycon [a]
+
+let bv_binop op  = let k = So.t_generic 0 in
+                   ( Sy.of_string op 
+                   , So.t_func 1 [t_bv k; t_bv k; t_bv k] ) 
+
+let bvand        = bv_binop "bvand"
+let bvor         = bv_binop "bvor"
+
+                 
+(********************* All Theories ****************************************)
+(** WARNING: DO NOT PUT INSIDE MakeTheory; adds SMT dependency *************)
+(***************************************************************************)
+
+(* API *)
+let is_interp t = List.mem t [set_tycon; map_tycon; sz32_tycon; sz64_tycon; bv_tycon]
+
+(* API *)
 let interp_syms _ 
-  = if !Constants.set_theory 
-     then [emp0; emp; sng; mem; cup; cap; dif; sub]
-     else []
+  = []
+    |> (!Constants.set_theory <?> (++) [emp0  ; emp; sng; mem; cup; cap; dif; sub])
+    |> (!Constants.map_theory <?> (++) [select; store])
+    |> (!Constants.bit_theory <?> (++) [bvand ; bvor])
 
+
+(***************************************************************************)
+(***************************************************************************)
+(***************************************************************************)
+
 module MakeTheory(SMT : SMTSOLVER): 
   (THEORY with type context = SMT.context 
           and  type sort    = SMT.sort
@@ -90,10 +139,41 @@
 let sym_sort d  = d.sy_sort
 
 (***************************************************************************)
-(******************** Theory of Sets ***************************************)
+(********* Wrappers Around Z3 Constructors For Last-Minute Checking ********)
 (***************************************************************************)
 
-let set_set : sortDef = 
+let app_sort_arity def = match So.func_of_t def.sy_sort with
+  | Some (n,_,_) -> n
+  | None         -> assertf "Theories: app with non-function symbol %s" 
+                    (Sy.to_string def.sy_name)
+
+let check_app_arities def tArgs eArgs = match So.func_of_t def.sy_sort with
+  | Some (n, ts,_) 
+     -> asserts (n = List.length tArgs)  
+          "Theories: app with mismatched sorts %s" (Sy.to_string def.sy_name);
+        asserts (List.length ts = List.length eArgs) 
+          "Theories: app with mismatched args %s" (Sy.to_string def.sy_name) 
+  | None         
+     -> assertf "Theories: app with non-function symbol %s" 
+          (Sy.to_string def.sy_name)
+
+
+(* API *)
+let mk_thy_app def c ts es = 
+  check_app_arities def ts es;
+  def.sy_emb c ts es
+
+(* API *)
+let mk_thy_sort def c ts = 
+  asserts (List.length ts = def.so_arity) 
+    "Theories: app with mismatched sorts %s" (So.tycon_string def.so_name);
+  def.so_emb c ts 
+
+
+(** Theory of Sets *********************************************************)
+
+
+let set_t : sortDef = 
   { so_name  = set_tycon 
   ; so_arity = 1 
   ; so_emb   = fun c -> function 
@@ -101,7 +181,6 @@
                  | _ -> assertf "Set_set: type mismatch"
   }  
 
-
 let set_empty : appDef  = 
   { sy_name  = fst emp0
   ; sy_sort  = snd emp0 
@@ -110,8 +189,6 @@
                  | _        -> assertf "Set_empty: type mismatch"
   }
 
-
-
 let set_emp : appDef  = 
   { sy_name  = fst emp 
   ; sy_sort  = snd emp 
@@ -133,7 +210,7 @@
   { sy_name = fst mem 
   ; sy_sort = snd mem
   ; sy_emb  = fun c ts es -> match ts, es with
-                 | [t], [e;es] -> SMT.mkSetMem c e es 
+                 | [_], [e;es] -> SMT.mkSetMem c e es 
                  | _           -> assertf "Set_mem: type mismatch"
   }
 
@@ -169,47 +246,102 @@
                  | _            -> assertf "Set_dif: type mismatch"
   }
 
-(***************************************************************************)
-(********* Wrappers Around Z3 Constructors For Last-Minute Checking ********)
-(***************************************************************************)
+(* API *)
+let theory_set 
+  = ([ set_t ]
+    ,[ set_emp 
+     ; set_empty 
+     ; set_sng 
+     ; set_mem 
+     ; set_cup 
+     ; set_cap 
+     ; set_dif 
+     ; set_sub ])
 
-let app_sort_arity def = match So.func_of_t def.sy_sort with
-  | Some (n,_,_) -> n
-  | None         -> assertf "Theories: app with non-function symbol %s" 
-                    (Sy.to_string def.sy_name)
+(** Theory of Maps *********************************************************)
 
-let check_app_arities def tArgs eArgs = match So.func_of_t def.sy_sort with
-  | Some (n, ts,_) 
-     -> asserts (n = List.length tArgs)  
-          "Theories: app with mismatched sorts %s" (Sy.to_string def.sy_name);
-        asserts (List.length ts = List.length eArgs) 
-          "Theories: app with mismatched args %s" (Sy.to_string def.sy_name) 
-  | None         
-     -> assertf "Theories: app with non-function symbol %s" 
-          (Sy.to_string def.sy_name)
+let map_t : sortDef = 
+  { so_name  = map_tycon 
+  ; so_arity = 2 
+  ; so_emb   = fun c -> function 
+                 | [k; v] -> SMT.mkMapSort c k v 
+                 | _      -> assertf "Map_t: type mismatch"
+  }  
 
+let map_select : appDef  = 
+  { sy_name = fst select 
+  ; sy_sort = snd select 
+  ; sy_emb  = fun c ts es -> match ts, es with
+                 | [_; _], [m; k] -> SMT.mkMapSelect c m k 
+                 | _           -> assertf "Map_select: type mismatch"
+  }
 
+let map_store : appDef  = 
+  { sy_name = fst store 
+  ; sy_sort = snd store 
+  ; sy_emb  = fun c ts es -> match ts, es with
+                 | [_; _], [m; k; v] -> SMT.mkMapStore c m k v 
+                 | _           -> assertf "Map_store: type mismatch"
+  }
+
 (* API *)
-let mk_thy_app def c ts es = 
-  check_app_arities def ts es;
-  def.sy_emb c ts es
+let theory_map
+  = ([map_t], [map_select; map_store])
 
+(** Theory of Bitvectors ***************************************************)
+
+let size32_t : sortDef =
+  { so_name  = sz32_tycon 
+  ; so_arity = 1 
+  ; so_emb   = fun c -> function 
+                 | [_] -> SMT.mkSizeSort c 32 
+                 | _   -> assertf "Map_t: type mismatch"
+  }  
+
+let size64_t : sortDef =
+  { so_name  = sz64_tycon 
+  ; so_arity = 1 
+  ; so_emb   = fun c   -> function 
+                 | [_] -> SMT.mkSizeSort c 64 
+                 | _   -> assertf "Map_t: type mismatch"
+  }  
+    
+let bit_t : sortDef =
+  { so_name  = bv_tycon 
+  ; so_arity = 1 
+  ; so_emb   = fun c -> function 
+                 | [n] -> SMT.mkBitSort c n 
+                 | _   -> assertf "BitVector: type mismatch"
+  }  
+
+let bit_and : appDef  = 
+  { sy_name = fst bvand 
+  ; sy_sort = snd bvand  
+  ; sy_emb  = fun c ts es -> match ts, es with
+                 | [_], [x; y] -> SMT.mkBitAnd c x y 
+                 | _           -> assertf "bit_and: type mismatch"
+  }
+
+let bit_or : appDef  = 
+  { sy_name = fst bvor
+  ; sy_sort = snd bvor
+  ; sy_emb  = fun c ts es -> match ts, es with
+                 | [_], [x; y] -> SMT.mkBitOr c x y 
+                 | _           -> assertf "bit_or: type mismatch"
+  }
+
 (* API *)
-let mk_thy_sort def c ts = 
-  asserts (List.length ts = def.so_arity) 
-    "Theories: app with mismatched sorts %s" (So.tycon_string def.so_name);
-  def.so_emb c ts 
+let theory_bit
+  = ([size32_t; size64_t; bit_t], [bit_and; bit_or])
+    
+(** Theory Composition *****************************************************)
 
 (* API *)
-let theories = 
-  ([set_set], [set_emp; 
-	       set_empty; 
-               set_sng; 
-               set_mem; 
-               set_cup; 
-               set_cap; 
-               set_dif; 
-               set_sub])
+let theories () = 
+  let add_thy (t1,s1) (t2,s2) = (t1 ++ t2, s1 ++ s2) in
+  ([], [])
+  |> (!Constants.set_theory <?> add_thy theory_set)
+  |> (!Constants.map_theory <?> add_thy theory_map)
+  |> (!Constants.bit_theory <?> add_thy theory_bit)
 
-  
 end
diff --git a/external/fixpoint/tpGen.ml b/external/fixpoint/tpGen.ml
--- a/external/fixpoint/tpGen.ml
+++ b/external/fixpoint/tpGen.ml
@@ -133,17 +133,20 @@
     if So.is_bool t then me.tbool else
       if So.is_int t then me.tint else
         if So.is_real t then me.treal else
-          match z3TypeThy me t with 
-            | Some t' -> t'
-            | None    -> me.tint
+          Misc.maybe_default (z3TypeThy me t) me.tint
+          (* match z3TypeThy me t with 
+              | Some t' -> t'
+              | None    -> me.tint *) 
   end t t
 
-and z3TypeThy me t = match So.app_of_t t with
- | Some (c, ts) when H.mem me.thy_sortm c -> 
+and z3TypeThy me t =
+  match So.app_of_t t with
+  | Some (c, ts) when H.mem me.thy_sortm c -> 
      let def = H.find me.thy_sortm c   in
      let zts = List.map (z3Type me) ts in
      Some (Th.mk_thy_sort def me.c zts)
- | _ -> None 
+  | _ ->
+     None 
  
 (***********************************************************************)
 (********************** Identifiers ************************************)
@@ -284,11 +287,17 @@
   | (e1, e2) -> 
       SMT.mkMul me.c (z3Exp me env e1) (z3Exp me env e2)
 
-and z3Exp me env = function
-  | A.Con (A.Constant.Int i), _ -> 
+and z3Con me env = function
+  | A.Constant.Int i -> 
       SMT.mkInt me.c i me.tint 
-  | A.Con (A.Constant.Real i), _ -> 
+  | A.Constant.Real i -> 
       SMT.mkReal me.c i me.treal
+  | A.Constant.Lit (l, t) ->
+      SMT.mkLit me.c l (z3Type me t)
+                
+and z3Exp me env = function
+  | A.Con c, _ ->
+      z3Con me env c
   | A.Var s, _ -> 
       z3Var me env s
   | A.Cst ((A.App (f, es), _), t), _ when (H.mem me.thy_symm f) -> 
@@ -398,7 +407,7 @@
 (************************************************************************)
 
 let create_theories () =
-  Th.theories 
+  Th.theories () 
   |> (Misc.hashtbl_of_list_with Th.sort_name <**> Misc.hashtbl_of_list_with Th.sym_name)
 
 let assert_distinct_constants me env = function [] -> () | cs -> 
diff --git a/external/misc/constants.ml b/external/misc/constants.ml
--- a/external/misc/constants.ml
+++ b/external/misc/constants.ml
@@ -80,7 +80,9 @@
 let gen_qual_sorts              = ref true  (* -no-gen-qual-sorts  *)
 let web_demo                    = ref false (* -web-demo *)
 let simple                      = ref true  (* -simple  *) 
+let bit_theory                  = ref true  (* -bit-theory  *) 
 let set_theory                  = ref true  (* -set-theory  *) 
+let map_theory                  = ref true  (* -map-theory  *) 
 let ueq_all_sorts               = ref false (* -ueq-all-sorts *)
 
 (* JHALA: what do these do ? *)
@@ -244,9 +246,15 @@
    ( "-nosimple"
    , Arg.Clear simple
    , " Directly propagate qualifiers for simple constraints (K1 <: K2) [true]");
+   ( "-nobittheory"
+   , Arg.Clear bit_theory
+   , " Support for SMT bitvector theory [true]");
    ( "-nosettheory"
    , Arg.Clear set_theory
-   , " Support for set theory on Z3 [true]");
+   , " Support for SMT set theory [true]");
+   ( "-nomaptheory"
+   , Arg.Clear map_theory
+   , " Support for SMT map theory [true]");
    ("-psimple", 
     Arg.Set psimple, 
     " prioritize simple constraints [true]");
diff --git a/external/ocamlgraph/.depend b/external/ocamlgraph/.depend
--- a/external/ocamlgraph/.depend
+++ b/external/ocamlgraph/.depend
@@ -1,128 +1,128 @@
-lib/bitv.cmo : lib/bitv.cmi
-lib/bitv.cmx : lib/bitv.cmi
-lib/heap.cmo : lib/heap.cmi
-lib/heap.cmx : lib/heap.cmi
-lib/unionfind.cmo : lib/unionfind.cmi
-lib/unionfind.cmx : lib/unionfind.cmi
-lib/bitv.cmi :
-lib/heap.cmi :
-lib/unionfind.cmi :
-src/blocks.cmo : src/util.cmi src/sig.cmi
-src/blocks.cmx : src/util.cmx src/sig.cmi
-src/builder.cmo : src/sig.cmi src/builder.cmi
-src/builder.cmx : src/sig.cmi src/builder.cmi
-src/classic.cmo : src/sig.cmi src/builder.cmi src/classic.cmi
-src/classic.cmx : src/sig.cmi src/builder.cmx src/classic.cmi
-src/cliquetree.cmo : src/util.cmi src/sig.cmi src/persistent.cmi \
-    src/oper.cmi src/gmap.cmi src/builder.cmi src/cliquetree.cmi
-src/cliquetree.cmx : src/util.cmx src/sig.cmi src/persistent.cmx \
-    src/oper.cmx src/gmap.cmx src/builder.cmx src/cliquetree.cmi
-src/components.cmo : src/util.cmi src/sig.cmi src/components.cmi
-src/components.cmx : src/util.cmx src/sig.cmi src/components.cmi
-src/delaunay.cmo : src/delaunay.cmi
-src/delaunay.cmx : src/delaunay.cmi
-src/dot.cmo : src/dot_parser.cmi src/dot_lexer.cmo src/dot_ast.cmi \
+lib/bitv.cmo: lib/bitv.cmi
+lib/bitv.cmx: lib/bitv.cmi
+lib/heap.cmo: lib/heap.cmi
+lib/heap.cmx: lib/heap.cmi
+lib/unionfind.cmo: lib/unionfind.cmi
+lib/unionfind.cmx: lib/unionfind.cmi
+lib/bitv.cmi:
+lib/heap.cmi:
+lib/unionfind.cmi:
+src/blocks.cmo: src/util.cmi src/sig.cmi
+src/blocks.cmx: src/util.cmx src/sig.cmi
+src/builder.cmo: src/sig.cmi src/builder.cmi
+src/builder.cmx: src/sig.cmi src/builder.cmi
+src/classic.cmo: src/sig.cmi src/builder.cmi src/classic.cmi
+src/classic.cmx: src/sig.cmi src/builder.cmx src/classic.cmi
+src/cliquetree.cmo: src/util.cmi src/sig.cmi src/persistent.cmi src/oper.cmi \
+    src/gmap.cmi src/builder.cmi src/cliquetree.cmi
+src/cliquetree.cmx: src/util.cmx src/sig.cmi src/persistent.cmx src/oper.cmx \
+    src/gmap.cmx src/builder.cmx src/cliquetree.cmi
+src/components.cmo: src/util.cmi src/sig.cmi src/components.cmi
+src/components.cmx: src/util.cmx src/sig.cmi src/components.cmi
+src/delaunay.cmo: src/delaunay.cmi
+src/delaunay.cmx: src/delaunay.cmi
+src/dot.cmo: src/dot_parser.cmi src/dot_lexer.cmo src/dot_ast.cmi \
     src/builder.cmi src/dot.cmi
-src/dot.cmx : src/dot_parser.cmx src/dot_lexer.cmx src/dot_ast.cmi \
+src/dot.cmx: src/dot_parser.cmx src/dot_lexer.cmx src/dot_ast.cmi \
     src/builder.cmx src/dot.cmi
-src/dot_lexer.cmo : src/dot_parser.cmi src/dot_ast.cmi
-src/dot_lexer.cmx : src/dot_parser.cmx src/dot_ast.cmi
-src/dot_parser.cmo : src/dot_ast.cmi src/dot_parser.cmi
-src/dot_parser.cmx : src/dot_ast.cmi src/dot_parser.cmi
-src/flow.cmo : src/util.cmi src/sig.cmi src/flow.cmi
-src/flow.cmx : src/util.cmx src/sig.cmi src/flow.cmi
-src/gcoloring.cmo : src/traverse.cmi src/sig.cmi src/gcoloring.cmi
-src/gcoloring.cmx : src/traverse.cmx src/sig.cmi src/gcoloring.cmi
-src/gmap.cmo : src/sig.cmi src/gmap.cmi
-src/gmap.cmx : src/sig.cmi src/gmap.cmi
-src/gml.cmo : src/builder.cmi src/gml.cmi
-src/gml.cmx : src/builder.cmx src/gml.cmi
-src/gpath.cmo : src/util.cmi src/sig.cmi lib/heap.cmi src/gpath.cmi
-src/gpath.cmx : src/util.cmx src/sig.cmi lib/heap.cmx src/gpath.cmi
-src/graphviz.cmo : src/graphviz.cmi
-src/graphviz.cmx : src/graphviz.cmi
-src/imperative.cmo : src/sig.cmi src/blocks.cmo lib/bitv.cmi \
+src/dot_lexer.cmo: src/dot_parser.cmi src/dot_ast.cmi
+src/dot_lexer.cmx: src/dot_parser.cmx src/dot_ast.cmi
+src/dot_parser.cmo: src/dot_ast.cmi src/dot_parser.cmi
+src/dot_parser.cmx: src/dot_ast.cmi src/dot_parser.cmi
+src/flow.cmo: src/util.cmi src/sig.cmi src/flow.cmi
+src/flow.cmx: src/util.cmx src/sig.cmi src/flow.cmi
+src/gcoloring.cmo: src/traverse.cmi src/sig.cmi src/gcoloring.cmi
+src/gcoloring.cmx: src/traverse.cmx src/sig.cmi src/gcoloring.cmi
+src/gmap.cmo: src/sig.cmi src/gmap.cmi
+src/gmap.cmx: src/sig.cmi src/gmap.cmi
+src/gml.cmo: src/builder.cmi src/gml.cmi
+src/gml.cmx: src/builder.cmx src/gml.cmi
+src/gpath.cmo: src/util.cmi src/sig.cmi lib/heap.cmi src/gpath.cmi
+src/gpath.cmx: src/util.cmx src/sig.cmi lib/heap.cmx src/gpath.cmi
+src/graphviz.cmo: src/graphviz.cmi
+src/graphviz.cmx: src/graphviz.cmi
+src/imperative.cmo: src/sig.cmi src/blocks.cmo lib/bitv.cmi \
     src/imperative.cmi
-src/imperative.cmx : src/sig.cmi src/blocks.cmx lib/bitv.cmx \
+src/imperative.cmx: src/sig.cmi src/blocks.cmx lib/bitv.cmx \
     src/imperative.cmi
-src/kruskal.cmo : src/util.cmi lib/unionfind.cmi src/sig.cmi src/kruskal.cmi
-src/kruskal.cmx : src/util.cmx lib/unionfind.cmx src/sig.cmi src/kruskal.cmi
-src/mcs_m.cmo : src/util.cmi src/sig.cmi src/persistent.cmi src/oper.cmi \
+src/kruskal.cmo: src/util.cmi lib/unionfind.cmi src/sig.cmi src/kruskal.cmi
+src/kruskal.cmx: src/util.cmx lib/unionfind.cmx src/sig.cmi src/kruskal.cmi
+src/mcs_m.cmo: src/util.cmi src/sig.cmi src/persistent.cmi src/oper.cmi \
     src/imperative.cmi src/gmap.cmi src/builder.cmi src/mcs_m.cmi
-src/mcs_m.cmx : src/util.cmx src/sig.cmi src/persistent.cmx src/oper.cmx \
+src/mcs_m.cmx: src/util.cmx src/sig.cmi src/persistent.cmx src/oper.cmx \
     src/imperative.cmx src/gmap.cmx src/builder.cmx src/mcs_m.cmi
-src/md.cmo : src/sig.cmi src/oper.cmi src/gmap.cmi src/cliquetree.cmi \
+src/md.cmo: src/sig.cmi src/oper.cmi src/gmap.cmi src/cliquetree.cmi \
     src/builder.cmi src/md.cmi
-src/md.cmx : src/sig.cmi src/oper.cmx src/gmap.cmx src/cliquetree.cmx \
+src/md.cmx: src/sig.cmi src/oper.cmx src/gmap.cmx src/cliquetree.cmx \
     src/builder.cmx src/md.cmi
-src/minsep.cmo : src/sig.cmi src/oper.cmi src/components.cmi src/minsep.cmi
-src/minsep.cmx : src/sig.cmi src/oper.cmx src/components.cmx src/minsep.cmi
-src/oper.cmo : src/sig.cmi src/builder.cmi src/oper.cmi
-src/oper.cmx : src/sig.cmi src/builder.cmx src/oper.cmi
-src/pack.cmo : src/traverse.cmi src/topological.cmi src/sig.cmi src/rand.cmi \
+src/minsep.cmo: src/sig.cmi src/oper.cmi src/components.cmi src/minsep.cmi
+src/minsep.cmx: src/sig.cmi src/oper.cmx src/components.cmx src/minsep.cmi
+src/oper.cmo: src/sig.cmi src/builder.cmi src/oper.cmi
+src/oper.cmx: src/sig.cmi src/builder.cmx src/oper.cmi
+src/pack.cmo: src/traverse.cmi src/topological.cmi src/sig.cmi src/rand.cmi \
     src/oper.cmi src/kruskal.cmi src/imperative.cmi src/graphviz.cmi \
     src/gpath.cmi src/gml.cmi src/flow.cmi src/dot.cmi src/components.cmi \
     src/classic.cmi src/builder.cmi src/pack.cmi
-src/pack.cmx : src/traverse.cmx src/topological.cmx src/sig.cmi src/rand.cmx \
+src/pack.cmx: src/traverse.cmx src/topological.cmx src/sig.cmi src/rand.cmx \
     src/oper.cmx src/kruskal.cmx src/imperative.cmx src/graphviz.cmx \
     src/gpath.cmx src/gml.cmx src/flow.cmx src/dot.cmx src/components.cmx \
     src/classic.cmx src/builder.cmx src/pack.cmi
-src/persistent.cmo : src/util.cmi src/sig.cmi src/blocks.cmo \
+src/persistent.cmo: src/util.cmi src/sig.cmi src/blocks.cmo \
     src/persistent.cmi
-src/persistent.cmx : src/util.cmx src/sig.cmi src/blocks.cmx \
+src/persistent.cmx: src/util.cmx src/sig.cmi src/blocks.cmx \
     src/persistent.cmi
-src/rand.cmo : src/sig.cmi src/delaunay.cmi src/builder.cmi src/rand.cmi
-src/rand.cmx : src/sig.cmi src/delaunay.cmx src/builder.cmx src/rand.cmi
-src/strat.cmo : src/sig.cmi src/strat.cmi
-src/strat.cmx : src/sig.cmi src/strat.cmi
-src/topological.cmo : src/sig.cmi src/topological.cmi
-src/topological.cmx : src/sig.cmi src/topological.cmi
-src/traverse.cmo : src/sig.cmi src/traverse.cmi
-src/traverse.cmx : src/sig.cmi src/traverse.cmi
-src/util.cmo : src/sig.cmi src/util.cmi
-src/util.cmx : src/sig.cmi src/util.cmi
-src/version.cmo :
-src/version.cmx :
-src/builder.cmi : src/sig.cmi
-src/classic.cmi : src/sig.cmi
-src/cliquetree.cmi : src/sig.cmi
-src/components.cmi : src/util.cmi src/sig.cmi
-src/delaunay.cmi :
-src/dot.cmi : src/dot_ast.cmi src/builder.cmi
-src/dot_ast.cmi :
-src/dot_parser.cmi : src/dot_ast.cmi
-src/flow.cmi : src/sig.cmi
-src/gcoloring.cmi : src/sig.cmi
-src/gmap.cmi : src/sig.cmi
-src/gml.cmi : src/builder.cmi
-src/gpath.cmi : src/sig.cmi
-src/graphviz.cmi :
-src/imperative.cmi : src/sig.cmi
-src/kruskal.cmi : src/sig.cmi
-src/mcs_m.cmi : src/sig.cmi
-src/md.cmi : src/sig.cmi
-src/minsep.cmi : src/sig.cmi
-src/oper.cmi : src/sig.cmi src/builder.cmi
-src/pack.cmi : src/sig_pack.cmi
-src/persistent.cmi : src/sig.cmi
-src/rand.cmi : src/sig.cmi src/builder.cmi
-src/sig.cmi :
-src/sig_pack.cmi :
-src/strat.cmi : src/sig.cmi
-src/topological.cmi : src/sig.cmi
-src/traverse.cmi : src/sig.cmi
-src/util.cmi : src/sig.cmi
-editor/ed_display.cmo :
-editor/ed_display.cmx :
-editor/ed_draw.cmo : src/components.cmi
-editor/ed_draw.cmx : src/components.cmx
-editor/ed_graph.cmo : src/traverse.cmi src/imperative.cmi src/graphviz.cmi \
+src/rand.cmo: src/sig.cmi src/delaunay.cmi src/builder.cmi src/rand.cmi
+src/rand.cmx: src/sig.cmi src/delaunay.cmx src/builder.cmx src/rand.cmi
+src/strat.cmo: src/sig.cmi src/strat.cmi
+src/strat.cmx: src/sig.cmi src/strat.cmi
+src/topological.cmo: src/sig.cmi src/topological.cmi
+src/topological.cmx: src/sig.cmi src/topological.cmi
+src/traverse.cmo: src/sig.cmi src/traverse.cmi
+src/traverse.cmx: src/sig.cmi src/traverse.cmi
+src/util.cmo: src/sig.cmi src/util.cmi
+src/util.cmx: src/sig.cmi src/util.cmi
+src/version.cmo:
+src/version.cmx:
+src/builder.cmi: src/sig.cmi
+src/classic.cmi: src/sig.cmi
+src/cliquetree.cmi: src/sig.cmi
+src/components.cmi: src/util.cmi src/sig.cmi
+src/delaunay.cmi:
+src/dot.cmi: src/dot_ast.cmi src/builder.cmi
+src/dot_ast.cmi:
+src/dot_parser.cmi: src/dot_ast.cmi
+src/flow.cmi: src/sig.cmi
+src/gcoloring.cmi: src/sig.cmi
+src/gmap.cmi: src/sig.cmi
+src/gml.cmi: src/builder.cmi
+src/gpath.cmi: src/sig.cmi
+src/graphviz.cmi:
+src/imperative.cmi: src/sig.cmi
+src/kruskal.cmi: src/sig.cmi
+src/mcs_m.cmi: src/sig.cmi
+src/md.cmi: src/sig.cmi
+src/minsep.cmi: src/sig.cmi
+src/oper.cmi: src/sig.cmi src/builder.cmi
+src/pack.cmi: src/sig_pack.cmi
+src/persistent.cmi: src/sig.cmi
+src/rand.cmi: src/sig.cmi src/builder.cmi
+src/sig.cmi:
+src/sig_pack.cmi:
+src/strat.cmi: src/sig.cmi
+src/topological.cmi: src/sig.cmi
+src/traverse.cmi: src/sig.cmi
+src/util.cmi: src/sig.cmi
+editor/ed_display.cmo:
+editor/ed_display.cmx:
+editor/ed_draw.cmo: src/components.cmi
+editor/ed_draw.cmx: src/components.cmx
+editor/ed_graph.cmo: src/traverse.cmi src/imperative.cmi src/graphviz.cmi \
     src/gml.cmi src/dot_ast.cmi src/dot.cmi src/components.cmi \
     src/builder.cmi
-editor/ed_graph.cmx : src/traverse.cmx src/imperative.cmx src/graphviz.cmx \
+editor/ed_graph.cmx: src/traverse.cmx src/imperative.cmx src/graphviz.cmx \
     src/gml.cmx src/dot_ast.cmi src/dot.cmx src/components.cmx \
     src/builder.cmx
-editor/ed_hyper.cmo :
-editor/ed_hyper.cmx :
-editor/ed_main.cmo :
-editor/ed_main.cmx :
+editor/ed_hyper.cmo:
+editor/ed_hyper.cmx:
+editor/ed_main.cmo:
+editor/ed_main.cmx:
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 Feb 6 22:49:24 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.1.1
+version:             0.2.2.0
 Copyright:           2010-15 Ranjit Jhala, University of California, San Diego.
 synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
 homepage:            https://github.com/ucsd-progsys/liquid-fixpoint
@@ -148,6 +148,7 @@
                    Language.Fixpoint.Errors,
                    Language.Fixpoint.Config,
                    Language.Fixpoint.Types,
+                   Language.Fixpoint.Bitvector,
                    Language.Fixpoint.Visitor,
                    Language.Fixpoint.Sort,
                    Language.Fixpoint.Interface, 
diff --git a/src/Language/Fixpoint/Bitvector.hs b/src/Language/Fixpoint/Bitvector.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Fixpoint/Bitvector.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE DeriveGeneric             #-}
+{-# LANGUAGE DeriveDataTypeable        #-}
+
+module Language.Fixpoint.Bitvector
+       ( -- * Sizes 
+         BvSize (..)
+
+         -- * Operators
+       , BvOp (..)
+
+         -- * BitVector Sort Constructor
+       , mkSort 
+
+         -- * BitVector Expression Constructor 
+       , eOp
+
+       ) 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)
+
+data Bv     = Bv BvSize String 
+
+data BvSize = S32   | S64
+              deriving (Eq, Ord, Show, Data, Typeable, Generic)
+
+data BvOp   = BvAnd | BvOr
+              deriving (Eq, Ord, Show, Data, Typeable, Generic)
+
+-- | Construct the bitvector `Sort` from its `BvSize`
+
+mkSort :: BvSize -> Sort
+mkSort s = fApp (Left bvTyCon) [sizeSort s]
+
+-- | Construct an `Expr` using a raw string, e.g. (Bv S32 "#x02000000")
+instance Expression Bv where
+  expr (Bv sz v) = ECon $ L (T.pack v) (mkSort sz)
+
+-- | Apply some bitvector operator to a list of arguments
+
+eOp :: BvOp -> [Expr] -> Expr
+eOp o es = EApp (opName o) es
+
+
+--------------------------------------------------------------------
+
+opName :: BvOp -> LocSymbol
+opName BvAnd = dummyLoc bvAndName
+opName BvOr  = dummyLoc bvOrName
+
+sizeSort     = (`FApp` []) . sizeTC
+sizeTC       = symbolFTycon . dummyLoc . sizeName 
+sizeName S32 = size32Name
+sizeName S64 = size64Name
+
+bvTyCon      = symbolFTycon $ dummyLoc bitVecName
+
+-- s32TyCon     = symbolFTycon $ dummyLoc size32Name 
+-- s64TyCon     = symbolFTycon $ dummyLoc size64Name
+
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
@@ -44,6 +44,7 @@
   , strConName
   , vvName
   , symSepName
+  , size32Name, size64Name, bitVecName, bvAndName, bvOrName
   , prims
 ) where
 
@@ -250,6 +251,12 @@
 vvName       = "VV"
 symSepName   = '#'
 
+size32Name   = "Size32" :: Symbol 
+size64Name   = "Size64" :: Symbol
+bitVecName   = "BitVec" :: Symbol
+bvOrName     = "bvor"   :: Symbol
+bvAndName    = "bvAnd"  :: Symbol
+
 prims :: [Symbol]
 prims = [ propConName
         , hpropConName
@@ -265,6 +272,14 @@
         , "Set_empty"
         , "Set_mem"
         , "Set_sub"
+        , "Map_t"
+        , "Map_select"
+        , "Map_store"
+        , size32Name
+        , size64Name
+        , bitVecName
+        , bvOrName 
+        , bvAndName
         , "FAppTy" 
         ]
 
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
@@ -275,23 +275,30 @@
 --------------------------------------------------------------------------
 
 elt, set :: Raw
-elt = "Elt"
-set = "Set"
+elt  = "Elt"
+set  = "Set"
+map  = "Map"
+bit  = "BitVec"
+sz32 = "Size32"
+sz64 = "Size64"
+             
 
 emp, add, cup, cap, mem, dif, sub, com :: Raw
-emp = "smt_set_emp"
-add = "smt_set_add"
-cup = "smt_set_cup"
-cap = "smt_set_cap"
-mem = "smt_set_mem"
-dif = "smt_set_dif"
-sub = "smt_set_sub"
-com = "smt_set_com"
-
+emp   = "smt_set_emp"
+add   = "smt_set_add"
+cup   = "smt_set_cup"
+cap   = "smt_set_cap"
+mem   = "smt_set_mem"
+dif   = "smt_set_dif"
+sub   = "smt_set_sub"
+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)]
+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 
@@ -328,6 +335,7 @@
         (sub, set, set, emp, dif)
     ]
 
+
 smtlibPreamble
   = [        "(set-logic QF_UFLIA)"
     , format "(define-sort {} () Int)"       (Only elt)
@@ -447,7 +455,8 @@
   smt2 (Push)              = "(push 1)"
   smt2 (Pop)               = "(pop 1)"
   smt2 (CheckSat)          = "(check-sat)"
-  smt2 (GetValue xs)       = LT.unwords $ ["(get-value ("] ++ map smt2 xs ++ ["))"]
+  smt2 (GetValue xs)       = LT.unwords $ ["(get-value ("] ++ fmap smt2 xs ++ ["))"]
+
 
 smt2s = LT.intercalate " " . fmap smt2
 
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
@@ -55,7 +55,8 @@
   , fObj
 
   -- * Expressions and Predicates
-  , SymConst (..), Constant (..)
+  , SymConst (..)
+  , Constant (..) 
   , Bop (..), Brel (..)
   , Expr (..), Pred (..)
   , eVar
@@ -153,11 +154,12 @@
   , dummyLoc, dummyPos, dummyName, isDummy
   ) where
 
-import GHC.Generics         (Generic)
 import Debug.Trace          (trace)
 
+import GHC.Generics         (Generic)
 import Data.Typeable        (Typeable)
 import Data.Generics        (Data)
+
 import Data.Monoid hiding   ((<>))
 import Data.Functor
 import Data.Char            (ord, chr, isAlpha, isUpper, toLower)
@@ -290,8 +292,6 @@
 toFix_constant (c, so)
   = text "constant" <+> toFix c <+> text ":" <+> toFix so
 
-
-
 ----------------------------------------------------------------------
 ------------------------ Type Constructors ---------------------------
 ----------------------------------------------------------------------
@@ -305,7 +305,6 @@
 propFTyCon = TC $ dummyLoc propConName
 appFTyCon  = TC $ dummyLoc "FAppTy"
 
-
 isListTC (TC (Loc _ c)) = c == listConName
 isTupTC  (TC (Loc _ c)) = c == tupConName
 isFAppTyTC = (== appFTyCon)
@@ -337,6 +336,8 @@
 
 fObj :: LocSymbol -> Sort
 fObj = fTyconSort . TC
+
+ 
 ----------------------------------------------------------------------
 ------------------------------- Sorts --------------------------------
 ----------------------------------------------------------------------
@@ -379,9 +380,10 @@
 instance Fixpoint FTycon where
   toFix (TC s)       = toFix s
 
--------------------------------------------------------------------------------------------
+
+------------------------------------------------------------------------
 sortSubst                  :: (M.HashMap Symbol Sort) -> Sort -> Sort
--------------------------------------------------------------------------------------------
+------------------------------------------------------------------------
 sortSubst θ t@(FObj x)   = fromMaybe t (M.lookup x θ)
 sortSubst θ (FFunc n ts) = FFunc n (sortSubst θ <$> ts)
 sortSubst θ (FApp c ts)  = FApp c  (sortSubst θ <$> ts)
@@ -406,7 +408,9 @@
 data SymConst = SL !Text
               deriving (Eq, Ord, Show, Data, Typeable, Generic)
 
-data Constant = I  !Integer | R !Double
+data Constant = I !Integer
+              | R !Double
+              | L !Text !Sort 
               deriving (Eq, Ord, Show, Data, Typeable, Generic)
 
 data Brel = Eq | Ne | Gt | Ge | Lt | Le | Ueq | Une
@@ -434,9 +438,10 @@
   toFix = double
 
 instance Fixpoint Constant where
-  toFix (I i)  = toFix i
-  toFix (R i)  = toFix i
-
+  toFix (I i)   = toFix i
+  toFix (R i)   = toFix i
+  toFix (L s t) = parens $ text "lit" <+> toFix s <+> toFix t   
+                    
 instance Fixpoint SymConst where
   toFix  = toFix . encodeSymConst
 
@@ -597,6 +602,8 @@
 -- | Generalizing Symbol, Expression, Predicate into Classes -----------
 ------------------------------------------------------------------------
 
+-- | Values that can be viewed as Constants 
+
 -- | Values that can be viewed as Expressions
 
 class Expression a where
@@ -635,11 +642,11 @@
   prop True  = PTrue
   prop False = PFalse
 
-eVar          ::  Symbolic a => a -> Expr
-eVar          = EVar . symbol
+eVar ::  Symbolic a => a -> Expr
+eVar = EVar . symbol
 
-eProp         ::  Symbolic a => a -> Pred
-eProp         = mkProp . eVar
+eProp ::  Symbolic a => a -> Pred
+eProp = mkProp . eVar
 
 relReft :: (Expression a) => Brel -> a -> Reft
 relReft r e   = Reft (vv_, [RConc $ PAtom r (eVar vv_)  (expr e)])
@@ -649,11 +656,6 @@
 notExprReft   = relReft Ne
 uexprReft     = relReft Ueq
 
-
--- exprReft e             = Reft (vv_, [RConc $ PAtom Eq (eVar vv_)  (expr e)])
--- notExprReft e          = Reft (vv_, [RConc $ PAtom Ne (eVar vv_)  (expr e)])
--- exprReft e             = Reft (vv_, [RConc $ PAtom Eq (eVar vv_)  (expr e)])
-
 propReft      ::  (Predicate a) => a -> Reft
 propReft p    = Reft (vv_, [RConc $ PIff     (eProp vv_) (prop p)])
 
@@ -1134,9 +1136,10 @@
   rnf (BE x m) = rnf x `seq` rnf m
 
 instance NFData Constant where
-  rnf (I x) = rnf x
-  rnf (R x) = rnf x
-
+  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