diff --git a/analyses/simpleactor/benchmarks-in/games_snake.rkt b/analyses/simpleactor/benchmarks-in/games_snake.rkt
new file mode 100644
index 0000000..b1d5e4b
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/games_snake.rkt
@@ -0,0 +1,255 @@
+#lang racket
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; Dummy functions `image`
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(struct image ())
+(define image/c (struct/c image))
+(define (circle r m c) (image))
+(define (empty-scene w h) (image))
+(define (place-image i₁ r c i₂) (image))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; data
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(struct posn (x y))
+(define (posn=? p1 p2)
+  (and (= (posn-x p1) (posn-x p2))
+       (= (posn-y p1) (posn-y p2))))
+(struct snake (dir segs))
+(struct world (snake food))
+(define DIR/C (one-of/c 'up 'down 'left 'right))
+(define POSN/C (struct/c posn real? real?))
+(define SNAKE/C (struct/c snake DIR/C (and/c cons? (listof POSN/C))))
+(define WORLD/C (struct/c world SNAKE/C POSN/C))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; const
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(define GRID-SIZE 30)
+(define BOARD-HEIGHT 20)
+(define BOARD-WIDTH 30)
+(define BOARD-HEIGHT-PIXELS (* GRID-SIZE BOARD-HEIGHT))
+(define BOARD-WIDTH-PIXELS (* GRID-SIZE BOARD-WIDTH))
+(define BACKGROUND (empty-scene BOARD-WIDTH-PIXELS BOARD-HEIGHT-PIXELS))
+(define SEGMENT-RADIUS (/ GRID-SIZE 2))
+(define SEGMENT-IMAGE  (circle SEGMENT-RADIUS "solid" "red"))
+(define FOOD-RADIUS SEGMENT-RADIUS)
+(define FOOD-IMAGE  (circle FOOD-RADIUS "solid" "green"))
+(define WORLD (world (snake 'right (cons (posn 5 3) empty))
+                       (posn 8 12)))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; collide
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; snake-wall-collide? : Snake -> Boolean
+;; Is the snake colliding with any/c of the walls?
+(define (snake-wall-collide? snk)
+  (head-collide? (car (snake-segs snk))))
+
+;; head-collide? : Posn -> Boolean
+(define (head-collide? p)
+  (or (<= (posn-x p) 0)
+      (>= (posn-x p) BOARD-WIDTH)
+      (<= (posn-y p) 0)
+      (>= (posn-y p) BOARD-HEIGHT)))
+
+;; snake-self-collide? : Snake -> Boolean
+(define (snake-self-collide? snk)
+  (segs-self-collide? (car (snake-segs snk))
+                      (cdr (snake-segs snk))))
+
+;; segs-self-collide? : Posn Segs -> Boolean
+(define (segs-self-collide? h segs)
+  (cond [(empty? segs) #f]
+        [else (or (posn=? (car segs) h)
+                  (segs-self-collide? h (cdr segs)))]))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; cut-tail
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; NeSegs is one of:
+;; - (cons Posn empty)
+;; - (cons Posn NeSegs)
+
+;; cut-tail : NeSegs -> Segs
+;; Cut off the tail.
+(define (cut-tail segs)
+  (let ([r (cdr segs)])
+    (cond [(empty? r) empty]
+          [else (cons (car segs) (cut-tail r))])))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; motion-help
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; next-head : Posn Direction -> Posn
+;; Compute next position for head.
+(define (next-head seg dir)
+  (cond [(equal? 'right dir) (posn (add1 (posn-x seg)) (posn-y seg))]
+        [(equal? 'left  dir) (posn (sub1 (posn-x seg)) (posn-y seg))]
+        [(equal? 'down  dir) (posn (posn-x seg) (sub1 (posn-y seg)))]
+        [else                (posn (posn-x seg) (add1 (posn-y seg)))]))
+
+;; snake-slither : Snake -> Snake
+;; move the snake one step
+(define (snake-slither snk)
+  (let ([d (snake-dir snk)])
+    (snake d
+           (cons (next-head (car (snake-segs snk))
+                            d)
+                 (cut-tail (snake-segs snk))))))
+
+;; snake-grow : Snake -> Snake
+;; Grow the snake one segment.
+(define (snake-grow snk)
+  (let ([d (snake-dir snk)])
+    (snake d
+           (cons (next-head (car (snake-segs snk))
+                            d)
+                 (snake-segs snk)))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; motion
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; world->world : World -> World
+(define (world->world w)
+  (cond [(eating? w) (snake-eat w)]
+        [else
+         (world (snake-slither (world-snake w))
+                (world-food w))]))
+;; eating? : World -> Boolean
+;; Is the snake eating the food in the world.
+(define (eating? w)
+  (posn=? (world-food w)
+          (car (snake-segs (world-snake w)))))
+;; snake-change-direction : Snake Direction -> Snake
+;; Change the direction of the snake.
+(define (snake-change-direction snk dir)
+  (snake dir
+         (snake-segs snk)))
+;; world-change-dir : World Direction -> World
+;; Change direction of the world.
+(define (world-change-dir w dir)
+  (world (snake-change-direction (world-snake w) dir)
+         (world-food w)))
+;; snake-eat : World -> World
+;; Eat the food and generate a new one.
+(define (snake-eat w)
+  (world (snake-grow (world-snake w))
+         ;(posn (random BOARD-WIDTH) (random BOARD-HEIGHT))
+         (posn (- BOARD-WIDTH 1) (- BOARD-HEIGHT 1))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; handlers
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; handle-key : World String -> World
+(define (handle-key w ke)
+  (cond [(equal? ke "w") (world-change-dir w 'up)]
+        [(equal? ke "s") (world-change-dir w 'down)]
+        [(equal? ke "a") (world-change-dir w 'left)]
+        [(equal? ke "d") (world-change-dir w 'right)]
+        [else w]))
+
+;; game-over? : World -> Boolean
+(define (game-over? w)
+  (or (snake-wall-collide? (world-snake w))
+      (snake-self-collide? (world-snake w))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; scenes
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; world->scene : World -> Image
+;; Build an image of the given world.
+(define (world->scene w)
+  (snake+scene (world-snake w)
+               (food+scene (world-food w) BACKGROUND)))
+
+;; food+scene : Food Image -> Image
+;; Add image of food to the given scene.
+(define (food+scene f scn)
+  (place-image-on-grid FOOD-IMAGE (posn-x f) (posn-y f) scn))
+
+;; place-image-on-grid : Image Number Number Image -> Image
+;; Just like PLACE-IMAGE, but use grid coordinates.
+(define (place-image-on-grid img x y scn)
+  (place-image img
+               (* GRID-SIZE x)
+               (- BOARD-HEIGHT-PIXELS (* GRID-SIZE y))
+               scn))
+
+;; snake+scene : Snake Image -> Image
+;; Add an image of the snake to the scene.
+(define (snake+scene snk scn)
+  (segments+scene (snake-segs snk) scn))
+
+;; segments+scene : Segs Image -> Image
+;; Add an image of the snake segments to the scene.
+(define (segments+scene segs scn)
+  (cond [(empty? segs) scn]
+        [else (segments+scene (cdr segs) ;; tail recursion
+                              (segment+scene (car segs) scn))]))
+
+;; segment+scene : Posn Image -> Image
+;; Add one snake segment to a scene.
+(define (segment+scene seg scn)
+  (place-image-on-grid SEGMENT-IMAGE (posn-x seg) (posn-y seg) scn))
+
+(provide
+ (contract-out
+  ;; data
+  ;[DIR/C contract?]
+  ;[POSN/C contract?]
+  ;[SNAKE/C contract?]
+  ;[WORLD/C contract?]
+  ;[struct posn ([x real?] [y real?])]
+  [posn=? (-> POSN/C POSN/C  boolean?/c)]
+  ;[struct snake ([dir DIR/C] [segs (and/c cons? (listof POSN/C))])]
+  ;[struct world ([snake SNAKE/C] [food POSN/C])]
+  ;; const
+  [WORLD WORLD/C]
+  [BACKGROUND image/c]
+  [FOOD-IMAGE image/c]
+  [SEGMENT-IMAGE image/c]
+  [GRID-SIZE real?]
+  [BOARD-HEIGHT-PIXELS real?]
+  [BOARD-WIDTH real?]
+  [BOARD-HEIGHT real?]
+  ;; collide
+  [snake-wall-collide? (-> SNAKE/C boolean?/c)]
+  [snake-self-collide? (-> SNAKE/C boolean?/c)]
+  ;; cut-tail
+  [cut-tail (-> (and/c cons?/c (listof POSN/C)) (listof POSN/C))]
+  ;; motion-help
+  [snake-slither (-> SNAKE/C SNAKE/C)]
+  [snake-grow (-> SNAKE/C SNAKE/C)]
+  ;; motion
+  [world-change-dir (-> WORLD/C DIR/C WORLD/C)]
+  [world->world (-> WORLD/C WORLD/C)]
+  ;; handlers
+  [handle-key (-> WORLD/C string?/c WORLD/C)]
+  [game-over? (-> WORLD/C boolean?/c)]
+  ;; scenes
+  [world->scene (-> WORLD/C image/c)]
+  [food+scene (-> POSN/C image/c image/c)]
+  [place-image-on-grid (-> image/c real?/c real?/c image/c image/c)]
+  [snake+scene (-> SNAKE/C image/c  image/c)]
+  [segments+scene (-> (listof POSN/C) image/c image/c)]
+  [segment+scene (-> POSN/C image/c  image/c)]
+  ))
+
+
diff --git a/analyses/simpleactor/benchmarks-in/games_tetris.rkt b/analyses/simpleactor/benchmarks-in/games_tetris.rkt
new file mode 100644
index 0000000..7340083
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/games_tetris.rkt
@@ -0,0 +1,469 @@
+#lang racket
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; data
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(struct block (x y color))
+(struct tetra (center blocks))
+(struct world (tetra blocks))
+(struct posn (x y))
+(define COLOR/C symbol?)
+(define POSN/C (struct/c posn real? real?))
+(define BLOCK/C (struct/c block real? real? COLOR/C))
+(define BSET/C (listof BLOCK/C))
+(define TETRA/C (struct/c tetra POSN/C BSET/C))
+(define WORLD/C (struct/c world TETRA/C BSET/C))
+
+(define (posn=? p1 p2)
+  (and (= (posn-x p1) (posn-x p2))
+       (= (posn-y p1) (posn-y p2))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; consts
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define block-size 20)
+(define board-height 20)
+(define board-width 10)
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; block
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; block=? : Block Block -> Boolean
+;; Determines if two blocks are the same (ignoring color).
+(define (block=? b1 b2)
+  (and (= (block-x b1) (block-x b2))
+       (= (block-y b1) (block-y b2))))
+
+;; block-move : Number Number Block -> Block
+(define (block-move dx dy b)
+  (block (+ dx (block-x b))
+         (+ dy (block-y b))
+         (block-color b)))
+
+;; block-rotate-ccw : Posn Block -> Block
+;; Rotate the block 90 counterclockwise around the posn.
+(define (block-rotate-ccw c b)
+  (block (+ (posn-x c) (- (posn-y c) (block-y b)))
+         (+ (posn-y c) (- (block-x b) (posn-x c)))
+         (block-color b)))
+
+;; block-rotate-cw : Posn Block -> Block
+;; Rotate the block 90 clockwise around the posn.
+(define (block-rotate-cw c b)
+  (block-rotate-ccw c (block-rotate-ccw c (block-rotate-ccw c b))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; list
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; TODO: some way to attach our specialized contract to library function instead
+
+(define (ormap p? xs)
+  (cond [(null? xs) #f]
+        [else (or (p? (car xs)) (ormap p? (cdr xs)))]))
+
+(define (andmap p? xs)
+  (cond [(null? xs) #t]
+        [else (and (p? (car xs)) (andmap p? (cdr xs)))]))
+
+(define (map f xs)
+  (cond [(null? xs) null]
+        [else (cons (f (car xs)) (map f (cdr xs)))]))
+
+(define (filter p? xs)
+  (cond [(null? xs) null]
+        [(p? (car xs)) (cons (car xs) (filter p? (cdr xs)))]
+        [else (filter p? (cdr xs))]))
+
+(define (append l r)
+  (cond [(null? l) r]
+        [else (cons (car l) (append (cdr l) r))]))
+
+(define (length xs)
+  (cond [(null? xs) 0]
+        [else (+ 1 (length (cdr xs)))]))
+
+(define (foldr f a xs)
+  (cond [(null? xs) a]
+        [else (f (car xs) (foldr f a (cdr xs)))]))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; bset
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; blocks-contains? : BSet Block -> Boolean
+;; Determine if the block is in the set of blocks.
+(define (blocks-contains? bs b)
+  (ormap (λ (c) (block=? b c)) bs))
+
+;; blocks-subset? : BSet BSet -> Boolean
+;; is every element in bs1 also in bs2?
+(define (blocks-subset? bs1 bs2)
+  (andmap (λ (b) (blocks-contains? bs2 b)) bs1))
+
+;; blocks=? : BSet BSet -> Boolean
+;; Determine if given sets of blocks are equal.
+(define (blocks=? bs1 bs2)
+  (and (blocks-subset? bs1 bs2)
+       (blocks-subset? bs2 bs1)))
+
+;; blocks-intersect : BSet BSet -> BSet
+;; Return the set of blocks that appear in both sets.
+(define (blocks-intersect bs1 bs2)
+  (filter (λ (b) (blocks-contains? bs2 b)) bs1))
+
+;; blocks-count : BSet -> Nat
+;; Return the number of blocks in the set.
+(define (blocks-count bs)
+  (length bs))  ;; No duplicates, cardinality = length.
+
+;; blocks-move : Number Number BSet -> BSet
+;; Move each block by the given X & Y displacement.
+(define (blocks-move dx dy bs)
+  (map (λ (b) (block-move dx dy b)) bs))
+
+;; blocks-rotate-ccw : Posn BSet -> BSet
+;; Rotate the blocks 90 counterclockwise around the posn.
+(define (blocks-rotate-ccw c bs)
+  (map (λ (b) (block-rotate-ccw c b)) bs))
+
+;; blocks-rotate-cw : Posn BSet -> BSet
+;; Rotate the blocks 90 clockwise around the posn.
+(define (blocks-rotate-cw c bs)
+  (map (λ (b) (block-rotate-cw c b)) bs))
+
+;; blocks-change-color : BSet Color -> BSet
+(define (blocks-change-color bs c)
+  (map (λ (b) (block (block-x b) (block-y b) c))
+       bs))
+
+;; blocks-row : BSet Number -> BSet
+;; Return the set of blocks in the given row.
+(define (blocks-row bs i)
+  (filter (λ (b) (= i (block-y b))) bs))
+
+;; full-row? : BSet Nat -> Boolean
+;; Are there a full row of blocks at the given row in the set.
+(define (full-row? bs i)
+  (= board-width (blocks-count (blocks-row bs i))))
+
+;; blocks-overflow? : BSet -> Boolean
+;; Have any/c of the blocks reach over the top of the board?
+(define (blocks-overflow? bs)
+  (ormap (λ (b) (<= (block-y b) 0)) bs))
+
+;; blocks-union : BSet BSet -> BSet
+;; Union the two sets of blocks.
+(define (blocks-union bs1 bs2)
+  (foldr (λ (b bs)
+           (cond [(blocks-contains? bs b) bs]
+                 [else (cons b bs)]))
+         bs2
+         bs1))
+
+;; blocks-max-y : BSet -> Number
+;; Compute the maximum y coordinate;
+;; if set is empty, return 0, the coord of the board's top edge.
+(define (blocks-max-y bs)
+  (foldr (λ (b n) (max (block-y b) n)) 0 bs))
+
+;; blocks-min-x : BSet -> Number
+;; Compute the minimum x coordinate;
+;; if set is empty, return the coord of the board's right edge.
+(define (blocks-min-x bs)
+  (foldr (λ (b n) (min (block-x b) n)) board-width bs))
+
+;; blocks-max-x : BSet -> Number
+;; Compute the maximum x coordinate;
+;; if set is empty, return 0, the coord of the board's left edge.
+(define (blocks-max-x bs)
+  (foldr (λ (b n) (max (block-x b) n)) 0 bs))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; elim
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define (eliminate-full-rows bs)
+  (elim-row bs board-height 0))
+
+(define (elim-row bs i offset)
+  (cond [(< i 0) empty]
+        [(full-row? bs i)   (elim-row bs (sub1 i) (add1 offset))]
+        [else (blocks-union (elim-row bs (sub1 i) offset)
+                            (blocks-move 0 offset (blocks-row bs i)))]))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; tetras
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; tetra-move : Number Number Tetra -> Tetra
+;; Move the Tetra by the given X & Y displacement.
+(define (tetra-move dx dy t)
+  (tetra (posn (+ dx (posn-x (tetra-center t)))
+               (+ dy (posn-y (tetra-center t))))
+         (blocks-move dx dy (tetra-blocks t))))
+
+;; tetra-rotate-ccw : Tetra -> Tetra
+;; Rotate the tetra 90 degrees counterclockwise around its center.
+(define (tetra-rotate-ccw t)
+  (tetra (tetra-center t)
+         (blocks-rotate-ccw (tetra-center t)
+                            (tetra-blocks t))))
+
+;; tetra-rotate-cw : Tetra -> Tetra
+;; Rotate the tetra 90 degrees clockwise around its center.
+(define (tetra-rotate-cw t)
+  (tetra (tetra-center t)
+         (blocks-rotate-cw (tetra-center t)
+                           (tetra-blocks t))))
+
+;; tetra-overlaps-blocks? : Tetra BSet -> Boolean
+;; Is the tetra on any/c of the blocks?
+(define (tetra-overlaps-blocks? t bs)
+  (false? (false? (blocks-intersect (tetra-blocks t) bs))))
+
+;; tetra-change-color : Tetra Color -> Tetra
+;; Change the color of the given tetra.
+(define (tetra-change-color t c)
+  (tetra (tetra-center t)
+         (blocks-change-color (tetra-blocks t) c)))
+
+(define (build-tetra-blocks color xc yc x1 y1 x2 y2 x3 y3 x4 y4)
+  (tetra-move 3 0 
+              (tetra (posn xc yc)
+                     (list (block x1 y1 color)
+                           (block x2 y2 color)
+                           (block x3 y3 color)
+                           (block x4 y4 color)))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; world
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; touchdown : World (Listof Tetra) -> World
+;; Add the current tetra's blocks onto the world's block list,
+;; and create a new tetra.
+(define (touchdown w tetras)
+  (world (list-pick-random tetras)
+         (eliminate-full-rows (blocks-union (tetra-blocks (world-tetra w))
+                                            (world-blocks w)))))
+
+;; world-jump-down : World -> World
+;; Take the current tetra and move it down until it lands.
+(define (world-jump-down w)
+  (cond [(landed? w) w]
+        [else (world-jump-down (world (tetra-move 0 1 (world-tetra w))
+                                      (world-blocks w)))]))
+
+;; landed-on-blocks? : World -> Boolean
+;; Has the current tetra landed on blocks?
+;; I.e., if we move the tetra down 1, will it touch any/c existing blocks?
+(define (landed-on-blocks? w)
+  (tetra-overlaps-blocks? (tetra-move 0 1 (world-tetra w))
+                          (world-blocks w)))
+
+;; landed-on-floor? : World -> Boolean
+;; Has the current tetra landed on the floor?
+(define (landed-on-floor? w)
+  (= (blocks-max-y (tetra-blocks (world-tetra w)))
+     (sub1 board-height)))
+
+;; landed? : World -> Boolean
+;; Has the current tetra landed?
+(define (landed? w)
+  (or (landed-on-blocks? w)
+      (landed-on-floor? w)))
+
+;; next-world : World (NeListof Tetra) -> World
+;; Step the world, either touchdown or move the tetra down on step.
+(define (next-world w tetras)
+  (cond [(landed? w) (touchdown w tetras)]
+        [else (world (tetra-move 0 1 (world-tetra w))
+                     (world-blocks w))]))
+
+;; try-new-tetra : World Tetra -> World
+;; Make a world with the new tetra *IF* if doesn't lie on top of some other
+;; block or lie off the board. Otherwise, no change.
+(define (try-new-tetra w new-tetra)
+  (cond [(or (<  (blocks-min-x (tetra-blocks new-tetra)) 0)
+             (>= (blocks-max-x (tetra-blocks new-tetra)) board-width)
+             (tetra-overlaps-blocks? new-tetra (world-blocks w)))
+         w]
+        [else (world new-tetra (world-blocks w))]))
+
+;; world-move : Number Number World -> World
+;; Move the Tetra by the given X & Y displacement, but only if you can.
+;; Otherwise stay put.
+(define (world-move dx dy w)
+  (try-new-tetra w (tetra-move dx dy (world-tetra w))))
+
+;; world-rotate-ccw : World -> World
+;; Rotate the Tetra 90 degrees counterclockwise, but only if you can.
+;; Otherwise stay put.
+(define (world-rotate-ccw w)
+  (try-new-tetra w (tetra-rotate-ccw (world-tetra w))))
+
+;; world-rotate-cw : World -> World
+;; Rotate the Tetra 90 degrees clockwise, but only if you can.
+;; Otherwise stay put.
+(define (world-rotate-cw w)
+  (try-new-tetra w (tetra-rotate-cw (world-tetra w))))
+
+;; ghost-blocks : World -> BSet
+;; Gray blocks representing where the current tetra would land.
+(define (ghost-blocks w)
+  (tetra-blocks (tetra-change-color (world-tetra (world-jump-down w))
+                                    'gray)))
+
+;; world-key-move : World KeyEvent -> World
+;; Move the world according to the given key event.
+(define (world-key-move w k)
+  (cond [(equal? k "left") (world-move neg-1 0 w)]
+        [(equal? k "right") (world-move 1 0 w)]
+        [(equal? k "down") (world-jump-down w)]
+        [(equal? k "a") (world-rotate-ccw w)]
+        [(equal? k "s") (world-rotate-cw w)]
+        [else w]))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; image (dummy)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(struct image ())
+(define (overlay i₁ i₂) (image))
+(define (circle r m c) (image))
+(define (rectangle w h m c) (image))
+(define (place-image i₁ r c i₂) (image))
+(define (empty-scene w h) (image))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; aux (dummy) TODO
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define (list-pick-random xs) ;; last
+  (cond [(null? (cdr xs)) (car xs)]
+        [else (list-pick-random (cdr xs))]))
+(define neg-1 (random 10))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; visual
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; Visualize whirled peas
+;; World -> Scene
+(define (world->image w)
+  (place-image (blocks->image (append (tetra-blocks (world-tetra w))
+                                      (append (ghost-blocks w)
+                                              (world-blocks w))))
+               0 0 
+               (empty-scene (* board-width block-size)
+                            (* board-height block-size))))
+
+;; BSet -> Scene
+(define (blocks->image bs)
+  (foldr (λ (b img)
+           (cond [(<= 0 (block-y b)) (place-block b img)]
+                 [else img]))
+         (empty-scene (add1 (* board-width block-size)) 
+                      (add1 (* board-height block-size)))
+         bs))
+
+;; Visualizes a block.
+;; Block -> Image
+(define (block->image b)
+  (overlay 
+   (rectangle (add1 block-size) (add1 block-size) 'solid (block-color b))
+   (rectangle (add1 block-size) (add1 block-size) 'outline 'black)))
+
+;; Block Scene -> Scene
+(define (place-block b scene)
+  (place-image (block->image b)
+               (+ (* (block-x b) block-size) (/ block-size 2))
+               (+ (* (block-y b) block-size) (/ block-size 2))
+               scene))
+
+(define (world0 tetras)
+  (world (list-pick-random tetras) null))
+
+(provide
+ (contract-out
+  ;; data
+  ; ignored for benchmarking [struct block ([x real?] [y real?] [color COLOR/C])]
+  ; ignored for benchmarking [struct posn ([x real?] [y real?])]
+  ; ignored for benchmarking [struct tetra ([center POSN/C] [blocks BSET/C])]
+  ; ignored for benchmarking [struct world ([tetra TETRA/C] [blocks BSET/C])]
+  [posn=? (-> POSN/C POSN/C boolean?/c)]
+  [COLOR/C any/c]
+  [POSN/C any/c]
+  [BLOCK/C any/c]
+  [TETRA/C any/c]
+  [WORLD/C any/c]
+  [BSET/C any/c]
+  ;; consts
+  [block-size integer?]
+  [board-width integer?]
+  [board-height integer?]
+  ;; block
+  [block-rotate-ccw (-> POSN/C BLOCK/C BLOCK/C)]
+  [block-rotate-cw (-> POSN/C BLOCK/C BLOCK/C)]
+  [block=? (-> BLOCK/C BLOCK/C boolean?/c)]
+  [block-move (-> real?/c real?/c BLOCK/C  BLOCK/C)]
+  ;; bset
+  [blocks-contains? (-> BSET/C BLOCK/C boolean?/c)]
+  [blocks=? (-> BSET/C BSET/C  boolean?/c)]
+  [blocks-subset? (-> BSET/C BSET/C boolean?/c)]
+  [blocks-intersect (-> BSET/C BSET/C BSET/C)]
+  [blocks-count (-> BSET/C real?/c)]
+  [blocks-overflow? (-> BSET/C boolean?/c)]
+  [blocks-move (-> real?/c real?/c BSET/C BSET/C)]
+  [blocks-rotate-cw (-> POSN/C BSET/C BSET/C)]
+  [blocks-rotate-ccw (-> POSN/C BSET/C BSET/C)]
+  [blocks-change-color (-> BSET/C COLOR/C BSET/C)]
+  [blocks-row (-> BSET/C real?/c BSET/C)]
+  [full-row? (-> BSET/C real?/c boolean?/c)]
+  [blocks-union (-> BSET/C BSET/C BSET/C)]
+  [blocks-max-x (-> BSET/C real?/c)]
+  [blocks-min-x (-> BSET/C real?/c)]
+  [blocks-max-y (-> BSET/C real?/c)]
+  ;; elim
+  [eliminate-full-rows (-> BSET/C BSET/C)]
+  ;; tetras
+  [tetra-move (-> integer?/c integer?/c TETRA/C TETRA/C)]
+  [tetra-rotate-ccw (-> TETRA/C TETRA/C)]
+  [tetra-rotate-cw (-> TETRA/C TETRA/C)]
+  [tetra-overlaps-blocks? (-> TETRA/C BSET/C boolean?/c)]
+  [build-tetra-blocks (-> COLOR/C real?/c real?/c integer?/c integer?/c integer?/c integer?/c integer?/c integer?/c integer?/c integer?/c TETRA/C)]
+  [tetra-change-color (-> TETRA/C COLOR/C TETRA/C)]
+  ;; world
+  [world-key-move (-> WORLD/C string?/c WORLD/C)]
+  [next-world (-> WORLD/C (and/c cons?/c (listof TETRA/C)) WORLD/C)]
+  [ghost-blocks (-> WORLD/C BSET/C)]
+  ;; image
+  [image? (-> any/c boolean?/c)]
+  [overlay (-> image? image? image?)]
+  [circle (-> real?/c real?/c string?/c image?)]
+  [rectangle (-> real?/c real?/c COLOR/C COLOR/C image?)]
+  [place-image (-> image?/c real?/c real?/c image?/c image?/c)]
+  [empty-scene (-> real?/c real?/c image?)]
+  ;; aux
+  [list-pick-random (-> (and/c cons?/c (listof TETRA/C)) TETRA/C)]
+  [neg-1 integer?/c] ;; ha!
+  ;; visual
+  [world->image (-> WORLD/C image?/c)]
+  [blocks->image (-> BSET/C image?/c)]
+  [block->image (-> BLOCK/C image?/c)]
+  [place-block (-> BLOCK/C image?/c image?/c)]
+  [world0 (-> (and/c cons?/c (listof TETRA/C)) WORLD/C)]
+  ))
diff --git a/analyses/simpleactor/benchmarks-in/games_zombie.rkt b/analyses/simpleactor/benchmarks-in/games_zombie.rkt
new file mode 100644
index 0000000..829e68d
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/games_zombie.rkt
@@ -0,0 +1,271 @@
+#lang racket
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; image (dummy)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(struct image ())
+(define (empty-scene w h) (image))
+(define (place-image i₁ r c i₂) (image))
+(define (circle r m c) (image))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; math
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define (min x y) (if (<= x y) x y))
+(define (max x y) (if (>= x y) x y))
+(define (abs x) (if (>= x 0) x (- 0 x)))
+(define (sqr x) (* x x))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;; zombie
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define WIDTH 400)
+(define HEIGHT 400)
+(define MT-SCENE (empty-scene WIDTH HEIGHT))
+(define PLAYER-SPEED 4)
+(define ZOMBIE-SPEED 2)
+(define ZOMBIE-RADIUS 20)
+(define PLAYER-RADIUS 20)
+(define PLAYER-IMG (circle PLAYER-RADIUS "solid" "green"))
+
+(define posn/c
+  (->d (one-of/c 'x 'y 'posn 'move-toward/speed 'draw-on/image 'dist)
+       (lambda (msg)
+            (cond
+              [(equal? msg 'x) (-> real?)]
+              [(equal? msg 'y) (-> real?)]
+              [(equal? msg 'posn) (-> posn/c)]
+              [(equal? msg 'move-toward/speed) (-> posn/c real? posn/c)]
+              [(equal? msg 'draw-on/image) (-> image? image? image?)]
+              [(equal? msg 'dist) (-> posn/c real?)]
+              [else "error"]))))
+
+(define player/c
+  (->d (one-of/c 'posn 'move-toward 'draw-on)
+       (lambda (msg)
+            (cond
+              [(equal? msg 'posn) (-> posn/c)]
+              [(equal? msg 'move-toward) (-> posn/c player/c)]
+              [(equal? msg 'draw-on) (-> image? image?)]
+              [else "error"]))))
+
+(define zombie/c
+  (->d (one-of/c 'posn 'draw-on/color 'touching? 'move-toward)
+       (lambda (msg)
+            (cond
+              [(equal? msg 'posn) (-> posn/c)]
+              [(equal? msg 'draw-on/color) (-> string? image? image?)]
+              [(equal? msg 'touching?) (-> posn/c boolean?)]
+              [(equal? msg 'move-toward) (-> posn/c zombie/c)]
+              [else "error"]))))
+
+(define horde/c
+  (->d (one-of/c 'dead 'undead 'draw-on 'touching? 'move-toward 'eat-brains)
+       (lambda (msg)
+            (cond
+              [(equal? msg 'dead) (-> zombies/c)]
+              [(equal? msg 'undead) (-> zombies/c)]
+              [(equal? msg 'draw-on) (-> image? image?)]
+              [(equal? msg 'touching?) (-> posn/c boolean?)]
+              [(equal? msg 'move-toward) (-> posn/c horde/c)]
+              [(equal? msg 'eat-brains) (-> horde/c)]
+              [else "error"]))))
+
+(define zombies/c
+  (->d (one-of/c 'move-toward 'draw-on/color 'touching? 'kill-all)
+       (lambda (msg)
+            (cond
+              [(equal? msg 'move-toward) (-> posn/c zombies/c)]
+              [(equal? msg 'draw-on/color) (-> string? image? image?)]
+              [(equal? msg 'touching?) (-> posn/c  boolean?)]
+              [(equal? msg 'kill-all) (-> zombies/c horde/c)]
+              [else "error"]))))
+
+(define world/c
+  (->d (one-of/c 'on-mouse 'on-tick 'to-draw 'stop-when)
+       (lambda (msg)
+            (cond
+              [(equal? msg 'on-mouse) (-> real? real? string? world/c)]
+              [(equal? msg 'on-tick) (-> world/c)]
+              [(equal? msg 'to-draw) (-> image?)]
+              [(equal? msg 'stop-when) (-> boolean?)]
+              [else "error"]))))
+
+(define (new-world player mouse zombies)
+  (λ (msg)
+    (cond
+      [(equal? msg 'on-mouse)
+       (λ (x y me)
+         (new-world player
+                    (if (equal? me "leave") ((player 'posn)) (new-posn x y))
+                    zombies))]
+      [(equal? msg 'on-tick)
+       (λ ()
+         (new-world ((player 'move-toward) mouse)
+                    mouse
+                    ((((zombies 'eat-brains)) 'move-toward) ((player 'posn)))))]
+      [(equal? msg 'to-draw)
+       (λ ()
+         ((player 'draw-on) ((zombies 'draw-on) MT-SCENE)))]
+      [(equal? msg 'stop-when)
+       (λ ()
+         ((zombies 'touching?) ((player 'posn))))]
+      [else "unknown message"])))
+
+(define (new-player p)
+  (λ (msg)
+    (cond
+      [(equal? msg 'posn) (λ () p)]
+      [(equal? msg 'move-toward)
+       (λ (q)
+         (new-player ((p 'move-toward/speed) q PLAYER-SPEED)))]
+      [(equal? msg 'draw-on)
+       (λ (scn)
+         ((p 'draw-on/image) PLAYER-IMG scn))]
+      [else "unknown message"])))
+
+(define (new-horde undead dead)
+  (λ (msg)
+    (cond
+      [(equal? msg 'dead) (λ () dead)]
+      [(equal? msg 'undead) (λ () undead)]
+      [(equal? msg 'draw-on)
+       (λ (scn)
+         ((undead 'draw-on/color) "yellow" ((dead 'draw-on/color) "black" scn)))]
+      [(equal? msg 'touching?)
+       (λ (p)
+         (or ((undead 'touching?) p) ((dead 'touching?) p)))]
+      [(equal? msg 'move-toward)
+       (λ (p)
+         (new-horde ((undead 'move-toward) p) dead))]
+      [(equal? msg 'eat-brains) (λ () ((undead 'kill-all) dead))]
+      [else "unknown message"])))
+
+(define (new-cons-zombies z r)
+  (λ (msg)
+    (cond
+      [(equal? msg 'move-toward)
+       (λ (p)
+         (new-cons-zombies ((z 'move-toward) p) ((r 'move-toward) p)))]
+      [(equal? msg 'draw-on/color)
+       (λ (c s)
+         ((z 'draw-on/color) c ((r 'draw-on/color) c s)))]
+      [(equal? msg 'touching?)
+       (λ (p)
+         (or ((z 'touching?) p) ((r 'touching?) p)))]
+      [(equal? msg 'kill-all)
+       (λ (dead)
+         (cond
+           [(or ((r 'touching?) ((z 'posn)))
+                ((dead 'touching?) ((z 'posn))))
+            ((r 'kill-all) (new-cons-zombies z dead))]
+           [else (let ([res ((r 'kill-all) dead)])
+                   (new-horde
+                    (new-cons-zombies z ((res 'undead)))
+                    ((res 'dead))))]))]
+      [else "unknown message"])))
+
+(define (new-mt-zombies)
+  (λ (msg)
+    (cond
+      [(equal? msg 'move-toward) (λ (p) (new-mt-zombies))]
+      [(equal? msg 'draw-on/color) (λ (c s) s)]
+      [(equal? msg 'touching?) (λ (p) #f)]
+      [(equal? msg 'kill-all)
+       (λ (dead)
+         (new-horde (new-mt-zombies) dead))]
+      [else "unknown message"])))
+
+(define (new-zombie p)
+  (λ (msg)
+    (cond
+      [(equal? msg 'posn) (λ () p)]
+      [(equal? msg 'draw-on/color)
+       (λ (c s)
+         ((p 'draw-on/image)
+          (circle ZOMBIE-RADIUS "solid" c)
+          s))]
+      [(equal? msg 'touching?)
+       (λ (q)
+         (<= ((p 'dist) q) ZOMBIE-RADIUS))]
+      [(equal? msg 'move-toward)
+       (λ (q)
+         (new-zombie ((p 'move-toward/speed) q ZOMBIE-SPEED)))]
+      [else "unknown message"])))
+
+(define (new-posn x y)
+  (letrec ([this
+            (λ (msg)
+              (cond
+                [(equal? msg 'x) (λ () x)]
+                [(equal? msg 'y) (λ () y)]
+                [(equal? msg 'posn) (λ () this)]
+                [(equal? msg 'move-toward/speed)
+                 (λ (p speed)
+                   (let* ([δx (- ((p 'x)) x)]
+                          [δy (- ((p 'y)) y)]
+                          [move-distance (min speed (max (abs δx) (abs δy)))])
+                     (cond
+                       [(< (abs δx) (abs δy))
+                        ((this 'move)
+                         0
+                         (if (positive? δy) move-distance (- 0 move-distance)))]
+                       [else
+                        ((this 'move)
+                         (if (positive? δx) move-distance (- 0 move-distance))
+                         0)])))]
+                [(equal? msg 'move)
+                 (λ (δx δy)
+                   (new-posn (+ x δx) (+ y δy)))]
+                [(equal? msg 'draw-on/image)
+                 (λ (img scn)
+                   (place-image img x y scn))]
+                [(equal? msg 'dist)
+                 (λ (p)
+                   (sqrt (+ (sqr (- ((p 'y)) y))
+                            (sqr (- ((p 'x)) x)))))]
+                [else "unknown message"]))])
+    this))
+
+(define w0
+  (new-world
+   (new-player (new-posn 0 0))
+   (new-posn 0 0)
+   (new-horde
+    (new-cons-zombies
+     (new-zombie (new-posn 100 300))
+     (new-cons-zombies
+      (new-zombie (new-posn 100 200))
+      (new-mt-zombies)))
+    (new-cons-zombies
+     (new-zombie (new-posn 200 200))
+     (new-mt-zombies)))))
+
+(provide
+ (contract-out
+  ;; image
+  [image? (-> any/c  boolean?/c)]
+  [empty-scene (-> real?/c real?/c image?)]
+  [place-image (-> image?/c real?/c real?/c image? image?)]
+  [circle (-> real?/c string?/c string?/c image?)]
+  ;; zombie
+  ;[posn/c contract?]
+  ;[player/c contract?]
+  ;[zombie/c contract?]
+  ;[zombies/c contract?]
+  ;[horde/c contract?]
+  ;[world/c contract?]
+  [new-world (-> player/c posn/c horde/c world/c)]
+  [new-player (-> posn/c  player/c)]
+  [new-horde (-> zombies/c zombies/c horde/c)]
+  [new-cons-zombies (-> zombie/c zombies/c zombies/c)]
+  [new-mt-zombies (-> zombies/c)]
+  [new-zombie (-> posn/c zombie/c)]
+  [new-posn (-> real?/c real?/c  posn/c)]
+  [w0 world/c]))
+
diff --git a/analyses/simpleactor/benchmarks-in/mochi_fold-div.rkt b/analyses/simpleactor/benchmarks-in/mochi_fold-div.rkt
new file mode 100644
index 0000000..cc446e5
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_fold-div.rkt
@@ -0,0 +1,17 @@
+#lang racket
+
+
+(define (foldl f z l)
+  (if (empty? l) z (foldl f (f z (car l)) (cdr l))))
+
+(define (randpos rand)
+  (let ([n (rand)]) (if (> n 0) n (randpos rand))))
+
+(define (mk-list rand n)
+  (if (<= n 0) empty
+      (cons (randpos rand) (mk-list rand (- n 1)))))
+
+(define (main rand n m) (foldl / m (mk-list rand n)))
+
+(provide (contract-out
+ [main (-> (-> integer?/c) integer?/c integer?/c real?/c)]))
diff --git a/analyses/simpleactor/benchmarks-in/mochi_hors.rkt b/analyses/simpleactor/benchmarks-in/mochi_hors.rkt
new file mode 100644
index 0000000..f69bff3
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_hors.rkt
@@ -0,0 +1,15 @@
+#lang racket
+
+(define (c _) 'unit)
+(define (b x _) (x 1))
+(define (a x y q) (if (= q 0)
+                      (begin (x 0) (y 0))
+                      (error 'invalid)))
+(define (f n x q)
+  (if (<= n 0) (x q)
+      (a x (λ (p) (f (- n 1) (λ (_) (b x _)) p)) q)))
+(define (s n q) (f n c q))
+
+(define (main n) (s n 0))
+
+(provide (contract-out [main (-> integer?/c any/c)]))
diff --git a/analyses/simpleactor/benchmarks-in/mochi_hrec.rkt b/analyses/simpleactor/benchmarks-in/mochi_hrec.rkt
new file mode 100644
index 0000000..33c9a22
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_hrec.rkt
@@ -0,0 +1,11 @@
+#lang racket
+
+(define (f g x)
+  (if (>= x 0) (g x) (f (λ (x) (f g x)) (g x))))
+
+(define (main n)
+  (f add1 n))
+
+(provide (contract-out
+  [f (-> (-> integer? integer?) integer? integer?)]
+  [main (-> integer? (and/c integer? (>=/c 0)))]))
diff --git a/analyses/simpleactor/benchmarks-in/mochi_l-zipunzip.rkt b/analyses/simpleactor/benchmarks-in/mochi_l-zipunzip.rkt
new file mode 100644
index 0000000..480e688
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_l-zipunzip.rkt
@@ -0,0 +1,20 @@
+#lang racket
+
+(define (f g) (λ (x y) (g (+ x 1) (+ y 1))))
+
+(define (unzip x k)
+  (if (= x 0) (k 0 0)
+      (unzip (- x 1) (f k))))
+
+(define (zip x y)
+  (if (= x 0)
+      (if (= y 0) 0 'fail)
+      (if (= y 0) 'fail
+	  (+ 1 (zip (- x 1) (- y 1))))))
+
+(define (main n)
+  (unzip n zip))
+
+(provide (contract-out
+ [f (-> (-> integer?/c integer?/c integer?/c) (-> integer?/c integer?/c integer?/c))]
+ [main (-> integer?/c integer?/c)]))
diff --git a/analyses/simpleactor/benchmarks-in/mochi_map-foldr.rkt b/analyses/simpleactor/benchmarks-in/mochi_map-foldr.rkt
new file mode 100644
index 0000000..4c1cc2c
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_map-foldr.rkt
@@ -0,0 +1,12 @@
+#lang racket
+
+(define (foldr f z xs)
+  (if (empty? xs) z
+      (f (car xs) (foldr f z (cdr xs)))))
+
+(define (map f xs)
+  (foldr (λ (x ys) (cons (f x) ys)) empty xs))
+
+(provide (contract-out
+ [foldr (-> (-> any/c any/c any/c) any/c (listof any/c) any/c)]
+ [map (-> (-> any/c any/c) (listof any/c) (listof any/c))]))
diff --git a/analyses/simpleactor/benchmarks-in/mochi_mappend.rkt b/analyses/simpleactor/benchmarks-in/mochi_mappend.rkt
new file mode 100644
index 0000000..6aef746
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_mappend.rkt
@@ -0,0 +1,13 @@
+#lang racket
+
+(define (mappend xs ys)
+  (if (empty? xs) ys
+      (cons (car xs) (mappend (cdr xs) ys))))
+
+(define (map-append f xs)
+  (if (empty? xs) empty
+      (mappend (f (car xs)) (map-append f (cdr xs)))))
+
+(provide (contract-out 
+ [map-append (-> (-> any/c (listof any/c)) (listof any/c) (listof any/c))]
+ [mappend (-> (listof any/c) (listof any/c) (listof any/c))]))
diff --git a/analyses/simpleactor/benchmarks-in/mochi_mem.rkt b/analyses/simpleactor/benchmarks-in/mochi_mem.rkt
new file mode 100644
index 0000000..2562075
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_mem.rkt
@@ -0,0 +1,14 @@
+#lang racket
+
+(define (mk-list n x)
+  (if (< n 0) empty (cons x (mk-list (- n 1) x))))
+
+(define (mem x xs)
+  (if (empty? xs) #f (or (= x (car xs)) (mem x (cdr xs)))))
+
+(provide (contract-out
+   [mk-list (->d integer?/c integer?/c 
+                 (lambda (_ x) 
+                   (and/c (listof integer?/c)
+                          (flat (lambda (l) (or (empty? l) (member x l)))))))]
+   [mem (-> integer?/c (listof integer?/c) boolean?/c)]))
diff --git a/analyses/simpleactor/benchmarks-in/mochi_mult.rkt b/analyses/simpleactor/benchmarks-in/mochi_mult.rkt
new file mode 100644
index 0000000..39e2971
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_mult.rkt
@@ -0,0 +1,10 @@
+#lang racket
+
+(define (mult n m)
+  (if (or (<= n 0) (<= m 0)) 0
+      (+ n (mult n (- m 1)))))
+
+(define (sqr n) (mult n n))
+
+(provide (contract-out [mult (-> integer?/c integer?/c (and/c integer?/c (>=/c 0)))]
+		       [sqr (->d integer?/c (lambda (n) (and/c integer?/c (>=/c n))))]))
diff --git a/analyses/simpleactor/benchmarks-in/mochi_neg.rkt b/analyses/simpleactor/benchmarks-in/mochi_neg.rkt
new file mode 100644
index 0000000..e4546e7
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_neg.rkt
@@ -0,0 +1,15 @@
+#lang racket
+
+(define (g x) (λ (_) x))
+
+(define (twice f x y) ((f (f x)) y))
+
+(define (neg x) (λ (_) (- 0 (x #f))))
+
+(define (main n)
+  (if (>= n 0)
+      (twice neg (g n) 'unit)
+      42))
+
+(provide (contract-out
+ [main (-> integer?/c (and/c integer?/c (>=/c 0)))]))
diff --git a/analyses/simpleactor/benchmarks-in/mochi_nth0.rkt b/analyses/simpleactor/benchmarks-in/mochi_nth0.rkt
new file mode 100644
index 0000000..26defa1
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_nth0.rkt
@@ -0,0 +1,15 @@
+#lang racket
+
+(define (nth n xs)
+  (if (= n 0) (car xs) (nth (- n 1) (cdr xs))))
+
+(define (mk-list n)
+  (if (< n 0) empty
+      (cons n (mk-list (- n 1)))))
+
+(define (main n)
+  (let ([xs (mk-list n)])
+    (if (empty? xs) 0 (nth 0 xs))))
+
+(provide (contract-out
+ [main (-> integer?/c integer?/c)]))
diff --git a/analyses/simpleactor/benchmarks-in/mochi_r-file.rkt b/analyses/simpleactor/benchmarks-in/mochi_r-file.rkt
new file mode 100644
index 0000000..dbb54b2
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_r-file.rkt
@@ -0,0 +1,36 @@
+#lang racket
+
+(define STATE/C (one-of/c 'init 'opened 'closed 'ignore))
+
+(define (loop) (loop))
+
+(define (readit st)
+  (if (equal? 'opened st) 'opened 'ignore))
+
+(define (read_ x st)
+  (if x (readit st) st))
+
+(define (closeit st)
+  (cond
+    [(equal? 'opened st) 'closed]
+    [(equal? 'ignore st) 'ignore]
+    [else (loop) 0]))
+
+(define (close_ x st)
+  (if x (closeit st) st))
+
+(define (f x y st)
+  (close_ y (close_ x st))
+  (f x y (read_ y (read_ x st))))
+
+(define (next st) (if (equal? 'init st) 'opened 'ignore))
+
+(define (g b3 x st)
+  (if (> b3 0) (f x #t (next st)) (f x #f st)))
+
+(define (main b2 b3)
+  (if (> b2 0) (g b3 #t 'opened) (g b3 #f 'init))
+  'unit)
+
+(provide (contract-out
+ [main (-> integer?/c integer?/c any/c)]))
diff --git a/analyses/simpleactor/benchmarks-in/mochi_r-lock.rkt b/analyses/simpleactor/benchmarks-in/mochi_r-lock.rkt
new file mode 100644
index 0000000..9050a1f
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_r-lock.rkt
@@ -0,0 +1,10 @@
+#lang racket
+
+(define (lock st) 1)
+(define (unlock st) 0)
+(define (f n st) (if (> n 0) (lock st) st))
+(define (g n st) (if (> n 0) (unlock st) st))
+(define (main n) (g n (f n 0)))
+
+(provide (contract-out
+ [main (-> integer?/c (one-of/c 0))]))
diff --git a/analyses/simpleactor/benchmarks-in/mochi_reverse.rkt b/analyses/simpleactor/benchmarks-in/mochi_reverse.rkt
new file mode 100644
index 0000000..fcadb08
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_reverse.rkt
@@ -0,0 +1,13 @@
+#lang racket
+
+(define (main len)
+  (let ([xs (mk-list len)])
+    (if (not (= len 0)) (car (reverse xs empty)) 0)))
+
+(define (reverse l ac)
+  (if (empty? l) ac (reverse (cdr l) (cons (car l) ac))))
+
+(define (mk-list n)
+  (if (= n 0) empty (cons n (mk-list (- n 1)))))
+
+(provide (contract-out [main (-> integer?/c integer?/c)]))
diff --git a/analyses/simpleactor/benchmarks-in/mochi_sum.rkt b/analyses/simpleactor/benchmarks-in/mochi_sum.rkt
new file mode 100644
index 0000000..d54a722
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_sum.rkt
@@ -0,0 +1,9 @@
+#lang racket
+
+(define (sum n)
+  (if (<= n 0) 0
+      (+ n (sum (- n 1)))))
+
+(provide (contract-out
+           [sum (->d integer?/c
+	         (lambda (n) (and/c integer?/c (>=/c n))))]))
diff --git a/analyses/simpleactor/benchmarks-in/mochi_zip.rkt b/analyses/simpleactor/benchmarks-in/mochi_zip.rkt
new file mode 100644
index 0000000..46cc552
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/mochi_zip.rkt
@@ -0,0 +1,17 @@
+#lang racket
+
+(define (zip xs ys) ; zip itself is unsafe
+  (cond
+   [(and (empty? xs) (empty? ys)) empty]
+   [(and (cons? xs) (cons? ys)) (cons (cons (car xs) (car ys)) (zip (cdr xs) (cdr ys)))]
+   [else 'fail]))
+
+(define (mk-list n)
+  (if (< n 0) empty (cons n (mk-list (- n 1)))))
+
+(define (main n)
+  (let ([xs (mk-list n)]) (zip xs xs)))
+
+(provide (contract-out
+ [mk-list (-> integer?/c (listof integer?/c))]
+ [main (-> integer?/c (listof (cons/c integer?/c integer?/c)))]))
diff --git a/analyses/simpleactor/benchmarks-in/sergey_blur.rkt b/analyses/simpleactor/benchmarks-in/sergey_blur.rkt
new file mode 100644
index 0000000..f441573
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/sergey_blur.rkt
@@ -0,0 +1,15 @@
+#lang racket
+; https://github.com/dvanhorn/oaam/blob/master/benchmarks/sergey/blur.sch
+
+(define id (λ (x) x))
+(define blur (λ (y) y))
+(define lp
+  (λ (a)
+    (λ (n)
+      (if (zero? n)
+	  (id a)
+	  (let* ([r ((blur id) #t)]
+		 [s ((blur id) #f)])
+	    (not (((blur lp) s) (sub1 n))))))))
+
+((lp #f) 2)
diff --git a/analyses/simpleactor/benchmarks-in/sergey_eta.rkt b/analyses/simpleactor/benchmarks-in/sergey_eta.rkt
new file mode 100644
index 0000000..be97c87
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/sergey_eta.rkt
@@ -0,0 +1,12 @@
+#lang racket
+; https://github.com/dvanhorn/oaam/blob/master/benchmarks/sergey/eta.sch
+
+(define (do-something)
+  10)
+
+(define (id y)
+  (do-something)
+  y)
+
+((id (λ (a) a)) #t)
+((id (λ (b) b)) #f)
diff --git a/analyses/simpleactor/benchmarks-in/sergey_kcfa2.rkt b/analyses/simpleactor/benchmarks-in/sergey_kcfa2.rkt
new file mode 100644
index 0000000..b0b0b53
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/sergey_kcfa2.rkt
@@ -0,0 +1,12 @@
+#lang racket
+; https://github.com/dvanhorn/oaam/blob/master/benchmarks/sergey/kcfa2.sch
+
+((λ (f1)
+   (let ((a (f1 #t)))
+     (f1 #f)))
+ (λ (x1)
+   ((λ (f2)
+      (let ((b (f2 #t)))
+	(let ((c (f2 #f)))
+	  (f2 #t))))
+    (λ (x2) ((λ (z) (z x1 x2)) (λ (y1 y2) y1))))))
diff --git a/analyses/simpleactor/benchmarks-in/sergey_kcfa3.rkt b/analyses/simpleactor/benchmarks-in/sergey_kcfa3.rkt
new file mode 100644
index 0000000..59450ed
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/sergey_kcfa3.rkt
@@ -0,0 +1,18 @@
+#lang racket
+; https://github.com/dvanhorn/oaam/blob/master/benchmarks/sergey/kcfa3.sch
+
+
+((λ (f1)
+   (let ((a (f1 #t)))
+     (f1 #f)))
+ (λ (x1)
+   ((λ (f2)
+      (let ((b (f2 #t)))
+	(f2 #f)))
+    (λ (x2)
+      ((λ (f3)
+	 (let ((c (f3 #t)))
+	   (f3 #f)))
+       (λ (x3)
+	 ((λ (z) (z x1 x2 x3))
+	  (λ (y1 y2 y3) y1))))))))
diff --git a/analyses/simpleactor/benchmarks-in/sergey_loop2.rkt b/analyses/simpleactor/benchmarks-in/sergey_loop2.rkt
new file mode 100644
index 0000000..79efc00
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/sergey_loop2.rkt
@@ -0,0 +1,20 @@
+#lang racket
+; https://github.com/dvanhorn/oaam/blob/master/benchmarks/sergey/loop2.sch
+
+(let ([lp1 2000])
+  (let ([a
+         (set! lp1 (λ (i x)
+                     (let ([a (= 0 i)])
+                       (if
+                        a
+                        x
+                        (let ([lp2 1000]) ;; FIXME should '(unspecified)
+                          (let ([b
+                                 (set! lp2 (λ (j f y)
+                                             (let ([b (= 0 j)])
+                                               (if b
+                                                   (lp1 (- i 1) y)
+                                                   (let ([$tmp$3 (f y)])
+                                                     (lp2 (- j 1) f $tmp$3))))))])
+                            (lp2 10 (λ (n) (+ n i )) x)))))))])
+    (lp1 10 0)))
diff --git a/analyses/simpleactor/benchmarks-in/sergey_mj09.rkt b/analyses/simpleactor/benchmarks-in/sergey_mj09.rkt
new file mode 100644
index 0000000..ee7967c
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/sergey_mj09.rkt
@@ -0,0 +1,14 @@
+#lang racket
+; https://github.com/dvanhorn/oaam/blob/master/benchmarks/sergey/mj09.sch
+
+(let ([h (λ (b)
+	   (let ([g (λ (z) z)])
+	     (let ([f (λ (k)
+			(if b
+			    (k 1)
+			    (k 2)))])
+	       (let ([y (f (λ (x) x))])
+		 (g y)))))])
+  (let* ([x (h #t)]
+	 [y (h #f)])
+    y))
diff --git a/analyses/simpleactor/benchmarks-in/sergey_sat.rkt b/analyses/simpleactor/benchmarks-in/sergey_sat.rkt
new file mode 100644
index 0000000..f270662
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/sergey_sat.rkt
@@ -0,0 +1,33 @@
+#lang racket
+; https://github.com/dvanhorn/oaam/blob/master/benchmarks/sergey/sat.sch
+
+(define phi
+  (λ (x1)
+    (λ (x2)
+      (λ (x3)
+        (λ (x4)
+          (λ (x5)
+            (λ (x6)
+              (λ (x7)
+                (and (or x1 x2)
+                     (or x1 (not x2) (not x3))
+                     (or x3 x4)
+                     (or (not x4) x1)
+                     (or (not x2) (not x3))
+                     (or x4 x2))))))))))
+
+(define try
+  (λ (f) (or (f #t) (f #f))))
+
+(define sat-solve-7
+  (λ (p)
+    (try (λ (n1)
+           (try (λ (n2)
+                  (try (λ (n3)
+                         (try (λ (n4)
+                                (try (λ (n5)
+                                       (try (λ (n6)
+                                              (try (λ (n7)
+                                                     (((((((p n1) n2) n3) n4) n5) n6) n7)))))))))))))))))
+
+(sat-solve-7 phi)
diff --git a/analyses/simpleactor/benchmarks-in/softy_append.rkt b/analyses/simpleactor/benchmarks-in/softy_append.rkt
new file mode 100644
index 0000000..9acf9ca
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/softy_append.rkt
@@ -0,0 +1,8 @@
+#lang racket
+
+(define (append xs ys)
+  (if (empty? xs) ys
+      (cons (car xs) (append (cdr xs) ys))))
+
+(provide (contract-out
+   [append (-> (listof any/c) (listof any/c) (listof any/c))]))
diff --git a/analyses/simpleactor/benchmarks-in/softy_cpstak.rkt b/analyses/simpleactor/benchmarks-in/softy_cpstak.rkt
new file mode 100644
index 0000000..1f2f608
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/softy_cpstak.rkt
@@ -0,0 +1,24 @@
+#lang racket
+
+(define (tak x y z k)
+  (if (not (< y x))
+      (k z)
+      (tak (- x 1)
+	   y
+	   z
+	   (lambda (v1)
+	     (tak (- y 1)
+		  z
+		  x
+		  (lambda (v2)
+		    (tak (- z 1)
+			 x
+			 y
+			 (lambda (v3)
+			   (tak v1 v2 v3 k)))))))))
+
+(define (tak-main x y z)
+  (tak x y z (λ (x) x)))
+
+(provide (contract-out
+ [tak-main (-> integer?/c integer?/c integer?/c integer?/c)]))
diff --git a/analyses/simpleactor/benchmarks-in/softy_last-pair.rkt b/analyses/simpleactor/benchmarks-in/softy_last-pair.rkt
new file mode 100644
index 0000000..577b186
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/softy_last-pair.rkt
@@ -0,0 +1,7 @@
+#lang racket
+
+(define (lastpair x)
+  (if (pair? (cdr x)) (lastpair (cdr x)) x))
+
+(provide (contract-out 
+   [lastpair (-> pair? pair?)]))
diff --git a/analyses/simpleactor/benchmarks-in/softy_last.rkt b/analyses/simpleactor/benchmarks-in/softy_last.rkt
new file mode 100644
index 0000000..64d480d
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/softy_last.rkt
@@ -0,0 +1,17 @@
+#lang racket
+
+(define (Y f)
+  (λ (y)
+     (((λ (x) (f (λ (z) ((x x) z))))
+       (λ (x) (f (λ (z) ((x x) z)))))
+      y)))
+
+(define (last l)
+  ((Y (λ (f)
+	 (λ (x)
+            (if (empty? (cdr x)) (car x) (f (cdr x))))))
+   l))
+
+
+(provide (contract-out
+ [last (-> (cons/c any/c (listof any/c)) any/c)]))
diff --git a/analyses/simpleactor/benchmarks-in/softy_length-acc.rkt b/analyses/simpleactor/benchmarks-in/softy_length-acc.rkt
new file mode 100644
index 0000000..241a4f5
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/softy_length-acc.rkt
@@ -0,0 +1,10 @@
+#lang racket
+
+(define (len xs)
+  (len-acc xs 0))
+(define (len-acc xs acc)
+  (if (empty? xs) acc
+      (len-acc (cdr xs) (+ 1 acc))))
+
+(provide (contract-out
+ [len (-> (listof any/c) (and/c integer?/c (>=/c 0)))]))
diff --git a/analyses/simpleactor/benchmarks-in/softy_length.rkt b/analyses/simpleactor/benchmarks-in/softy_length.rkt
new file mode 100644
index 0000000..341e4e4
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/softy_length.rkt
@@ -0,0 +1,8 @@
+#lang racket
+
+(define (len xs)
+  (if (empty? xs) 0
+      (+ 1 (len (cdr xs)))))
+
+(provide (contract-out 
+ [len (-> (listof any/c) (and/c integer?/c (>=/c 0)))]))
diff --git a/analyses/simpleactor/benchmarks-in/softy_member.rkt b/analyses/simpleactor/benchmarks-in/softy_member.rkt
new file mode 100644
index 0000000..39fedf4
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/softy_member.rkt
@@ -0,0 +1,8 @@
+#lang racket
+
+(define (member x l)
+  (if (empty? l) empty
+      (if (equal? x (car l)) l (member x (cdr l)))))
+
+(provide (contract-out
+ [member (-> (any/c (listof any/c)  (listof any/c)))]))
diff --git a/analyses/simpleactor/benchmarks-in/softy_recursive-div2.rkt b/analyses/simpleactor/benchmarks-in/softy_recursive-div2.rkt
new file mode 100644
index 0000000..0bcab02
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/softy_recursive-div2.rkt
@@ -0,0 +1,11 @@
+#lang racket
+
+(define (recursive-div2 l)
+  (if (empty? l) empty
+      (cons (car l) (recursive-div2 (cdr (cdr l))))))
+
+(define even-list/c
+  (flat (lambda () (or/c null? (cons/c any/c (cons/c any/c even-list/c))))))
+
+(provide (contract-out
+ [recursive-div2 (-> (even-list/c) (listof any/c))]))
diff --git a/analyses/simpleactor/benchmarks-in/softy_subst.rkt b/analyses/simpleactor/benchmarks-in/softy_subst.rkt
new file mode 100644
index 0000000..2987a15
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/softy_subst.rkt
@@ -0,0 +1,9 @@
+(define (subst* new old t)
+  (cond
+   ((equal? old t) new)
+   ((pair? t) (cons (subst* new old (car t))
+		    (subst* new old (cdr t))))
+   (else t)))
+
+(provide (contract-out
+  (subst* (-> any? any? any? any?))))
diff --git a/analyses/simpleactor/benchmarks-in/softy_tak.rkt b/analyses/simpleactor/benchmarks-in/softy_tak.rkt
new file mode 100644
index 0000000..6c6be52
--- /dev/null
+++ b/analyses/simpleactor/benchmarks-in/softy_tak.rkt
@@ -0,0 +1,12 @@
+;; OK
+
+(define (tak x y z)
+  (if (< y x) ;; original: (false? (< y x)), swapped consequent and alternative
+      (tak (tak (- x 1) y z)
+	   (tak (- y 1) z x)
+	   (tak (- z 1) x y))
+      z))
+
+(provide (contract-out
+ (tak (-> number?/c number?/c number?/c number?/c))))
+
diff --git a/analyses/simpleactor/primitive-contracts.rkt b/analyses/simpleactor/primitive-contracts.rkt
new file mode 100644
index 0000000..cd9b716
--- /dev/null
+++ b/analyses/simpleactor/primitive-contracts.rkt
@@ -0,0 +1,8 @@
+real?
+boolean?
+number?
+image?
+cons?
+integer?
+and/c
+pair?
diff --git a/analyses/simpleactor/scripts/copy_selected_benchmarks.py b/analyses/simpleactor/scripts/copy_selected_benchmarks.py
new file mode 100755
index 0000000..5e0920f
--- /dev/null
+++ b/analyses/simpleactor/scripts/copy_selected_benchmarks.py
@@ -0,0 +1,36 @@
+#!/usr/bin/env python
+
+from pathlib import Path
+import os
+import subprocess
+import sys
+import shutil
+
+if len(sys.argv) != 3:
+    print("Error: wrong number of arguments")
+    print("Usage: ")
+    print(f"{sys.argv[0]} PROGRAM_LIST_LOCATION BENCHMARK_LOCATION")
+    sys.exit(1)
+else:
+    PROGRAMS_LOCATION = sys.argv[1]
+    BENCHMARK_LOCATION = Path(sys.argv[2]).absolute()
+
+try:
+    PROGRAMS = open(PROGRAMS_LOCATION).readlines()
+    OUTPUT_DIR = (Path(__file__).parent.parent / "benchmarks-in")
+    WORKING_DIR = BENCHMARK_LOCATION
+
+    os.chdir(WORKING_DIR)
+except Exception as e:
+    print(e)
+    print("Failed to read benchmark programs, check the path. ")
+    
+    sys.exit(1)
+
+print("[*] Copying files")
+for program in PROGRAMS:
+    program = program.strip()
+    new_location = OUTPUT_DIR / program.replace("/", "_")
+    print(f"[*] Copying {program} to {new_location}")
+    shutil.copy(program, new_location.absolute())
+