diff --git a/heapster-saw/examples/arrays.saw b/heapster-saw/examples/arrays.saw
index 1a12837847..d81d40085b 100644
--- a/heapster-saw/examples/arrays.saw
+++ b/heapster-saw/examples/arrays.saw
@@ -1,28 +1,50 @@
 enable_experimental;
 env <- heapster_init_env_from_file "arrays.sawcore" "arrays.bc";
 
+// Integer types
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 heapster_define_perm env "int8" " " "llvmptr 8" "exists x:bv 8.eq(llvmword(x))";
 
 heapster_define_perm env "int64array" "len:bv 64" "llvmptr 64" "array(0,<len,*8,[(W,0) |-> int64<>])";
 
 
-heapster_typecheck_fun env "contains0_rec_" "(len:bv 64).arg0:eq(llvmword(len)), arg1:int64array<len>, arg2:int64<> -o arg0:true, arg1:int64array<len>, arg2:true, ret:int64<>";
+heapster_typecheck_fun env "contains0_rec_"
+  "(len:bv 64). arg0:eq(llvmword(len)), arg1:int64array<len>, arg2:int64<> -o \
+              \ arg0:true, arg1:int64array<len>, arg2:true, ret:int64<>";
 
 // the old way using a block entry hint
-// heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
-// heapster_block_entry_hint env "contains0" 9 "top0:bv 64, top1:llvmptr 64, top2:llvmptr 64" "frm:llvmframe 64, x0:llvmptr 64, x1:llvmptr 64" "top0:true, top1:array(0,<top0,*1,[(W,0) |-> int64<>]), top2:eq(llvmword(top0)), arg0:ptr((W,0) |-> true), arg1:ptr((W,0) |-> eq(x1)), arg2:ptr((W,0) |-> eq(x0)), arg3:ptr((W,0) |-> int64<>), frm:llvmframe [arg3:8, arg2:8, arg1:8, arg0:8], x0:eq(top2), x1:eq(top1)";
-// heapster_typecheck_fun env "contains0" "(len:bv 64).arg0:array(0,<len,*1,[(W,0) |-> int64<>]), arg1:eq(llvmword(len)) -o arg0:array(0,<len,*1,[(W,0) |-> int64<>]), arg1:true, ret:int64<>";
-
-heapster_typecheck_fun env "contains0" "(len:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)) -o arg0:int64array<len>, arg1:true, ret:int64<>";
-
-heapster_typecheck_fun env "zero_array" "(len:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)) -o arg0:int64array<len>, arg1:true, ret:true";
-
-heapster_typecheck_fun env "zero_array_from" "(len:bv 64, off:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)), arg2:eq(llvmword(off)) -o arg0:int64array<len>, arg1:true, ret:true";
+// heapster_block_entry_hint env "contains0" 9
+//   "top0:bv 64, top1:llvmptr 64, top2:llvmptr 64"
+//   "frm:llvmframe 64, x0:llvmptr 64, x1:llvmptr 64"
+//   "top0:true, top1:array(0,<top0,*1,[(W,0) |-> int64<>]),
+//   \ top2:eq(llvmword(top0)), arg0:ptr((W,0) |-> true), \
+//   \ arg1:ptr((W,0) |-> eq(x1)), arg2:ptr((W,0) |-> eq(x0)), arg3:ptr((W,0) |-> int64<>), \
+//   \ frm:llvmframe [arg3:8, arg2:8, arg1:8, arg0:8], x0:eq(top2), x1:eq(top1)";
+// heapster_typecheck_fun env "contains0"
+//   "(len:bv 64). arg0:array(0,<len,*1,[(W,0) |-> int64<>]), arg1:eq(llvmword(len)) -o \
+//               \ arg0:array(0,<len,*1,[(W,0) |-> int64<>]), arg1:true, ret:int64<>";
+
+heapster_typecheck_fun env "contains0"
+  "(len:bv 64). arg0:int64array<len>, arg1:eq(llvmword(len)) -o \
+              \ arg0:int64array<len>, arg1:true, ret:int64<>";
+
+heapster_typecheck_fun env "zero_array"
+  "(len:bv 64). arg0:int64array<len>, arg1:eq(llvmword(len)) -o \
+              \ arg0:int64array<len>, arg1:true, ret:true";
+
+heapster_typecheck_fun env "zero_array_from"
+  "(len:bv 64, off:bv 64). arg0:int64array<len>, arg1:eq(llvmword(len)), arg2:eq(llvmword(off)) -o \
+                         \ arg0:int64array<len>, arg1:true, arg2:true, ret:true";
 
 heapster_join_point_hint env "filter_and_sum_pos" [];
-heapster_typecheck_fun env "filter_and_sum_pos" "(len:bv 64).arg0:int64array<len>, arg1:eq(llvmword(len)) -o arg0:int64array<len>, arg1:true, ret:int64<>";
-
-heapster_typecheck_fun env "sum_2d" "(l1:bv 64,l2:bv 64).arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:eq(llvmword(l1)), arg2:eq(llvmword(l2)) -o arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> exists z:bv 64.eq(llvmword(z))])]), arg1:true, arg2:true, ret:int64<>";
+heapster_typecheck_fun env "filter_and_sum_pos"
+  "(len:bv 64). arg0:int64array<len>, arg1:eq(llvmword(len)) -o \
+              \ arg0:int64array<len>, arg1:true, ret:int64<>";
+
+heapster_typecheck_fun env "sum_2d"
+  "(l1:bv 64,l2:bv 64). arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> int64<>])]), \
+                      \ arg1:eq(llvmword(l1)), arg2:eq(llvmword(l2)) -o \
+                      \ arg0:array(0,<l1,*8,[(W,0) |-> array(0,<l2,*8,[(W,0) |-> int64<>])]), \
+                      \ arg1:true, arg2:true, ret:int64<>";
 
 heapster_export_coq env "arrays_gen.v";
diff --git a/heapster-saw/examples/clearbufs.saw b/heapster-saw/examples/clearbufs.saw
index b819426484..42ac69eeb0 100644
--- a/heapster-saw/examples/clearbufs.saw
+++ b/heapster-saw/examples/clearbufs.saw
@@ -4,10 +4,21 @@ env <- heapster_init_env_from_file "clearbufs.sawcore" "clearbufs.bc";
 // Integer types
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 
-heapster_define_reachability_perm env "Bufs" "x:llvmptr 64" "llvmptr 64" "exists len:(bv 64).ptr((W,0) |-> Bufs<x>) * ptr((W,8) |-> eq(llvmword(len))) * array(16, <len, *8, [(W,0) |-> int64<>])" "Mbox_def" "foldMbox" "unfoldMbox" "transMbox";
+heapster_define_reachability_perm env "Bufs"
+  "x:llvmptr 64" "llvmptr 64"
+  "exists len:(bv 64).ptr((W,0) |-> Bufs<x>) * \
+  \ ptr((W,8) |-> eq(llvmword(len))) * \
+  \ array(16, <len, *8, [(W,0) |-> int64<>])"
+  "Mbox_def" "foldMbox" "unfoldMbox" "transMbox";
 
-heapster_block_entry_hint env "clearbufs" 3 "top1:llvmptr 64" "frm:llvmframe 64,ghost:llvmptr 64" "top1:Bufs<ghost>, arg0:ptr((W,0) |-> eq(ghost)), ghost:Bufs<llvmword(0)>,frm:llvmframe [arg0:8]";
+heapster_block_entry_hint env "clearbufs" 3
+  "top1:llvmptr 64"
+  "frm:llvmframe 64,ghost:llvmptr 64"
+  "top1:Bufs<ghost>, \
+  \ arg0:ptr((W,0) |-> eq(ghost)), \
+  \ ghost:Bufs<llvmword(0)>,frm:llvmframe [arg0:8]";
 
-heapster_typecheck_fun env "clearbufs" "().arg0:Bufs<llvmword(0)> -o arg0:Bufs<llvmword(0)>";
+heapster_typecheck_fun env "clearbufs"
+  "(). arg0:Bufs<llvmword(0)> -o arg0:Bufs<llvmword(0)>";
 
 heapster_export_coq env "clearbufs_gen.v";
diff --git a/heapster-saw/examples/iso_recursive.saw b/heapster-saw/examples/iso_recursive.saw
index bd297051a9..e6b695ba95 100644
--- a/heapster-saw/examples/iso_recursive.saw
+++ b/heapster-saw/examples/iso_recursive.saw
@@ -1,10 +1,21 @@
 enable_experimental;
 env <- heapster_init_env_from_file "iso_recursive.sawcore" "iso_recursive.bc";
 
-heapster_define_irt_recursive_perm env "List" "X:perm(llvmptr 64), l:lifetime, rw:rwmodality" "llvmptr 64" ["eq(llvmword(0))","[l]ptr((rw,0) |-> X) * ptr((rw,8) |-> List<X,l,rw>)"];
+// Integer types
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 
-heapster_define_irt_recursive_shape env "ListS" 64 "X:llvmshape 64" "(fieldsh(eq(llvmword(0)))) orsh (fieldsh(eq(llvmword(1)));X;ListS<X>)";
+heapster_define_irt_recursive_perm env "List"
+  "X:perm(llvmptr 64), l:lifetime, rw:rwmodality"
+  "llvmptr 64"
+  [ "eq(llvmword(0))",
+    "[l]ptr((rw,0) |-> X) * ptr((rw,8) |-> List<X,l,rw>)" ];
 
-heapster_typecheck_fun env "is_elem" "(x:bv 64).arg0:eq(llvmword(x)), arg1:List<(exists y:(bv 64).eq(llvmword(y))),always,R> -o arg0:true, arg1:true, ret:exists z:(bv 64).eq(llvmword(z))";
+heapster_define_irt_recursive_shape env "ListS" 64
+  "X:llvmshape 64"
+  "fieldsh(eq(llvmword(0))) orsh (fieldsh(eq(llvmword(1))); X; ListS<X>)";
+
+heapster_typecheck_fun env "is_elem"
+  "(x:bv 64). arg0:eq(llvmword(x)), arg1:List<int64<>,always,R> -o \
+            \ arg0:true, arg1:true, ret:int64<>";
 
 heapster_export_coq env "iso_recursive_gen.v";
diff --git a/heapster-saw/examples/iter_linked_list.saw b/heapster-saw/examples/iter_linked_list.saw
index d36cfcf08b..6f7e0363e8 100644
--- a/heapster-saw/examples/iter_linked_list.saw
+++ b/heapster-saw/examples/iter_linked_list.saw
@@ -4,18 +4,45 @@ env <- heapster_init_env_from_file "iter_linked_list.sawcore" "iter_linked_list.
 // Integer types
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 
-heapster_define_reachability_perm env "ListF" "X:perm(llvmptr 64), l:lifetime, rw:rwmodality, y:llvmptr 64" "llvmptr 64" "[l]ptr((rw,0) |-> X) * [l]ptr((rw,8) |-> ListF<X,l,rw,y>)" "List_def" "foldList" "unfoldList" "appendList";
-
-heapster_block_entry_hint env "is_elem" 3 "top_ptr:llvmptr 64, top_ptr1:llvmptr 64" "ghost_frm:llvmframe 64, ghost_ptr:llvmptr 64" "top_ptr:int64<>, top_ptr1:true, arg0:ptr((W,0) |-> true), arg1:ptr((W,0) |-> eq(top_ptr)), arg2:ptr((W,0) |-> eq(ghost_ptr)), ghost_ptr:ListF<int64<>,always,R,llvmword(0)>, ghost_frm:llvmframe [arg2:8, arg1:8, arg0:8]";
-
-heapster_typecheck_fun env "is_elem" "().arg0:int64<>, arg1:ListF<int64<>,always,R,llvmword(0)> -o arg0:true, arg1:true, ret:int64<>";
-
-heapster_block_entry_hint env "incr_list" 3 "top1:llvmptr 64" "frm:llvmframe 64,ghost:llvmptr 64" "top1:ListF<(exists y:(bv 64).eq(llvmword(y))),always,W,ghost>, arg0:ptr((W,0) |-> eq(ghost)),ghost:ListF<(exists y:(bv 64).eq(llvmword(y))),always,W,llvmword(0)>,frm:llvmframe [arg0:8]";
-
-heapster_typecheck_fun env "incr_list" "().arg0:ListF<(exists y:(bv 64).eq(llvmword(y))),always,W,llvmword(0)> -o arg0:ListF<(exists y:(bv 64).eq(llvmword(y))),always,W,llvmword(0)>, ret:true";
-
-heapster_block_entry_hint env "length" 3 "top1:llvmptr 64" "frm:llvmframe 64,ghost:llvmptr 64" "top1:ListF<(int64<>),always,W,ghost>, arg0:ptr((W,0) |-> eq(ghost)),ghost:ListF<(int64<>),always,W,llvmword(0)>,arg1:ptr((W,0) |-> int64<>),frm:llvmframe [arg1:8,arg0:8]";
-
-heapster_typecheck_fun env "length" "().arg0:ListF<int64<>,always,W,llvmword(0)> -o arg0:true, ret:int64<>";
+heapster_define_reachability_perm env "ListF"
+  "X:perm(llvmptr 64), l:lifetime, rw:rwmodality, y:llvmptr 64"
+  "llvmptr 64"
+  "[l]ptr((rw,0) |-> X) * [l]ptr((rw,8) |-> ListF<X,l,rw,y>)"
+  "List_def" "foldList" "unfoldList" "appendList";
+
+heapster_block_entry_hint env "is_elem" 3
+  "top_ptr:llvmptr 64, top_ptr1:llvmptr 64"
+  "ghost_frm:llvmframe 64, ghost_ptr:llvmptr 64"
+  "top_ptr:int64<>, top_ptr1:true, \
+  \ arg0:ptr((W,0) |-> true), arg1:ptr((W,0) |-> eq(top_ptr)), \
+  \ arg2:ptr((W,0) |-> eq(ghost_ptr)), \
+  \ ghost_ptr:ListF<int64<>,always,R,llvmword(0)>, \
+  \ ghost_frm:llvmframe [arg2:8, arg1:8, arg0:8]";
+
+heapster_typecheck_fun env "is_elem"
+  "(). arg0:int64<>, arg1:ListF<int64<>,always,R,llvmword(0)> -o \
+     \ arg0:true, arg1:true, ret:int64<>";
+
+heapster_block_entry_hint env "incr_list" 3
+  "top1:llvmptr 64"
+  "frm:llvmframe 64,ghost:llvmptr 64"
+  "top1:ListF<int64<>,always,W,ghost>, \
+  \ arg0:ptr((W,0) |-> eq(ghost)), \
+  \ ghost:ListF<int64<>,always,W,llvmword(0)>, frm:llvmframe [arg0:8]";
+
+heapster_typecheck_fun env "incr_list"
+  "(). arg0:ListF<int64<>,always,W,llvmword(0)> -o \
+     \ arg0:ListF<int64<>,always,W,llvmword(0)>, ret:true";
+
+heapster_block_entry_hint env "length" 3
+  "top1:llvmptr 64"
+  "frm:llvmframe 64, ghost:llvmptr 64"
+  "top1:ListF<int64<>,always,W,ghost>, \
+  \ arg0:ptr((W,0) |-> eq(ghost)), arg1:ptr((W,0) |-> int64<>), \
+  \ ghost:ListF<int64<>,always,W,llvmword(0)>, frm:llvmframe [arg1:8,arg0:8]";
+
+heapster_typecheck_fun env "length"
+  "(). arg0:ListF<int64<>,always,W,llvmword(0)> -o \
+     \ arg0:true, ret:int64<>";
 
 heapster_export_coq env "iter_linked_list_gen.v";
