diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
index 65d6e99..9a6f724 100644
--- a/turnstile/examples/rosette/rosette2.rkt
+++ b/turnstile/examples/rosette/rosette2.rkt
@@ -84,6 +84,8 @@
 (define-type-constructor CIVectorof #:arity = 1)
 (define-type-constructor CMVectorof #:arity = 1)
 (define-type-constructor CBoxof #:arity = 1)
+;; TODO: Hash subtyping?
+(define-type-constructor HashTable #:arity = 2)
 (define-named-type-alias (CVectorof X) (CU (CIVectorof X) (CMVectorof X)))
 (define-type-constructor CList #:arity >= 0)
 
@@ -450,6 +452,11 @@
                                                 #'(CIVectorof (CU τ ...))
                                                 #'(CIVectorof (U τ ...)))]]])
 
+;; ---------------------------------
+;; hash tables
+
+(define-rosette-primop hash-keys : (C→ (HashTable Any Any) (CListof Any)))
+
 ;; ---------------------------------
 ;; lists
 
@@ -918,16 +925,16 @@
 
 (provide (rosette-typed-out [core : (C→ CSolution (U (Listof Any) CFalse))]
                             ; TODO: implement hash
-                            [model : (C→ CSolution Any)]
+                            [model : (C→ CSolution (HashTable Any Any))]
                             [sat : (Ccase-> (C→ CSolution)
-                                            (C→ Any CSolution))]
+                                            (C→ (HashTable Any Any) CSolution))]
                             [sat? : (C→ Any Bool)]
                             [unsat? : (C→ Any Bool)]
                             [unsat : (Ccase-> (C→ CSolution)
                                               (C→ (CListof Bool) CSolution))]
                             [forall : (C→ (CListof Any) Bool Bool)]
                             [exists : (C→ (CListof Any) Bool Bool)]))
-                            
+
 (define-typed-syntax verify
   [(_ e) ≫
    [⊢ [e ≫ e- ⇒ : _]]
diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt
index 1cd59eb..d5fdd0f 100644
--- a/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt
@@ -232,7 +232,9 @@
 (define f1 (forall (list a1) (exists (list b1) (= a1 (+ a1 b1))))) ; no free constants
 ; so the model has no bindings
 (define sol1 (solve (assert f1)))
-(check-type sol1 : CSolution) ; -> (sat) ; TODO: how to check empty model?
+(check-type sol1 : CSolution)
+(check-type (model sol1) : (HashTable Any Any))
+(check-type (hash-keys (model sol1)) : (CListof Any) -> (list)) ; empty solution
 (check-type (sat? sol1) : Bool -> #t)
 (define g1 (forall (list a1) (= a1 (+ a1 b1))))  ; b is free in g
 ; so the model has a binding for b