diff --git a/heapster-saw/examples/linked_list.saw b/heapster-saw/examples/linked_list.saw
index 24460e8247..3ab875f062 100644
--- a/heapster-saw/examples/linked_list.saw
+++ b/heapster-saw/examples/linked_list.saw
@@ -1,19 +1,41 @@
-// This script expects to be run from the saw-script root directory
 enable_experimental;
 env <- heapster_init_env_from_file "linked_list.sawcore" "linked_list.bc";
 
-heapster_define_recursive_perm env "List" "X:perm(llvmptr 64), l:lifetime, rw:rwmodality" "llvmptr 64" ["eq(llvmword(0))","[l]ptr((rw,0) |-> X) * [l]ptr((rw,8) |-> List<X,l,rw>)"] "List_def" "foldList" "unfoldList";
-
-heapster_typecheck_fun env "is_elem" "(x:bv 64).arg0:eq(llvmword(x)), arg1:List<(exists y:(bv 64).eq(llvmword(y))),always,R> -o arg0:true, arg1:true, ret:exists z:(bv 64).eq(llvmword(z))";
-
-heapster_assume_fun env "malloc" "(sz:bv 64).arg0:eq(llvmword(8*sz)) -o arg0:true, ret:array(0,<sz,*8,[(W,0) |-> true])" "mallocSpec";
-
-heapster_typecheck_fun env "any" "().arg0:llvmfunptr{1,64}(().arg0:(exists x:(bv 64).eq(llvmword(x))) -o arg0:true, ret:(exists x:(bv 64).eq(llvmword(x)))), arg1:List<(exists x:(bv 64).eq(llvmword(x))),always,R> -o arg0:true, arg1:true, ret:exists x:(bv 64).eq(llvmword(x))";
-
-heapster_typecheck_fun env "find_elem" "().arg0:exists x:(bv 64).eq(llvmword(x)), arg1:List<(exists y:(bv 64).eq(llvmword(y))),always,W> -o arg0:true, arg1:true, ret:List<(exists x:(bv 64).eq(llvmword(x))),always,W>";
-
-heapster_typecheck_fun env "sorted_insert" "(x:bv 64).arg0:eq(llvmword(x)), arg1:List<(exists y:(bv 64).eq(llvmword(y))),always,W> -o arg0:true, arg1:true, ret:List<(exists y:(bv 64).eq(llvmword(y))),always,W>";
-
-heapster_typecheck_fun env "sorted_insert_no_malloc" "(x:bv 64).arg0:ptr((W,0) |-> eq(llvmword(x))) * ptr((W,8) |-> eq(llvmword(0))), arg1:List<(exists y:(bv 64).eq(llvmword(y))),always,W> -o arg0:true, arg1:true, ret:List<(exists y:(bv 64).eq(llvmword(y))),always,W>";
+// Integer types
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
+
+heapster_define_recursive_perm env "List"
+  "X:perm(llvmptr 64), l:lifetime, rw:rwmodality"
+  "llvmptr 64"
+  [ "eq(llvmword(0))",
+    "[l]ptr((rw,0) |-> X) * [l]ptr((rw,8) |-> List<X,l,rw>)" ]
+  "List_def" "foldList" "unfoldList";
+
+heapster_typecheck_fun env "is_elem"
+  "(). arg0:int64<>, arg1:List<int64<>,always,R> -o \
+     \ arg0:true, arg1:true, ret:int64<>";
+
+heapster_assume_fun env "malloc"
+  "(sz:bv 64). arg0:eq(llvmword(8*sz)) -o \
+             \ arg0:true, ret:array(0,<sz,*8,[(W,0) |-> true])"
+  "mallocSpec";
+
+heapster_typecheck_fun env "any"
+  "(). arg0:llvmfunptr{1,64}((). arg0:int64<> -o arg0:true, ret:int64<>), \
+     \ arg1:List<int64<>,always,R> -o \
+     \ arg0:true, arg1:true, ret:int64<>";
+
+heapster_typecheck_fun env "find_elem"
+  "(). arg0:int64<>, arg1:List<int64<>,always,W> -o \
+     \ arg0:true, arg1:true, ret:List<int64<>,always,W>";
+
+heapster_typecheck_fun env "sorted_insert"
+  "(). arg0:int64<>, arg1:List<int64<>,always,W> -o \
+     \ arg0:true, arg1:true, ret:List<int64<>,always,W>";
+
+heapster_typecheck_fun env "sorted_insert_no_malloc"
+  "(). arg0:ptr((W,0) |-> int64<>) * ptr((W,8) |-> eq(llvmword(0))), \
+     \ arg1:List<int64<>,always,W> -o \
+     \ arg0:true, arg1:true, ret:List<int64<>,always,W>";
 
 heapster_export_coq env "linked_list_gen.v";
diff --git a/heapster-saw/examples/loops.saw b/heapster-saw/examples/loops.saw
index 286d3ef3b2..835ca507b3 100644
--- a/heapster-saw/examples/loops.saw
+++ b/heapster-saw/examples/loops.saw
@@ -1,14 +1,24 @@
 enable_experimental;
 env <- heapster_init_env_from_file "loops.sawcore" "loops.bc";
 
+// Integer types
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 
-heapster_block_entry_hint env "add_loop" 3 "top0:llvmptr 64,top1:llvmptr 64" "frm:llvmframe 64,x0:llvmptr 64,x1:llvmptr 64" "top0:int64<>,top1:int64<>,arg0:ptr((W,0) |-> int64<>),arg1:ptr((W,0) |-> int64<>),frm:llvmframe [arg1:8,arg0:8,x1:8,x0:8],x0:ptr((W,0) |-> true),x1:ptr((W,0) |-> true)";
+heapster_block_entry_hint env "add_loop" 3
+  "top0:llvmptr 64, top1:llvmptr 64"
+  "frm:llvmframe 64, x0:llvmptr 64, x1:llvmptr 64"
+  "top0:int64<>, top1:int64<>, \
+  \ arg0:ptr((W,0) |-> int64<>), arg1:ptr((W,0) |-> int64<>), \
+  \ frm:llvmframe [arg1:8,arg0:8,x1:8,x0:8], \
+  \ x0:ptr((W,0) |-> true), x1:ptr((W,0) |-> true)";
 
-heapster_typecheck_fun env "add_loop" "().arg0:int64<>, arg1:int64<> -o ret:int64<>";
+heapster_typecheck_fun env "add_loop"
+  "(). arg0:int64<>, arg1:int64<> -o ret:int64<>";
 
-heapster_typecheck_fun env "sign_of_sum" "().arg0:int64<>, arg1:int64<> -o ret:int64<>";
+heapster_typecheck_fun env "sign_of_sum"
+  "(). arg0:int64<>, arg1:int64<> -o ret:int64<>";
 
-heapster_typecheck_fun env "compare_sum" "().arg0:int64<>, arg1:int64<>, arg2:int64<> -o ret:int64<>";
+heapster_typecheck_fun env "compare_sum"
+  "(). arg0:int64<>, arg1:int64<>, arg2:int64<> -o ret:int64<>";
 
 heapster_export_coq env "loops_gen.v";
diff --git a/heapster-saw/examples/mbox.saw b/heapster-saw/examples/mbox.saw
index 19844ce74b..44dc67fa86 100644
--- a/heapster-saw/examples/mbox.saw
+++ b/heapster-saw/examples/mbox.saw
@@ -22,13 +22,29 @@ heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x)
 
 heapster_define_perm env "state_t" " " "llvmptr 64" "array(0, <16, *1, [(W,0) |-> int64<>])";
 
-heapster_define_perm env "aes_sw_ctx" "rw1:rwmodality, rw2:rwmodality" "llvmptr 64" "array(0, <240, *1, [(rw1,0) |-> int64<>]) * ptr((rw2, 1920) |-> int64<>)";
-
-heapster_define_reachability_perm env "mbox" "rw:rwmodality, x:llvmptr 64" "llvmptr 64" "ptr((rw,0) |-> int64<>) * ptr((rw,8) |-> int64<>) * ptr((rw,16) |-> mbox<rw,x>) * array(24, <128, *1, [(rw,0,8) |-> int8<>])" "Mbox_def" "foldMbox" "unfoldMbox" "transMbox";
-
-// heapster_define_perm env "mbox_nonnull" "rw:rwmodality, p:perm (llvmptr 64)" "llvmptr 64" "ptr((rw,0) |-> int64<>) * ptr((rw,8) |-> int64<>) * ptr((rw,16) |-> int64<>) * ptr((rw,24) |-> mbox<rw, p>) * array(32, <128, *1, [(rw,0,8) |-> int8<>])";
-
-heapster_define_perm env "byte_array" "rw:rwmodality, len:bv 64" "llvmptr 64" "array(0, <len, *1, [(rw,0,8) |-> int8<>])";
+heapster_define_perm env "aes_sw_ctx"
+  "rw1:rwmodality, rw2:rwmodality"
+  "llvmptr 64"
+  "array(0, <240, *1, [(rw1,0) |-> int64<>]) * ptr((rw2, 1920) |-> int64<>)";
+
+heapster_define_reachability_perm env "mbox"
+  "rw:rwmodality, x:llvmptr 64"
+  "llvmptr 64"
+  "ptr((rw,0) |-> int64<>) * ptr((rw,8) |-> int64<>) * ptr((rw,16) |-> mbox<rw,x>) * \
+  \ array(24, <128, *1, [(rw,0,8) |-> int8<>])"
+  "Mbox_def" "foldMbox" "unfoldMbox" "transMbox";
+
+// heapster_define_perm env "mbox_nonnull"
+//   "rw:rwmodality, p:perm (llvmptr 64)"
+//   "llvmptr 64"
+//   "ptr((rw,0) |-> int64<>) * ptr((rw,8) |-> int64<>) * \
+//   \ ptr((rw,16) |-> int64<>) * ptr((rw,24) |-> mbox<rw, p>) * \
+//   \ array(32, <128, *1, [(rw,0,8) |-> int8<>])";
+
+heapster_define_perm env "byte_array"
+  "rw:rwmodality, len:bv 64"
+  "llvmptr 64"
+  "array(0, <len, *1, [(rw,0,8) |-> int8<>])";
 
 heapster_define_perm env "boolean" " " "llvmptr 1" "exists x:bv 1.eq(llvmword(x))";
 
@@ -37,13 +53,27 @@ heapster_define_perm env "boolean" " " "llvmptr 1" "exists x:bv 1.eq(llvmword(x)
 // LLVM intrinsics
 
 // memcpy i64
-// heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" "(X:perm(llvmptr 64), Y:perm(llvmptr 64)).arg0:(exists x:bv 1.X), arg1:(exists x:bv 1.Y), arg2:true, arg3:true -o arg0:(exists x:bv 1.Y), arg1:(exists x:bv 1.Y)" "\\ (X:sort 0) (Y:sort 0) (_:SigBV1 X) (y:SigBV1 Y) -> returnM (SigBV1 Y * (SigBV1 Y * #())) (y, (y, ()))";
-
-// heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" "(len:bv 64).arg0:byte_array<W,len>, arg1:byte_array<W,len>, arg2:eq(llvmword(len)), arg3:true -o arg0:byte_array<W,len>, arg1:byte_array<W,len>" "\\ (len:Vec 64 Bool) (x y:BVVec 64 len (Vec 8 Bool)) -> returnM (BVVec 64 len (Vec 8 Bool) * (BVVec 64 len (Vec 8 Bool) * #())) (y, (y, ()))";
+// heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64"
+//   "(X:perm(llvmptr 64), Y:perm(llvmptr 64)). \
+//   \ arg0:(exists x:bv 1.X), arg1:(exists x:bv 1.Y), arg2:true, arg3:true -o \
+//   \ arg0:(exists x:bv 1.Y), arg1:(exists x:bv 1.Y)"
+//   "\\ (X:sort 0) (Y:sort 0) (_:SigBV1 X) (y:SigBV1 Y) -> \
+//     \ returnM (SigBV1 Y * (SigBV1 Y * #())) (y, (y, ()))";
+
+// heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64"
+//   "(len:bv 64). arg0:byte_array<W,len>, arg1:byte_array<W,len>, \
+//               \ arg2:eq(llvmword(len)), arg3:true -o \
+//               \ arg0:byte_array<W,len>, arg1:byte_array<W,len>"
+//   "\\ (len:Vec 64 Bool) (x y:BVVec 64 len (Vec 8 Bool)) -> \
+//     \ returnM (BVVec 64 len (Vec 8 Bool) * (BVVec 64 len (Vec 8 Bool) * #())) (y, (y, ()))";
 
 heapster_assume_fun env "llvm.objectsize.i64.p0i8" "().empty -o empty" "returnM #() ()";
 
-heapster_assume_fun env "__memcpy_chk" "(len:bv 64).arg0:byte_array<W,len>,arg1:byte_array<W,len>,arg2:eq(llvmword (len)) -o arg0:byte_array<W,len>,arg1:byte_array<W,len>" "\\ (len:Vec 64 Bool) (_ src : BVVec 64 len (Vec 8 Bool)) -> returnM (BVVec 64 len (Vec 8 Bool) * BVVec 64 len (Vec 8 Bool)) (src, src)";
+heapster_assume_fun env "__memcpy_chk"
+  "(len:bv 64). arg0:byte_array<W,len>, arg1:byte_array<W,len>, arg2:eq(llvmword (len)) -o \
+              \ arg0:byte_array<W,len>, arg1:byte_array<W,len>"
+  "\\ (len:Vec 64 Bool) (_ src : BVVec 64 len (Vec 8 Bool)) -> \
+    \ returnM (BVVec 64 len (Vec 8 Bool) * BVVec 64 len (Vec 8 Bool)) (src, src)";
 
 
 //------------------------------------------------------------------------------
@@ -56,83 +86,191 @@ heapster_assume_fun env "rand" "().empty -o ret:int32<>" "randSpec";
 // mbox.c
 
 
-heapster_assume_fun env "mbox_all_freed" "().empty -o ret:boolean<>" "mboxAllFreedSpec";
-
-
-heapster_assume_fun env "mbox_new" "().empty -o ret:mbox<W,llvmword(0)>" "mboxNewSpec";
-
+heapster_assume_fun env "mbox_all_freed"
+  "(). empty -o ret:boolean<>"
+  "mboxAllFreedSpec";
+
 
-heapster_assume_fun env "mbox_free" "().arg0:ptr((W,0) |-> true) * ptr((W,8) |-> true) * ptr((W,16) |-> true) * array(24, <128, *1, [(W,0,8) |-> int8<>]) -o arg0:true, ret:int32<>" "mboxFreeSpec";
+heapster_assume_fun env "mbox_new"
+  "(). empty -o ret:mbox<W,llvmword(0)>"
+  "mboxNewSpec";
 
 
-heapster_block_entry_hint env "mbox_free_chain" 3 "top1:llvmptr 64" "frm:llvmframe 64" "top1:true, arg0:ptr((W,0,32) |-> true), arg1:ptr((W,0) |-> mbox<W,llvmword(0)>), arg2:ptr((W,0) |-> true), arg3:ptr((W,0,32) |-> true),frm:llvmframe [arg3:4,arg2:8,arg1:8,arg0:4]";
+heapster_assume_fun env "mbox_free"
+  "(). arg0:ptr((W,0) |-> true) * ptr((W,8) |-> true) * ptr((W,16) |-> true) * \
+     \      array(24, <128, *1, [(W,0,8) |-> int8<>]) -o \
+     \ arg0:true, ret:int32<>"
+  "mboxFreeSpec";
+
+
+heapster_block_entry_hint env "mbox_free_chain" 3
+  "top1:llvmptr 64"
+  "frm:llvmframe 64"
+  "top1:true, \
+  \ arg0:ptr((W,0,32) |-> true), arg1:ptr((W,0) |-> mbox<W,llvmword(0)>), \
+  \ arg2:ptr((W,0) |-> true), arg3:ptr((W,0,32) |-> true), \
+  \ frm:llvmframe [arg3:4,arg2:8,arg1:8,arg0:4]";
 
-heapster_typecheck_fun env "mbox_free_chain" "().arg0:mbox<W,llvmword(0)> -o arg0:true, ret:int32<>";
+heapster_typecheck_fun env "mbox_free_chain"
+  "(). arg0:mbox<W,llvmword(0)> -o arg0:true, ret:int32<>";
 
 
-heapster_block_entry_hint env "mbox_eq" 29 "top1:llvmptr 64, top2:llvmptr 64" "frm:llvmframe 64, x0:llvmptr 64, x1:llvmptr 64" "top1:mbox<W,x0>, top2:mbox<W,x1>, arg0:ptr((W,0,32) |-> true), arg1:ptr((W,0) |-> eq(x0)), arg2:ptr((W,0) |-> eq(x1)), arg3:ptr((W,0) |-> int64<>), arg4:ptr((W,0) |-> int64<>), frm:llvmframe [arg4:8, arg3:8, arg2:8, arg1:8, arg0:4], x0:mbox<W,llvmword(0)>, x1:mbox<W,llvmword(0)>";
+heapster_block_entry_hint env "mbox_eq" 29
+  "top1:llvmptr 64, top2:llvmptr 64"
+  "frm:llvmframe 64, x0:llvmptr 64, x1:llvmptr 64"
+  "top1:mbox<W,x0>, top2:mbox<W,x1>, \
+  \ arg0:ptr((W,0,32) |-> true), arg1:ptr((W,0) |-> eq(x0)), \
+  \ arg2:ptr((W,0) |-> eq(x1)), arg3:ptr((W,0) |-> int64<>), arg4:ptr((W,0) |-> int64<>), \
+  \ frm:llvmframe [arg4:8, arg3:8, arg2:8, arg1:8, arg0:4], \
+  \ x0:mbox<W,llvmword(0)>, x1:mbox<W,llvmword(0)>";
 
-heapster_typecheck_fun env "mbox_eq" "().arg0:mbox<W,llvmword(0)>, arg1:mbox<W,llvmword(0)> -o arg0:mbox<W,llvmword(0)>, arg1:mbox<W,llvmword(0)>, ret:int32<>";
+heapster_typecheck_fun env "mbox_eq"
+  "(). arg0:mbox<W,llvmword(0)>, arg1:mbox<W,llvmword(0)> -o \
+     \ arg0:mbox<W,llvmword(0)>, arg1:mbox<W,llvmword(0)>, ret:int32<>";
 
 
-heapster_block_entry_hint env "mbox_from_buffer" 24 "top1:bv 64, top2:llvmptr 64, top3:llvmptr 64" "frm:llvmframe 64, ghost0:llvmptr 64, ghost1:bv 64" "top1:true, top2:array(0, <top1, *1, [(W,0,8) |-> int8<>]), top3:eq(llvmword(top1)), arg0:ptr((W,0) |-> true), arg1:ptr((W,0) |-> eq(top2)), arg2:ptr((W,0) |-> eq(llvmword(top1))), arg3:ptr((W,0) |-> mbox<W, ghost0>), arg4:ptr((W,0) |-> eq(ghost0)), arg5:ptr((W,0) |-> eq(llvmword(ghost1))), arg6:ptr((W,0) |-> true), frm:llvmframe [arg6:8, arg5:8, arg4:8, arg3:8, arg2:8, arg1:8, arg0:8], ghost0:ptr((W,0) |-> int64<>) * ptr((W,8) |-> int64<>) * ptr((W,16) |-> mbox<W, llvmword(0)>) * array(24, <128, *1, [(W,0,8) |-> int8<>]), ghost1:true";
+heapster_block_entry_hint env "mbox_from_buffer" 24
+  "top1:bv 64, top2:llvmptr 64, top3:llvmptr 64"
+  "frm:llvmframe 64, ghost0:llvmptr 64, ghost1:bv 64"
+  "top1:true, top2:array(0, <top1, *1, [(W,0,8) |-> int8<>]), \
+  \ top3:eq(llvmword(top1)), arg0:ptr((W,0) |-> true), \
+  \ arg1:ptr((W,0) |-> eq(top2)), arg2:ptr((W,0) |-> eq(llvmword(top1))), \
+  \ arg3:ptr((W,0) |-> mbox<W, ghost0>), arg4:ptr((W,0) |-> eq(ghost0)), \
+  \ arg5:ptr((W,0) |-> eq(llvmword(ghost1))), arg6:ptr((W,0) |-> true), \
+  \ frm:llvmframe [arg6:8, arg5:8, arg4:8, arg3:8, arg2:8, arg1:8, arg0:8], \
+  \ ghost0:ptr((W,0) |-> int64<>) * ptr((W,8) |-> int64<>) * \
+  \        ptr((W,16) |-> mbox<W, llvmword(0)>) * array(24, <128, *1, [(W,0,8) |-> int8<>]), \
+  \ ghost1:true";
 
-heapster_typecheck_fun env "mbox_from_buffer" "(len:bv 64).arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:eq(llvmword(len)) -o arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:true, ret:mbox<W,llvmword(0)>";
+heapster_typecheck_fun env "mbox_from_buffer"
+  "(len:bv 64). arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:eq(llvmword(len)) -o \
+              \ arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:true, ret:mbox<W,llvmword(0)>";
 
 
-heapster_block_entry_hint env "mbox_to_buffer" 32 "top1:bv 64, top2:llvmptr 64, top3:llvmptr 64, top4:llvmptr 64, top5:llvmptr 64" "frm:llvmframe 64, ghost0:llvmptr 64" "top1:true, top2:array(0, <top1, *1, [(W,0,8) |-> int8<>]), top3:eq(llvmword(top1)), top4:mbox<W,ghost0>, top5:int64<>, arg0:ptr((W,0) |-> true), arg1:ptr((W,0) |-> eq(top2)), arg2:ptr((W,0) |-> eq(top3)), arg3:ptr((W,0) |-> eq(ghost0)), arg4:ptr((W,0) |-> int64<>), arg5:ptr((W,0) |-> int64<>), arg6:ptr((W,0) |-> true), frm:llvmframe [arg6:8, arg5:8, arg4:8, arg3:8, arg2:8, arg1:8, arg0:8], ghost0:mbox<W,llvmword(0)>";
+heapster_block_entry_hint env "mbox_to_buffer" 32
+  "top1:bv 64, top2:llvmptr 64, top3:llvmptr 64, top4:llvmptr 64, top5:llvmptr 64"
+  "frm:llvmframe 64, ghost0:llvmptr 64"
+  "top1:true, top2:array(0, <top1, *1, [(W,0,8) |-> int8<>]), \
+  \ top3:eq(llvmword(top1)), top4:mbox<W,ghost0>, \
+  \ top5:int64<>, arg0:ptr((W,0) |-> true), \
+  \ arg1:ptr((W,0) |-> eq(top2)), arg2:ptr((W,0) |-> eq(top3)), \
+  \ arg3:ptr((W,0) |-> eq(ghost0)), arg4:ptr((W,0) |-> int64<>), \
+  \ arg5:ptr((W,0) |-> int64<>), arg6:ptr((W,0) |-> true), \
+  \ frm:llvmframe [arg6:8, arg5:8, arg4:8, arg3:8, arg2:8, arg1:8, arg0:8], \
+  \ ghost0:mbox<W,llvmword(0)>";
 
-heapster_typecheck_fun env "mbox_to_buffer" "(len:bv 64).arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:eq(llvmword(len)), arg2:mbox<W, llvmword(0)>, arg3:int64<> -o arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:true, arg2:mbox<W,llvmword(0)>, arg3:true, ret:int64<>";
+heapster_typecheck_fun env "mbox_to_buffer"
+  "(len:bv 64). arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), \
+              \ arg1:eq(llvmword(len)), arg2:mbox<W, llvmword(0)>, arg3:int64<> -o \
+              \ arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), \
+              \ arg1:true, arg2:mbox<W,llvmword(0)>, arg3:true, ret:int64<>";
 
 
-heapster_typecheck_fun env "mbox_to_buffer_rec" "(len:bv 64).arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:eq(llvmword(len)), arg2:mbox<W,llvmword(0)> -o arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), arg1:true, arg2:mbox<W,llvmword(0)>, ret:true";
+heapster_typecheck_fun env "mbox_to_buffer_rec"
+  "(len:bv 64). arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), \
+              \ arg1:eq(llvmword(len)), arg2:mbox<W,llvmword(0)> -o \
+              \ arg0:array(0,<len,*1,[(W,0,8) |-> int8<>]), \
+              \ arg1:true, arg2:mbox<W,llvmword(0)>, ret:true";
 
-// heapster_typecheck_fun env "mbox_to_buffer_rec" "(len:bv 64).arg0:byte_array<W,len>, arg1:eq(llvmword(len)), arg2:mbox<W>, arg3:int64<> -o arg0:byte_array<W,len>, arg1:true, arg2:mbox<W>, arg3:true, ret:int64<>";
+// heapster_typecheck_fun env "mbox_to_buffer_rec"
+//   "(len:bv 64). arg0:byte_array<W,len>, arg1:eq(llvmword(len)), \
+//               \ arg2:mbox<W>, arg3:int64<> -o \
+//               \ arg0:byte_array<W,len>, arg1:true, \
+//               \ arg2:mbox<W>, arg3:true, ret:int64<>";
 
 
-heapster_block_entry_hint env "mbox_len" 3 "top1:llvmptr 64" "frm:llvmframe 64, ghost:llvmptr 64" "top1:mbox<W,ghost>, arg0:ptr((W,0) |-> eq(ghost)), arg1:ptr((W,0) |-> int64<>), frm:llvmframe [arg1:8, arg0:8], ghost:mbox<W,llvmword(0)>";
+heapster_block_entry_hint env "mbox_len" 3
+  "top1:llvmptr 64"
+  "frm:llvmframe 64, ghost:llvmptr 64"
+  "top1:mbox<W,ghost>, \
+  \ arg0:ptr((W,0) |-> eq(ghost)), arg1:ptr((W,0) |-> int64<>), \
+  \ frm:llvmframe [arg1:8, arg0:8], \
+  \ ghost:mbox<W,llvmword(0)>";
 
-heapster_typecheck_fun env "mbox_len" "().arg0:mbox<W,llvmword(0)> -o arg0:mbox<W,llvmword(0)>, ret:int64<>";
+heapster_typecheck_fun env "mbox_len"
+  "(). arg0:mbox<W,llvmword(0)> -o arg0:mbox<W,llvmword(0)>, ret:int64<>";
 
 
-heapster_typecheck_fun env "mbox_concat" "().arg0:mbox<W,llvmword(0)>, arg1:mbox<W,llvmword(0)> -o arg0:mbox<W,llvmword(0)>, arg1:true";
+heapster_typecheck_fun env "mbox_concat"
+  "(). arg0:mbox<W,llvmword(0)>, arg1:mbox<W,llvmword(0)> -o \
+     \ arg0:mbox<W,llvmword(0)>, arg1:true";
 
 
-heapster_block_entry_hint env "mbox_concat_chains" 16 "top1:llvmptr 64, top2:llvmptr 64" "frm:llvmframe 64, x0:llvmptr 64" "top1:mbox<W,x0>, top2:mbox<W,llvmword(0)>, arg0:ptr((W,0) |-> eq(x0)), arg1:ptr((W,0) |-> eq(top2)), frm:llvmframe [arg1:8, arg0:8], x0:ptr((W,0) |-> int64<>) * ptr((W,8) |-> int64<>) * ptr((W,16) |-> mbox<W,llvmword(0)>) * array(24, <128, *1, [(W,0,8) |-> int8<>])";
+heapster_block_entry_hint env "mbox_concat_chains" 16
+  "top1:llvmptr 64, top2:llvmptr 64"
+  "frm:llvmframe 64, x0:llvmptr 64"
+  "top1:mbox<W,x0>, top2:mbox<W,llvmword(0)>, \
+  \ arg0:ptr((W,0) |-> eq(x0)), arg1:ptr((W,0) |-> eq(top2)), \
+  \ frm:llvmframe [arg1:8, arg0:8], \
+  \ x0:ptr((W,0) |-> int64<>) * ptr((W,8) |-> int64<>) * \
+  \    ptr((W,16) |-> mbox<W,llvmword(0)>) * array(24, <128, *1, [(W,0,8) |-> int8<>])";
 
-heapster_typecheck_fun env "mbox_concat_chains" "().arg0:mbox<W,llvmword(0)>, arg1:mbox<W,llvmword(0)> -o arg0:mbox<W,llvmword(0)>";
+heapster_typecheck_fun env "mbox_concat_chains"
+  "(). arg0:mbox<W,llvmword(0)>, arg1:mbox<W,llvmword(0)> -o \
+     \ arg0:mbox<W,llvmword(0)>";
 
 
-heapster_typecheck_fun env "mbox_split_at" "().arg0:ptr((W,0) |-> mbox<W,llvmword(0)>), arg1:int64<> -o arg0:ptr((W,0) |-> mbox<W,llvmword(0)>), arg1:true, ret:mbox<W,llvmword(0)>";
+heapster_typecheck_fun env "mbox_split_at"
+  "(). arg0:ptr((W,0) |-> mbox<W,llvmword(0)>), arg1:int64<> -o \
+     \ arg0:ptr((W,0) |-> mbox<W,llvmword(0)>), arg1:true, ret:mbox<W,llvmword(0)>";
 
 
-heapster_typecheck_fun env "mbox_copy" "().arg0:mbox<W,llvmword(0)> -o arg0:mbox<W,llvmword(0)>, ret:mbox<W,llvmword(0)>";
+heapster_typecheck_fun env "mbox_copy"
+  "(). arg0:mbox<W,llvmword(0)> -o \
+     \ arg0:mbox<W,llvmword(0)>, ret:mbox<W,llvmword(0)>";
 
-// heapster_typecheck_fun env "mbox_copy" "().arg0:mbox_nonnull<W,mbox<W>> -o arg0:true, ret:mbox<W>";
+// heapster_typecheck_fun env "mbox_copy"
+//   "(). arg0:mbox_nonnull<W,mbox<W>> -o arg0:true, ret:mbox<W>";
 
 
-// heapster_block_entry_hint env "mbox_copy_chain" 51 "top1:llvmptr 64,top2:llvmptr 64" "frm:llvmframe 64" "top1:true, top2:true, arg0:ptr((W,0) |-> eq(llvmword(true))), arg1:ptr((W,0) |-> eq(top2)), frm:llvmframe [arg1:8,arg0:8], x0:mbox<W>";
+// heapster_block_entry_hint env "mbox_copy_chain" 51
+//   "top1:llvmptr 64, top2:llvmptr 64"
+//   "frm:llvmframe 64"
+//   "top1:true, top2:true, \
+//   \ arg0:ptr((W,0) |-> eq(llvmword(true))), \
+//   \ arg1:ptr((W,0) |-> eq(top2)), \
+//   \ frm:llvmframe [arg1:8,arg0:8], \
+//   \ x0:mbox<W>";
 
-// heapster_block_entry_hint env "mbox_copy_chain" 7 "top1:llvmptr 64,top2:llvmptr 64" "frm:llvmframe 64" "top1:mbox<W>, top2:mbox<W>, frm:llvmframe []";
+// heapster_block_entry_hint env "mbox_copy_chain" 7
+//   "top1:llvmptr 64, top2:llvmptr 64"
+//   "frm:llvmframe 64"
+//   "top1:mbox<W>, top2:mbox<W>, frm:llvmframe []";
 
-heapster_typecheck_fun env "mbox_copy_chain" "().arg0:mbox<W,llvmword(0)>, arg1:int64<> -o arg0:mbox<W,llvmword(0)>, arg1:true, ret:mbox<W,llvmword(0)>";
+heapster_typecheck_fun env "mbox_copy_chain"
+  "(). arg0:mbox<W,llvmword(0)>, arg1:int64<> -o \
+     \ arg0:mbox<W,llvmword(0)>, arg1:true, ret:mbox<W,llvmword(0)>";
 
 
-heapster_typecheck_fun env "mbox_detach" "().arg0:ptr((W,0) |-> mbox<W,llvmword(0)>) -o arg0:ptr((W,0) |-> mbox<W,llvmword(0)>), ret:mbox<W,llvmword(0)>";
+heapster_typecheck_fun env "mbox_detach"
+  "(). arg0:ptr((W,0) |-> mbox<W,llvmword(0)>) -o \
+     \ arg0:ptr((W,0) |-> mbox<W,llvmword(0)>), ret:mbox<W,llvmword(0)>";
 
 
-heapster_typecheck_fun env "mbox_detach_from_end" "().arg0:ptr((W,0) |-> mbox<W,llvmword(0)>), arg1:int64<> -o arg0:ptr((W,0) |-> mbox<W,llvmword(0)>), arg1:true, ret:mbox<W,llvmword(0)>";
+heapster_typecheck_fun env "mbox_detach_from_end"
+  "(). arg0:ptr((W,0) |-> mbox<W,llvmword(0)>), arg1:int64<> -o \
+     \ arg0:ptr((W,0) |-> mbox<W,llvmword(0)>), arg1:true, ret:mbox<W,llvmword(0)>";
 
 
-heapster_typecheck_fun env "mbox_increment" "().arg0:mbox<W,llvmword(0)> -o arg0:mbox<W,llvmword(0)>, ret:int32<>";
+heapster_typecheck_fun env "mbox_increment"
+  "(). arg0:mbox<W,llvmword(0)> -o arg0:mbox<W,llvmword(0)>, ret:int32<>";
 
 
-heapster_block_entry_hint env "mbox_randomize" 16 "top1:llvmptr 64" "frm:llvmframe 64" "top1:ptr((W,0) |-> int64<>) * ptr((W,8) |-> int64<>) * ptr((W,16) |-> mbox<W,llvmword(0)>) * array(24, <128, *1, [(W,0,8) |-> int8<>]), arg0:ptr((W,0,32) |-> true), arg1:ptr((W,0) |-> eq(top1)), arg2:ptr((W,0) |-> int64<>), frm:llvmframe [arg2:8, arg1:8, arg0:4]";
+heapster_block_entry_hint env "mbox_randomize" 16
+  "top1:llvmptr 64"
+  "frm:llvmframe 64"
+  "top1:ptr((W,0) |-> int64<>) * ptr((W,8) |-> int64<>) * \
+  \     ptr((W,16) |-> mbox<W,llvmword(0)>) * array(24, <128, *1, [(W,0,8) |-> int8<>]), \
+  \ arg0:ptr((W,0,32) |-> true), arg1:ptr((W,0) |-> eq(top1)), arg2:ptr((W,0) |-> int64<>), \
+  \ frm:llvmframe [arg2:8, arg1:8, arg0:4]";
 
-heapster_typecheck_fun env "mbox_randomize" "().arg0:mbox<W,llvmword(0)> -o arg0:mbox<W,llvmword(0)>, ret:int32<>";
+heapster_typecheck_fun env "mbox_randomize"
+  "(). arg0:mbox<W,llvmword(0)> -o arg0:mbox<W,llvmword(0)>, ret:int32<>";
 
 
-heapster_typecheck_fun env "mbox_drop" "().arg0:mbox<W,llvmword(0)>, arg1:int64<> -o arg0:mbox<W,llvmword(0)>, arg1:true";
+heapster_typecheck_fun env "mbox_drop"
+  "(). arg0:mbox<W,llvmword(0)>, arg1:int64<> -o \
+     \ arg0:mbox<W,llvmword(0)>, arg1:true";
 
 
 //------------------------------------------------------------------------------
diff --git a/heapster-saw/examples/memcpy.saw b/heapster-saw/examples/memcpy.saw
index c5620066f8..1d0cc90fe7 100644
--- a/heapster-saw/examples/memcpy.saw
+++ b/heapster-saw/examples/memcpy.saw
@@ -1,14 +1,22 @@
 enable_experimental;
 env <- heapster_init_env_from_file "memcpy.sawcore" "memcpy.bc";
 
+// Integer types
 heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
 
-heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, b:llvmblock 64, len:bv 64).arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(b)), arg2:eq(llvmword(len))  -o  arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))" "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
+heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64"
+  "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, b:llvmblock 64, len:bv 64). \
+  \ arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(b)), arg2:eq(llvmword(len)) -o \
+  \ arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))"
+  "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
 
-heapster_typecheck_fun env "copy_int" "().arg0:int64<> -o ret:int64<>";
+heapster_typecheck_fun env "copy_int"
+  "().arg0:int64<> -o ret:int64<>";
 
-heapster_typecheck_fun env "copy_ptr_contents" "().arg0:ptr((R,0) |-> int64<>) -o ret:int64<>";
+heapster_typecheck_fun env "copy_ptr_contents"
+  "().arg0:ptr((R,0) |-> int64<>) -o ret:int64<>";
 
-heapster_typecheck_fun env "copy_ptr" "().arg0:ptr((W,0) |-> int64<>) -o arg0:ptr((W,0) |-> int64<>)";
+heapster_typecheck_fun env "copy_ptr"
+  "().arg0:ptr((W,0) |-> int64<>) -o arg0:ptr((W,0) |-> int64<>)";
 
 heapster_export_coq env "memcpy_gen.v";
diff --git a/heapster-saw/examples/rust_data.saw b/heapster-saw/examples/rust_data.saw
index e23b31b6b9..90bdaa185d 100644
--- a/heapster-saw/examples/rust_data.saw
+++ b/heapster-saw/examples/rust_data.saw
@@ -37,15 +37,26 @@ heapster_define_rust_type env "pub enum Option<X> { None, Some (X) }";
 // For now we have to define the shape explicitly without the int8 name because
 // we don't yet have implications on array cells
 //heapster_define_llvmshape env "str" 64 "" "exsh len:bv 64.arraysh(len,1,[(8,int8<>)])";
-heapster_define_llvmshape env "str" 64 "" "exsh len:bv 64.arraysh(len,1,[(8,exists x:bv 8.eq(llvmword(x)))])";
+heapster_define_llvmshape env "str" 64 ""
+  "exsh len:bv 64.arraysh(len,1,[(8,exists x:bv 8.eq(llvmword(x)))])";
 //heapster_define_rust_type env "type str = [u8];";
 
 // The String type
-heapster_define_llvmshape env "String" 64 "" "exsh cap:bv 64. ptrsh(arraysh(cap,1,[(8,int8<>)]));fieldsh(int64<>);fieldsh(eq(llvmword(cap)))";
+heapster_define_llvmshape env "String" 64 ""
+  "exsh cap:bv 64. ptrsh(arraysh(cap,1,[(8,int8<>)])); \
+                 \ fieldsh(int64<>);fieldsh(eq(llvmword(cap)))";
 
 // List type
-//heapster_define_llvmshape env "List" 64 "L:perm(llvmptr 64),X:llvmshape 64" "(fieldsh(eq(llvmword(0)))) orsh (fieldsh(eq(llvmword(1)));X;fieldsh(L))";
-//heapster_define_recursive_perm env "ListPerm" "X:llvmshape 64, Xlen:bv 64, rw:rwmodality, l:lifetime" "llvmptr 64" ["[l]memblock(rw,0,Xlen + 16,List<ListPerm<X,Xlen,rw,l>,X>)"] "\\ (X:sort 0) (_:Vec 64 Bool) -> List X" "\\ (X:sort 0) (_:Vec 64 Bool) -> foldListPermH X" "\\ (X:sort 0) (_:Vec 64 Bool) -> unfoldListPermH X";
+//heapster_define_llvmshape env "List" 64
+//  "L:perm(llvmptr 64), X:llvmshape 64"
+//  "fieldsh(eq(llvmword(0))) orsh (fieldsh(eq(llvmword(1))); X; fieldsh(L))";
+//heapster_define_recursive_perm env "ListPerm"
+//  "X:llvmshape 64, Xlen:bv 64, rw:rwmodality, l:lifetime"
+//  "llvmptr 64"
+//  ["[l]memblock(rw,0,Xlen + 16,List<ListPerm<X,Xlen,rw,l>,X>)"]
+//  "\\ (X:sort 0) (_:Vec 64 Bool) -> List X"
+//  "\\ (X:sort 0) (_:Vec 64 Bool) -> foldListPermH X"
+//  "\\ (X:sort 0) (_:Vec 64 Bool) -> unfoldListPermH X";
 heapster_define_rust_type env "pub enum List<X> { Nil, Cons (X,Box<List<X>>) }";
 
 // The Rust Void type is really a general existential type; this is not directly
@@ -67,19 +78,25 @@ heapster_define_rust_type env "pub struct FiveValues(u32,u32,u32,u32,u32);";
 
 // MixedStruct type
 // heapster_define_llvmshape env "MixedStruct" 64 "" "String<>;fieldsh(64,int64<>);fieldsh(64,int64<>)";
-heapster_define_rust_type env "pub struct MixedStruct { pub s: String, pub i1: u64, pub i2: u64, }";
+heapster_define_rust_type env
+  "pub struct MixedStruct { pub s: String, pub i1: u64, pub i2: u64, }";
 
 // TrueEnum type
 heapster_define_rust_type env "pub enum TrueEnum { Foo, Bar, Baz }";
 
 // Opaque type for Vec<T>
-heapster_define_opaque_llvmshape env "Vec" 64 "T:llvmshape 64" "24" "\\ (T:sort 0) -> List T";
+heapster_define_opaque_llvmshape env "Vec" 64
+  "T:llvmshape 64" "24"
+  "\\ (T:sort 0) -> List T";
 
 // Opaque type for HashMap<T,U>
-heapster_define_opaque_llvmshape env "HashMap" 64 "T:llvmshape 64, U:llvmshape 64" "56" "\\ (T:sort 0) (U:sort 0) -> List (T * U)";
+heapster_define_opaque_llvmshape env "HashMap" 64
+  "T:llvmshape 64, U:llvmshape 64" "56"
+  "\\ (T:sort 0) (U:sort 0) -> List (T * U)";
 
 // BinTree<X> type
-heapster_define_rust_type env "pub enum BinTree<X> { BinLeaf (X), BinNode (Box<BinTree<X>>,Box<BinTree<X>>) }";
+heapster_define_rust_type env
+  "pub enum BinTree<X> { BinLeaf (X), BinNode (Box<BinTree<X>>,Box<BinTree<X>>) }";
 
 // Tree<X> type
 // FIXME: this does not work yet because Heapster cannot yet handle recursive types
@@ -87,13 +104,37 @@ heapster_define_rust_type env "pub enum BinTree<X> { BinLeaf (X), BinNode (Box<B
 //heapster_define_rust_type env "pub enum Tree<X> { Leaf (X), Node (Vec<Tree<X>>) }";
 
 // Enum20 type
-heapster_define_rust_type env "pub enum Enum20<X> { Enum20_0(X), Enum20_1(X), Enum20_2(X), Enum20_3(X), Enum20_4(X), Enum20_5(X), Enum20_6(X), Enum20_7(X), Enum20_8(X), Enum20_9(X), Enum20_10(X), Enum20_11(X), Enum20_12(X), Enum20_13(X), Enum20_14(X), Enum20_15(X), Enum20_16(X), Enum20_17(X), Enum20_18(X), Enum20_19(X), }";
+heapster_define_rust_type env
+  "pub enum Enum20<X> { \
+  \ Enum20_0(X), Enum20_1(X), Enum20_2(X), Enum20_3(X), Enum20_4(X), \
+  \ Enum20_5(X), Enum20_6(X), Enum20_7(X), Enum20_8(X), Enum20_9(X), \
+  \ Enum20_10(X), Enum20_11(X), Enum20_12(X), Enum20_13(X), Enum20_14(X), \
+  \ Enum20_15(X), Enum20_16(X), Enum20_17(X), Enum20_18(X), Enum20_19(X), }";
 
 // List10 type
-heapster_define_rust_type env "pub enum List10<X> { List10_Head(X,Box<List10<X>>), List10_0(X,Box<List10<X>>), List10_1(X,Box<List10<X>>), List10_2(X,Box<List10<X>>), List10_3(X,Box<List10<X>>), List10_4(X,Box<List10<X>>), List10_5(X,Box<List10<X>>), List10_6(X,Box<List10<X>>), List10_7(X,Box<List10<X>>), List10_8(X,Box<List10<X>>), List10_9(X,Box<List10<X>>), }";
+heapster_define_rust_type env
+  "pub enum List10<X> { \
+  \ List10_Head(X,Box<List10<X>>), List10_0(X,Box<List10<X>>), \
+  \ List10_1(X,Box<List10<X>>), List10_2(X,Box<List10<X>>), \
+  \ List10_3(X,Box<List10<X>>), List10_4(X,Box<List10<X>>), \
+  \ List10_5(X,Box<List10<X>>), List10_6(X,Box<List10<X>>), \
+  \ List10_7(X,Box<List10<X>>), List10_8(X,Box<List10<X>>), \
+  \ List10_9(X,Box<List10<X>>), }";
 
 // List20 type
-heapster_define_rust_type env "pub enum List20<X> { List20_Head(X,Box<List20<X>>), List20_0(X,Box<List20<X>>), List20_1(X,Box<List20<X>>), List20_2(X,Box<List20<X>>), List20_3(X,Box<List20<X>>), List20_4(X,Box<List20<X>>), List20_5(X,Box<List20<X>>), List20_6(X,Box<List20<X>>), List20_7(X,Box<List20<X>>), List20_8(X,Box<List20<X>>), List20_9(X,Box<List20<X>>), List20_10(X,Box<List20<X>>), List20_11(X,Box<List20<X>>), List20_12(X,Box<List20<X>>), List20_13(X,Box<List20<X>>), List20_14(X,Box<List20<X>>), List20_15(X,Box<List20<X>>), List20_16(X,Box<List20<X>>), List20_17(X,Box<List20<X>>), List20_18(X,Box<List20<X>>), List20_19(X,Box<List20<X>>), }";
+heapster_define_rust_type env
+  "pub enum List20<X> { \
+  \ List20_Head(X,Box<List20<X>>), List20_0(X,Box<List20<X>>), \
+  \ List20_1(X,Box<List20<X>>), List20_2(X,Box<List20<X>>), \
+  \ List20_3(X,Box<List20<X>>), List20_4(X,Box<List20<X>>), \
+  \ List20_5(X,Box<List20<X>>), List20_6(X,Box<List20<X>>), \
+  \ List20_7(X,Box<List20<X>>), List20_8(X,Box<List20<X>>), \
+  \ List20_9(X,Box<List20<X>>), List20_10(X,Box<List20<X>>), \
+  \ List20_11(X,Box<List20<X>>), List20_12(X,Box<List20<X>>), \
+  \ List20_13(X,Box<List20<X>>), List20_14(X,Box<List20<X>>), \
+  \ List20_15(X,Box<List20<X>>), List20_16(X,Box<List20<X>>), \
+  \ List20_17(X,Box<List20<X>>), List20_18(X,Box<List20<X>>), \
+  \ List20_19(X,Box<List20<X>>), }";
 
 
 /***
@@ -105,32 +146,48 @@ heapster_define_rust_type_qual env "fmt" "pub struct Error { }";
 
 // fmt::Result type
 // FIXME: there seems to be some optimization in Rust that lays out fmt::Result as a 1-bit value
-heapster_define_llvmshape env "fmt::Result" 64 "" "fieldsh(1,eq(llvmword(0))) orsh fieldsh(1,eq(llvmword(1)))";
-//heapster_define_rust_type_qual env "fmt" "pub enum Result { Ok (), Err (fmt::Error) }";
+heapster_define_llvmshape env "fmt::Result" 64 ""
+  "fieldsh(1,eq(llvmword(0))) orsh fieldsh(1,eq(llvmword(1)))";
+//heapster_define_rust_type_qual env "fmt"
+//  "pub enum Result { Ok (), Err (fmt::Error) }";
 
 // fmt::Formatter type
 heapster_define_opaque_llvmshape env "fmt::Formatter" 64 "" "64" "#()";
 
 // fmt::Alignment type
-heapster_define_rust_type_qual env "fmt" "pub enum Alignment { Left, Right, Center, Unknown,}";
+heapster_define_rust_type_qual env "fmt"
+  "pub enum Alignment { Left, Right, Center, Unknown,}";
 
 // fmt::Count type
-heapster_define_rust_type_qual env "fmt" "pub enum Count { Is(usize), Param(usize), NextParam, Implied,}";
+heapster_define_rust_type_qual env "fmt"
+  "pub enum Count { Is(usize), Param(usize), NextParam, Implied,}";
 
 // fmt::FormatSpec
-heapster_define_rust_type_qual env "fmt" "pub struct FormatSpec { pub fill: char, pub align: fmt::Alignment, pub flags: u32, pub precision: fmt::Count, pub width: fmt::Count, }";
+heapster_define_rust_type_qual env "fmt"
+  "pub struct FormatSpec { pub fill: char, pub align: fmt::Alignment, \
+                         \ pub flags: u32, pub precision: fmt::Count, \
+                         \ pub width: fmt::Count, }";
 
 // fmt::Position
-heapster_define_rust_type_qual env "fmt" "pub enum Position { Next, At(usize),}";
+heapster_define_rust_type_qual env "fmt"
+  "pub enum Position { Next, At(usize),}";
 
 // fmt::Argument type
-heapster_define_rust_type_qual env "fmt" "pub struct Argument { pub position: fmt::Position, pub format: fmt::FormatSpec,}";
+heapster_define_rust_type_qual env "fmt"
+  "pub struct Argument { pub position: fmt::Position, \
+                       \ pub format: fmt::FormatSpec,}";
 
 // fmt::ArgumentV1 type
-heapster_define_rust_type_qual env "fmt" "pub struct ArgumentV1<'a> { value: &'a Void, formatter: for <'b> fn(&'b Void, &'b mut fmt::Formatter) -> fmt::Result, }";
+heapster_define_rust_type_qual env "fmt"
+  "pub struct ArgumentV1<'a> { \
+  \ value: &'a Void, \
+  \ formatter: for <'b> fn(&'b Void, &'b mut fmt::Formatter) -> fmt::Result, }";
 
 // fmt::Arguments type
-//heapster_define_rust_type_qual env "fmt" "pub struct Arguments<'a> { pieces: &'a [&'a str], fmt: Option<&'a [fmt::Argument]>, args: &'a [fmt::ArgumentV1<'a>], }";
+//heapster_define_rust_type_qual env "fmt"
+//  "pub struct Arguments<'a> { pieces: &'a [&'a str], \
+//                            \ fmt: Option<&'a [fmt::Argument]>, \
+//                            \ args: &'a [fmt::ArgumentV1<'a>], }";
 
 
 /***
@@ -139,44 +196,105 @@ heapster_define_rust_type_qual env "fmt" "pub struct ArgumentV1<'a> { value: &'a
 
 // exchange_malloc
 exchange_malloc_sym <- heapster_find_symbol env "15exchange_malloc";
-//heapster_assume_fun_rename env exchange_malloc_sym "exchange_malloc" "(len:bv 64).arg0:eq(llvmword(len)),arg1:true -o ret:array(0,<len,*1,[(W,0,8) |-> true])" "\\ (len:Vec 64 Bool) -> returnM (BVVec 64 len #()) (repeatBVVec 64 len #() ())";
-heapster_assume_fun_rename env exchange_malloc_sym "exchange_malloc" "(len:bv 64).arg0:eq(llvmword(len)),arg1:true -o ret:memblock(W,0,len,emptysh)" "\\ (len:Vec 64 Bool) -> returnM #() ()";
+//heapster_assume_fun_rename env exchange_malloc_sym "exchange_malloc"
+//  "(len:bv 64). arg0:eq(llvmword(len)), arg1:true -o
+//              \ ret:array(0,<len,*1,[(W,0,8) |-> true])"
+//  "\\ (len:Vec 64 Bool) -> returnM (BVVec 64 len #()) (repeatBVVec 64 len #() ())";
+heapster_assume_fun_rename env exchange_malloc_sym "exchange_malloc"
+  "(len:bv 64). arg0:eq(llvmword(len)), arg1:true -o \
+              \ ret:memblock(W,0,len,emptysh)"
+  "\\ (len:Vec 64 Bool) -> returnM #() ()";
 
 // memcpy
-heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, b:llvmblock 64, len:bv 64).arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(b)), arg2:eq(llvmword(len))  -o  arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))" "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
+heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64"
+  "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, b:llvmblock 64, len:bv 64). \
+  \ arg0:[l1]memblock(W,0,len,sh), arg1:[l2]memblock(rw,0,len,eqsh(b)), arg2:eq(llvmword(len)) -o \
+  \ arg0:[l1]memblock(W,0,len,eqsh(b)), arg1:[l2]memblock(rw,0,len,eqsh(b))"
+  "\\ (X:sort 0) (len:Vec 64 Bool) (x:X) (_:#()) -> returnM (#() * #()) ((),())";
 
 // <str as alloc::string::ToString>::to_string
 to_string_str <- heapster_find_symbol env "$LT$str$u20$as$u20$alloc..string..ToString$GT$9to_string";
 // NOTE: this is the more incorrect version, with no lifetime argument and no shapes
-//heapster_assume_fun_rename env to_string_str "to_string_str" "(len:bv 64). arg0:memblock(W,0,24,emptysh), arg1:array(0,<len,*1,[(R,0,8) |-> int8<>]), arg2:eq(llvmword(len)) -o arg0:exists len':bv 64. ptr((W,0) |-> array(0,<len',*1,[(W,0,8) |-> int8<>])) * ptr((W,8) |-> int64<>) * ptr((W,16) |-> eq(llvmword(len')))" "\\ (len:Vec 64 Bool) (_:#()) (str:BVVec 64 len (Vec 8 Bool)) -> returnM (Sigma (Vec 64 Bool) (\\ (len':Vec 64 Bool) -> BVVec 64 len' (Vec 8 Bool) * Vec 64 Bool * #())) (exists (Vec 64 Bool) (\\ (len':Vec 64 Bool) -> BVVec 64 len' (Vec 8 Bool) * Vec 64 Bool * #()) len (str, len, ()))";
+//heapster_assume_fun_rename env to_string_str "to_string_str"
+//  "(len:bv 64). arg0:memblock(W,0,24,emptysh),
+//              \ arg1:array(0,<len,*1,[(R,0,8) |-> int8<>]), \
+//              \ arg2:eq(llvmword(len)) -o \
+//              \ arg0:exists len':bv 64. ptr((W,0) |-> array(0,<len',*1,[(W,0,8) |-> int8<>])) * \
+//              \                         ptr((W,8) |-> int64<>) * ptr((W,16) |-> eq(llvmword(len')))"
+//  "\\ (len:Vec 64 Bool) (_:#()) (str:BVVec 64 len (Vec 8 Bool)) -> \
+//    \ returnM (Sigma (Vec 64 Bool) (\\ (len':Vec 64 Bool) -> \
+//    \           BVVec 64 len' (Vec 8 Bool) * Vec 64 Bool * #())) \
+//    \         (exists (Vec 64 Bool) (\\ (len':Vec 64 Bool) -> \
+//    \           BVVec 64 len' (Vec 8 Bool) * Vec 64 Bool * #()) len (str, len, ()))";
 
 // NOTE: this is the incorrect version, with no lifetime argument
-heapster_assume_fun_rename env to_string_str "to_string_str" "(len:bv 64). arg0:memblock(W,0,24,emptysh), arg1:array(0,<len,*1,[(R,0,8) |-> int8<>]), arg2:eq(llvmword(len)) -o arg0:memblock(W,0,24,String<>)" "\\ (len:Vec 64 Bool) (_:#()) (str:BVVec 64 len (Vec 8 Bool)) -> returnM (Sigma (Vec 64 Bool) (\\ (len':Vec 64 Bool) -> BVVec 64 len' (Vec 8 Bool) * Vec 64 Bool * #())) (exists (Vec 64 Bool) (\\ (len':Vec 64 Bool) -> BVVec 64 len' (Vec 8 Bool) * Vec 64 Bool * #()) len (str, len, ()))";
+heapster_assume_fun_rename env to_string_str "to_string_str"
+  "(len:bv 64). arg0:memblock(W,0,24,emptysh), \
+              \ arg1:array(0,<len,*1,[(R,0,8) |-> int8<>]), \
+              \ arg2:eq(llvmword(len)) -o \
+              \ arg0:memblock(W,0,24,String<>)"
+  "\\ (len:Vec 64 Bool) (_:#()) (str:BVVec 64 len (Vec 8 Bool)) -> \
+    \ returnM (Sigma (Vec 64 Bool) (\\ (len':Vec 64 Bool) -> \
+    \           BVVec 64 len' (Vec 8 Bool) * Vec 64 Bool * #())) \
+    \         (exists (Vec 64 Bool) (\\ (len':Vec 64 Bool) -> \
+    \           BVVec 64 len' (Vec 8 Bool) * Vec 64 Bool * #()) len (str, len, ()))";
 
 // FIXME: this is the correct version, with a lifetime argument
-//heapster_assume_fun_rename env to_string_str "to_string_str" "(ps:lowned_perm,l:lifetime,len:bv 64). l:lowned ps, arg0:[l]memblock(W,0,24,emptysh), arg1:array(0,<len,*1,[[l](R,0,8) |-> int8<>]), arg2:eq(llvmword(len)) -o l:lowned ps, arg0:[l]memblock(W,0,24,String<>)" "\\ (len:Vec 64 Bool) (_:#()) (str:BVVec 64 len (Vec 8 Bool)) -> returnM (Sigma (Vec 64 Bool) (\\ (len':Vec 64 Bool) -> BVVec 64 len' (Vec 8 Bool) * Vec 64 Bool * #())) (exists (Vec 64 Bool) (\\ (len':Vec 64 Bool) -> BVVec 64 len' (Vec 8 Bool) * Vec 64 Bool * #()) len (str, len, ()))";
+//heapster_assume_fun_rename env to_string_str "to_string_str"
+//  "(ps:lowned_perm, l:lifetime, len:bv 64). \
+//  \ l:lowned ps, arg0:[l]memblock(W,0,24,emptysh), \
+//  \ arg1:array(0,<len,*1,[[l](R,0,8) |-> int8<>]), arg2:eq(llvmword(len)) -o \
+//  \ l:lowned ps, arg0:[l]memblock(W,0,24,String<>)"
+//  "\\ (len:Vec 64 Bool) (_:#()) (str:BVVec 64 len (Vec 8 Bool)) -> \
+//    \ returnM (Sigma (Vec 64 Bool) (\\ (len':Vec 64 Bool) -> \
+//    \           BVVec 64 len' (Vec 8 Bool) * Vec 64 Bool * #())) \
+//    \         (exists (Vec 64 Bool) (\\ (len':Vec 64 Bool) -> \
+//    \           BVVec 64 len' (Vec 8 Bool) * Vec 64 Bool * #()) len (str, len, ()))";
 
 
 // HashMap::insert
 // FIXME: we currently pretend this always returns None
-hashmap_u64_u64_insert_sym <- heapster_find_symbol env "std11collections4hash3map24HashMap$LT$K$C$V$C$S$GT$6insert";
-heapster_assume_fun_rename_prim env hashmap_u64_u64_insert_sym "hashmap_u64_u64_insert" "<'a> fn (&'a mut HashMap<u64,u64>,u64,u64) -> Option<u64>";
-//heapster_assume_fun_rename env hashmap_u64_u64_insert_sym "hashmap_u64_u64_insert" "<'a> fn (&'a mut HashMap<u64,u64>,u64,u64) -> Option<u64>" "\\ (endl:HashMap (Vec 64 Bool) (Vec 64 Bool) * #() -> CompM (HashMap (Vec 64 Bool) (Vec 64 Bool) * #())) (h:HashMap (Vec 64 Bool) (Vec 64 Bool)) (k:Vec 64 Bool) (v:Vec 64 Bool) -> returnM ((#() -> CompM (HashMap (Vec 64 Bool) (Vec 64 Bool) * #())) * Either #() (Vec 64 Bool) * #()) ((\\ (_:#()) -> returnM (HashMap (Vec 64 Bool) (Vec 64 Bool) * #()) (Cons (Vec 64 Bool * Vec 64 Bool) (k,v) h, ())), Left #() (Vec 64 Bool) (), ())";
+hashmap_u64_u64_insert_sym <- heapster_find_symbol env
+  "std11collections4hash3map24HashMap$LT$K$C$V$C$S$GT$6insert";
+heapster_assume_fun_rename_prim env hashmap_u64_u64_insert_sym "hashmap_u64_u64_insert"
+  "<'a> fn (&'a mut HashMap<u64,u64>,u64,u64) -> Option<u64>";
+//heapster_assume_fun_rename env hashmap_u64_u64_insert_sym "hashmap_u64_u64_insert"
+//  "<'a> fn (&'a mut HashMap<u64,u64>,u64,u64) -> Option<u64>"
+//  "\\ (endl:HashMap (Vec 64 Bool) (Vec 64 Bool) * #() -> \
+//    \       CompM (HashMap (Vec 64 Bool) (Vec 64 Bool) * #())) \
+//    \ (h:HashMap (Vec 64 Bool) (Vec 64 Bool)) (k:Vec 64 Bool) (v:Vec 64 Bool) -> \
+//    \ returnM ((#() -> CompM (HashMap (Vec 64 Bool) (Vec 64 Bool) * #())) * \
+//    \          Either #() (Vec 64 Bool) * #()) \
+//    \         ((\\ (_:#()) -> returnM (HashMap (Vec 64 Bool) (Vec 64 Bool) * #()) \
+//    \                                 (Cons (Vec 64 Bool * Vec 64 Bool) (k,v) h, ())), \
+//    \          Left #() (Vec 64 Bool) (), ())";
 
 /*
 String__fmt_sym <- heapster_find_trait_method_symbol env "core::fmt::Display::fmt<String>";
-// heapster_assume_fun_rename env String__fmt_sym "String__fmt" "<'a, 'b> fn(&'a String, f: &'b mut fmt::Formatter) -> fmt::Result" "\\ (end_a : List (Vec 8 Bool) * #() -> CompM (List (Vec 8 Bool) * #())) (end_b : #() * #() -> CompM (#() * #())) (str:List (Vec 8 Bool)) (fmt : #()) -> returnM ((#() -> CompM (List (Vec 8 Bool) * #())) * (#() -> CompM (#() * #())) * Either #() #() * #()) ((\\ (_:#()) -> returnM (List (Vec 8 Bool) * #()) (str, ())), (\\ (_:#()) -> returnM (#() * #()) ((), ())), Left #() #() (), ())";
-heapster_assume_fun_rename_prim env String__fmt_sym "String__fmt" "<'a, 'b> fn(&'a String, f: &'b mut fmt::Formatter) -> fmt::Result";
+// heapster_assume_fun_rename env String__fmt_sym "String__fmt"
+//  "<'a, 'b> fn(&'a String, f: &'b mut fmt::Formatter) -> fmt::Result"
+//  "\\ (end_a : List (Vec 8 Bool) * #() -> CompM (List (Vec 8 Bool) * #())) \
+//    \ (end_b : #() * #() -> CompM (#() * #())) (str:List (Vec 8 Bool)) (fmt : #()) -> \
+//    \ returnM ((#() -> CompM (List (Vec 8 Bool) * #())) * \
+//    \          (#() -> CompM (#() * #())) * Either #() #() * #()) \
+//    \         ((\\ (_:#()) -> returnM (List (Vec 8 Bool) * #()) \
+//    \                                 (str, ())), \
+//    \          (\\ (_:#()) -> returnM (#() * #()) ((), ())), \
+//    \          Left #() #() (), ())";
+heapster_assume_fun_rename_prim env String__fmt_sym "String__fmt"
+  "<'a, 'b> fn(&'a String, f: &'b mut fmt::Formatter) -> fmt::Result";
 */
 
 
 // Arguments::new_v1
 Arguments__new_v1_sym <- heapster_find_symbol env "3fmt9Arguments6new_v1";
-//heapster_assume_fun_rename_prim env Arguments__new_v1_sym "Arguments__new" "<'a> fn (pieces: &'a [&'a str], args: &'a [ArgumentV1<'a>]) -> Arguments<'a>";
+//heapster_assume_fun_rename_prim env Arguments__new_v1_sym "Arguments__new"
+//  "<'a> fn (pieces: &'a [&'a str], args: &'a [ArgumentV1<'a>]) -> Arguments<'a>";
 
 // Formatter::write_str
 Formatter__write_str_sym <- heapster_find_symbol env "9Formatter9write_str";
-heapster_assume_fun_rename_prim env Formatter__write_str_sym "Formatter__write_str" "<'a,'b> fn (&'a mut fmt::Formatter, &'b str) -> fmt::Result";
+heapster_assume_fun_rename_prim env Formatter__write_str_sym "Formatter__write_str"
+  "<'a,'b> fn (&'a mut fmt::Formatter, &'b str) -> fmt::Result";
 
 
 /***
@@ -196,72 +314,103 @@ heapster_typecheck_fun_rename env mk_two_values_sym "mk_two_values" "<> fn (u32,
 
 // test_result
 test_result_sym <- heapster_find_symbol env "11test_result";
-heapster_typecheck_fun_rename env test_result_sym "test_result" "<'a> fn (r:&'a Result<u64,u64>) -> bool";
-//heapster_typecheck_fun_rename env test_result_sym "test_result" "().arg0:memblock(R,0,16,Result<fieldsh(int64<>),fieldsh(int64<>)>) -o ret:int1<>";
+heapster_typecheck_fun_rename env test_result_sym "test_result"
+  "<'a> fn (r:&'a Result<u64,u64>) -> bool";
+//heapster_typecheck_fun_rename env test_result_sym "test_result"
+//  "().arg0:memblock(R,0,16,Result<fieldsh(int64<>),fieldsh(int64<>)>) -o ret:int1<>";
 
 // test_sum_impl
 test_sum_impl_sym <- heapster_find_symbol env "13test_sum_impl";
-heapster_typecheck_fun_rename env test_sum_impl_sym "test_sum_impl" "().arg0:memblock(R,0,16,Sum<fieldsh(int64<>),fieldsh(int64<>)>) -o ret:int1<>";
+heapster_typecheck_fun_rename env test_sum_impl_sym "test_sum_impl"
+  "().arg0:memblock(R,0,16,Sum<fieldsh(int64<>),fieldsh(int64<>)>) -o ret:int1<>";
 
 // NOTE: Fails because of `clone` in the implementation
 // MixedStruct::get_s
 // mixed_struct_get_s <- heapster_find_symbol env "11MixedStruct5get_s";
-// heapster_typecheck_fun_rename env mixed_struct_get_s "MixedStruct_get_s" "<'a> fn (m:&'a MixedStruct) -> String";
+// heapster_typecheck_fun_rename env mixed_struct_get_s "MixedStruct_get_s"
+//   "<'a> fn (m:&'a MixedStruct) -> String";
 
 // MixedStruct::get_i1
 mixed_struct_get_i1 <- heapster_find_symbol env "11MixedStruct6get_i1";
-heapster_typecheck_fun_rename env mixed_struct_get_i1 "MixedStruct_get_i1" "<'a> fn (m:&'a MixedStruct) -> u64";
+heapster_typecheck_fun_rename env mixed_struct_get_i1 "MixedStruct_get_i1"
+  "<'a> fn (m:&'a MixedStruct) -> u64";
 
 // MixedStruct::get_i2
 mixed_struct_get_i2 <- heapster_find_symbol env "11MixedStruct6get_i2";
-heapster_typecheck_fun_rename env mixed_struct_get_i2 "MixedStruct_get_i2" "<'a> fn (m:&'a MixedStruct) -> u64";
+heapster_typecheck_fun_rename env mixed_struct_get_i2 "MixedStruct_get_i2"
+  "<'a> fn (m:&'a MixedStruct) -> u64";
 
 cycle_true_enum_sym <- heapster_find_symbol env "15cycle_true_enum";
 // NOTE: This typecheck requires full(er) support for disjunctive shapes, which Heapster currently lacks
-// heapster_typecheck_fun_rename env cycle_true_enum_sym "cycle_true_enum" "<'a> fn (te:&'a TrueEnum) -> TrueEnum";
+// heapster_typecheck_fun_rename env cycle_true_enum_sym "cycle_true_enum"
+//   "<'a> fn (te:&'a TrueEnum) -> TrueEnum";
 
 TrueEnum__fmt_sym <- heapster_find_trait_method_symbol env "core::fmt::Display::fmt<TrueEnum>";
-heapster_typecheck_fun_rename env TrueEnum__fmt_sym "TrueEnum__fmt" "<'a, 'b> fn (&'a TrueEnum, f: &'b mut fmt::Formatter) -> fmt::Result";
+heapster_typecheck_fun_rename env TrueEnum__fmt_sym "TrueEnum__fmt"
+  "<'a, 'b> fn (&'a TrueEnum, f: &'b mut fmt::Formatter) -> fmt::Result";
 
 // list_is_empty
 list_is_empty_sym <- heapster_find_symbol env "13list_is_empty";
-heapster_typecheck_fun_rename env list_is_empty_sym "list_is_empty" "<'a> fn (l: &'a List<u64>) -> bool";
-//heapster_typecheck_fun_rename env list_is_empty_sym "list_is_empty" "(rw:rwmodality).arg0:ListPerm<fieldsh(int64<>),8,rw,always> -o ret:int1<>";
+heapster_typecheck_fun_rename env list_is_empty_sym "list_is_empty"
+  "<'a> fn (l: &'a List<u64>) -> bool";
+//heapster_typecheck_fun_rename env list_is_empty_sym "list_is_empty"
+//  "(rw:rwmodality).arg0:ListPerm<fieldsh(int64<>),8,rw,always> -o ret:int1<>";
 
 // list_head
 list_head_sym <- heapster_find_symbol env "9list_head";
-heapster_typecheck_fun_rename env list_head_sym "list_head" "<'a> fn (l: &'a List<u64>) -> Box<Sum<u64,()>>";
-//heapster_typecheck_fun_rename env list_head_sym "list_head" "(rw:rwmodality).arg0:List<fieldsh(int64<>),8,rw,always> -o ret:memblock(W,0,16,Result<fieldsh(int64<>),emptysh>)";
+heapster_typecheck_fun_rename env list_head_sym "list_head"
+  "<'a> fn (l: &'a List<u64>) -> Box<Sum<u64,()>>";
+//heapster_typecheck_fun_rename env list_head_sym "list_head"
+//  "(rw:rwmodality). arg0:List<fieldsh(int64<>),8,rw,always> -o \
+//                  \ ret:memblock(W,0,16,Result<fieldsh(int64<>),emptysh>)";
 
 // list_head_impl
 list_head_impl_sym <- heapster_find_symbol env "14list_head_impl";
-heapster_typecheck_fun_rename env list_head_impl_sym "list_head_impl" "<'a> fn (l: &'a List<u64>) -> Result<u64,()>";
-//heapster_typecheck_fun_rename env list_head_impl_sym "list_head_impl" "(rw:rwmodality).arg0:List<fieldsh(int64<>),8,rw,always> -o ret:(struct(eq(llvmword(0)),exists z:bv 64. eq(llvmword(z)))) or (struct(eq(llvmword(1)),true))";
+heapster_typecheck_fun_rename env list_head_impl_sym "list_head_impl"
+  "<'a> fn (l: &'a List<u64>) -> Result<u64,()>";
+//heapster_typecheck_fun_rename env list_head_impl_sym "list_head_impl"
+//  "(rw:rwmodality). arg0:List<fieldsh(int64<>),8,rw,always> -o \
+//                  \ ret:(struct(eq(llvmword(0)), exists z:bv 64. eq(llvmword(z)))) or \
+//                  \     (struct(eq(llvmword(1)),true))";
 
 // list64_is_empty
 list64_is_empty_sym <- heapster_find_symbol env "15list64_is_empty";
-heapster_typecheck_fun_rename env list_is_empty_sym "list64_is_empty" "<'a> fn (l: &'a List64<>) -> bool";
+heapster_typecheck_fun_rename env list_is_empty_sym "list64_is_empty"
+  "<'a> fn (l: &'a List64<>) -> bool";
 
 // StrStruct::new
 str_struct_new <- heapster_find_symbol env "9StrStruct3new";
 
 // FIXME: this is the simplified version, that returns ptr permissions
-//heapster_typecheck_fun_rename env str_struct_new "str_struct_new" "(len:bv 64).arg0:memblock(W,0,24,emptysh), arg1:array(0,<len,*1,[(R,0,8) |-> int8<>]), arg2:eq(llvmword(len)) -o arg0:exists len':bv 64. ptr((W,0) |-> array(0,<len',*1,[(R,0,8) |-> int8<>])) * ptr((W,8) |-> int64<>) * ptr((W,16) |-> eq(llvmword(len')))";
+//heapster_typecheck_fun_rename env str_struct_new "str_struct_new"
+//  "(len:bv 64). arg0:memblock(W,0,24,emptysh), \
+//              \ arg1:array(0,<len,*1,[(R,0,8) |-> int8<>]), \
+//              \ arg2:eq(llvmword(len)) -o \
+//              \ arg0:exists len':bv 64. ptr((W,0) |-> array(0,<len',*1,[(R,0,8) |-> int8<>])) * \
+//              \\     ptr((W,8) |-> int64<>) * ptr((W,16) |-> eq(llvmword(len')))";
 
 // FIXME: this is the correct version, with the String shape
-heapster_typecheck_fun_rename env str_struct_new "str_struct_new" "(len:bv 64).arg0:memblock(W,0,24,emptysh), arg1:array(0,<len,*1,[(R,0,8) |-> int8<>]), arg2:eq(llvmword(len)) -o arg0:memblock(W,0,24,String<>)";
+heapster_typecheck_fun_rename env str_struct_new "str_struct_new"
+  "(len:bv 64). arg0:memblock(W,0,24,emptysh), \
+              \ arg1:array(0,<len,*1,[(R,0,8) |-> int8<>]), \
+              \ arg2:eq(llvmword(len)) -o \
+              \ arg0:memblock(W,0,24,String<>)";
 
 bintree_is_leaf_sym <- heapster_find_symbol env "15bintree_is_leaf";
-heapster_typecheck_fun_rename env bintree_is_leaf_sym "bintree_is_leaf" "<'a> fn (t: &'a BinTree<u64>) -> bool";
+heapster_typecheck_fun_rename env bintree_is_leaf_sym "bintree_is_leaf"
+  "<'a> fn (t: &'a BinTree<u64>) -> bool";
 
 enum20_list_proj_sym <- heapster_find_symbol env "16enum20_list_proj";
-//heapster_typecheck_fun_rename env enum20_list_proj_sym "enum20_list_proj" "<'a> fn (x:&'a Enum20<List<u64>>) -> &'a List<u64>";
+//heapster_typecheck_fun_rename env enum20_list_proj_sym "enum20_list_proj"
+  "<'a> fn (x:&'a Enum20<List<u64>>) -> &'a List<u64>";
 
 list10_head_sym <- heapster_find_symbol env "11list10_head";
-//heapster_typecheck_fun_rename env list10_head_sym "list10_head" "<'a> fn (x:&'a List10<List<u64>>) -> &'a List<u64>";
+//heapster_typecheck_fun_rename env list10_head_sym "list10_head"
+  "<'a> fn (x:&'a List10<List<u64>>) -> &'a List<u64>";
 
 list20_head_sym <- heapster_find_symbol env "11list20_head";
-heapster_typecheck_fun_rename env list20_head_sym "list20_head" "<'a> fn (x:&'a List20<List<u64>>) -> &'a List<u64>";
+heapster_typecheck_fun_rename env list20_head_sym "list20_head"
+  "<'a> fn (x:&'a List20<List<u64>>) -> &'a List<u64>";
 
 
 /***
diff --git a/heapster-saw/examples/rust_lifetimes.saw b/heapster-saw/examples/rust_lifetimes.saw
index e30d5cfdbb..140bcf28f6 100644
--- a/heapster-saw/examples/rust_lifetimes.saw
+++ b/heapster-saw/examples/rust_lifetimes.saw
@@ -19,14 +19,21 @@ heapster_define_llvmshape env "u64" 64 "" "fieldsh(int64<>)";
  ***/
 
 // llvm.uadd.with.overflow.i64
-heapster_assume_fun env "llvm.uadd.with.overflow.i64" "().arg0:int64<>, arg1:int64<> -o ret:struct(int64<>,int1<>)" "\\ (x y:Vec 64 Bool) -> returnM (Vec 64 Bool * Vec 1 Bool) (bvAdd 64 x y, gen 1 Bool (\\ (_:Nat) -> bvCarry 64 x y))";
+heapster_assume_fun env "llvm.uadd.with.overflow.i64"
+  "(). arg0:int64<>, arg1:int64<> -o \
+     \ ret:struct(int64<>,int1<>)"
+  "\\ (x y:Vec 64 Bool) -> \
+    \ returnM (Vec 64 Bool * Vec 1 Bool) \
+    \         (bvAdd 64 x y, gen 1 Bool (\\ (_:Nat) -> bvCarry 64 x y))";
 
 // llvm.expect.i1
-heapster_assume_fun env "llvm.expect.i1" "().arg0:int1<>, arg1:int1<> -o ret:int1<>" "\\ (x y:Vec 1 Bool) -> returnM (Vec 1 Bool) x";
+heapster_assume_fun env "llvm.expect.i1"
+  "().arg0:int1<>, arg1:int1<> -o ret:int1<>" "\\ (x y:Vec 1 Bool) -> returnM (Vec 1 Bool) x";
 
 // core::panicking::panic
 //panic_sym <- heapster_find_symbol env "5panic";
-//heapster_assume_fun_rename env panic_sym "panic" "().empty -o empty" "returnM (Vec 1 Bool) x";
+//heapster_assume_fun_rename env panic_sym "panic"
+//  "().empty -o empty" "returnM (Vec 1 Bool) x";
 
 
 /***
@@ -35,11 +42,19 @@ heapster_assume_fun env "llvm.expect.i1" "().arg0:int1<>, arg1:int1<> -o ret:int
 
 // mux_mut_refs_u64
 mux_mut_refs_u64_sym <- heapster_find_symbol env "16mux_mut_refs_u64";
-heapster_typecheck_fun_rename env mux_mut_refs_u64_sym "mux_mut_refs_u64" "(l:lifetime,l1:lifetime,l2:lifetime).l:lowned (arg0:[l]memblock(R,0,8,u64<>), arg1:[l]memblock(R,0,8,u64<>) -o arg0:[l1]memblock(W,0,8,u64<>), arg1:[l2]memblock(W,0,8,u64<>)), arg0:[l]memblock(W,0,8,u64<>), arg1:[l]memblock(W,0,8,u64<>), arg2:int1<> -o l:lowned (ret:[l]memblock(R,0,8,u64<>) -o arg0:[l1]memblock(W,0,8,u64<>), arg1:[l2]memblock(W,0,8,u64<>)), ret:[l]memblock(W,0,8,u64<>)";
+heapster_typecheck_fun_rename env mux_mut_refs_u64_sym "mux_mut_refs_u64"
+  "(l:lifetime, l1:lifetime ,l2:lifetime). \
+  \ l:lowned(arg0:[l]memblock(R,0,8,u64<>), arg1:[l]memblock(R,0,8,u64<>) -o \
+  \          arg0:[l1]memblock(W,0,8,u64<>), arg1:[l2]memblock(W,0,8,u64<>)), \
+  \ arg0:[l]memblock(W,0,8,u64<>), arg1:[l]memblock(W,0,8,u64<>), arg2:int1<> -o \
+  \ l:lowned (ret:[l]memblock(R,0,8,u64<>) -o \
+  \ arg0:[l1]memblock(W,0,8,u64<>), arg1:[l2]memblock(W,0,8,u64<>)), \
+  \ ret:[l]memblock(W,0,8,u64<>)";
 
 // use_mux_mut_refs
 use_mux_mut_refs_sym <- heapster_find_symbol env "16use_mux_mut_refs";
-heapster_typecheck_fun_rename env use_mux_mut_refs_sym "use_mux_mut_refs" "(). empty -o ret:int64<>";
+heapster_typecheck_fun_rename env use_mux_mut_refs_sym "use_mux_mut_refs"
+  "(). empty -o ret:int64<>";
 
 
 /***
diff --git a/heapster-saw/examples/string_set.saw b/heapster-saw/examples/string_set.saw
index aa516df987..ed7992b0c0 100644
--- a/heapster-saw/examples/string_set.saw
+++ b/heapster-saw/examples/string_set.saw
@@ -14,17 +14,28 @@ heapster_define_opaque_perm env "string_set" "rw:rwmodality, l:lifetime" "llvmpt
 // heapster_define_opaque_perm env "string_set" "rw:rwmodality, l:lifetime" "llvmptr 64" "StringSet.stringList";
 
 
-heapster_assume_fun env "string_set_insert" "(l1:lifetime).arg0:string_set<W,l1>, arg1:string<> -o arg0:string_set<W,l1>, arg1:true, ret:true" "listInsertM String";
-heapster_assume_fun env "string_set_remove" "(l1:lifetime).arg0:string_set<W,l1>, arg1:string<> -o arg0:string_set<W,l1>, arg1:string<>, ret:true" "listRemoveM String equalString";
+heapster_assume_fun env "string_set_insert"
+  "(l1:lifetime). arg0:string_set<W,l1>, arg1:string<> -o \
+                \ arg0:string_set<W,l1>, arg1:true, ret:true"
+  "listInsertM String";
+heapster_assume_fun env "string_set_remove"
+  "(l1:lifetime).arg0:string_set<W,l1>, arg1:string<> -o \
+                \ arg0:string_set<W,l1>, arg1:string<>, ret:true"
+  "listRemoveM String equalString";
 
 // The old way: we have to define names to use the functions above
-// heapster_assume_fun env "string_set_insert" "(l1:lifetime).arg0:string_set<W,l1>, arg1:string<> -o arg0:string_set<W,l1>, arg1:true, ret:true" "stringListInsertM";
-// heapster_assume_fun env "string_set_remove" "(l1:lifetime).arg0:string_set<W,l1>, arg1:string<> -o arg0:string_set<W,l1>, arg1:string<>, ret:true" "stringListRemoveM";
+// heapster_assume_fun env "string_set_insert"
+//   "(l1:lifetime). arg0:string_set<W,l1>, arg1:string<> -o \
+//                 \ arg0:string_set<W,l1>, arg1:true, ret:true"
+//   "stringListInsertM";
+// heapster_assume_fun env "string_set_remove"
+//   "(l1:lifetime). arg0:string_set<W,l1>, arg1:string<> -o \
+//                 \ arg0:string_set<W,l1>, arg1:string<>, ret:true"
+//   "stringListRemoveM";
 
 // Type-check our insert_remove function
-heapster_typecheck_fun env "insert_remove" "(l:lifetime).arg0:string_set<W,l>, arg1:string<>, arg2:string<> -o arg0:string_set<W,l>, arg1:true, arg2:string<>";
-
-// FIXME: should be able to write the above like this when all the changes above happen
-// heapster_typecheck_fun env "insert_remove" "(l:lifetime).arg0:string_set<W,l>, arg1:string<>, arg2:string<> -o arg0:string_set<W,l>, arg1:true, arg2:string<>";
+heapster_typecheck_fun env "insert_remove"
+  "(l:lifetime). arg0:string_set<W,l>, arg1:string<>, arg2:string<> -o \
+               \ arg0:string_set<W,l>, arg1:true, arg2:string<>";
 
 heapster_export_coq env "string_set_gen.v";
diff --git a/heapster-saw/examples/xor_swap.saw b/heapster-saw/examples/xor_swap.saw
index 1832a9a6b6..b187001b7b 100644
--- a/heapster-saw/examples/xor_swap.saw
+++ b/heapster-saw/examples/xor_swap.saw
@@ -1,5 +1,11 @@
-// This script expects to be run from the saw-script root directory
 enable_experimental;
 env <- heapster_init_env "xor_swap" "xor_swap.bc";
-heapster_typecheck_fun env "xor_swap" "(x:bv 64, y:bv 64). arg0: ptr((W,0) |-> eq(llvmword(x))), arg1: ptr((W,0) |-> eq(llvmword(y))) -o arg0: ptr((W,0) |-> exists z:bv 64.eq(llvmword(z))), arg1: ptr((W,0) |-> exists z:bv 64.eq(llvmword(z))), ret:true";
+
+// Integer types
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
+
+heapster_typecheck_fun env "xor_swap"
+  "(). arg0: ptr((W,0) |-> int64<>), arg1: ptr((W,0) |-> int64<>) -o \
+     \ arg0: ptr((W,0) |-> int64<>), arg1: ptr((W,0) |-> int64<>), ret:true";
+
 heapster_export_coq env "xor_swap_gen.v";
diff --git a/heapster-saw/examples/xor_swap_rust.saw b/heapster-saw/examples/xor_swap_rust.saw
index ab764a67fe..1376895c67 100644
--- a/heapster-saw/examples/xor_swap_rust.saw
+++ b/heapster-saw/examples/xor_swap_rust.saw
@@ -1,11 +1,16 @@
-// This script expects to be run from the saw-script root directory
 enable_experimental;
 env <- heapster_init_env "xor_swap_rust" "xor_swap_rust.bc";
 
 heapster_define_llvmshape env "i64" 64 "" "fieldsh(exists x:bv 64.eq(llvmword(x)))";
 
 xor_swap_sym <- heapster_find_symbol env "13xor_swap_rust13xor_swap_rust";
-heapster_typecheck_fun_rename env xor_swap_sym "xor_swap_rust" "<'a,'b> fn (x:&'a mut i64, y:&'b mut i64)";
-//heapster_typecheck_fun_rename env xor_swap_sym "xor_swap_rust" "(x:bv 64, y:bv 64). arg0: ptr((W,0) |-> eq(llvmword(x))), arg1: ptr((W,0) |-> eq(llvmword(y))) -o arg0: ptr((W,0) |-> exists z:bv 64.eq(llvmword(z))), arg1: ptr((W,0) |-> exists z:bv 64.eq(llvmword(z))), ret:true";
+heapster_typecheck_fun_rename env xor_swap_sym "xor_swap_rust"
+  "<'a,'b> fn (x:&'a mut i64, y:&'b mut i64)";
+
+//heapster_typecheck_fun_rename env xor_swap_sym "xor_swap_rust"
+//  "(x:bv 64, y:bv 64). arg0:ptr((W,0) |-> eq(llvmword(x))), \
+//                     \ arg1: ptr((W,0) |-> eq(llvmword(y))) -o \
+//                     \ arg0: ptr((W,0) |-> exists z:bv 64.eq(llvmword(z))), \
+//                     \ arg1: ptr((W,0) |-> exists z:bv 64.eq(llvmword(z))), ret:true";
 
 heapster_export_coq env "xor_swap_rust_gen.v";