diff --git a/turnstile/examples/rosette/lib/synthax.rkt b/turnstile/examples/rosette/lib/synthax.rkt
index 6893e73..e2bc854 100644
--- a/turnstile/examples/rosette/lib/synthax.rkt
+++ b/turnstile/examples/rosette/lib/synthax.rkt
@@ -16,10 +16,10 @@
    #:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
    [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]]
    #:fail-unless (syntax-e #'s?)
-                 (format "Must provide a Rosette-solvable type, given ~a." 
+                 (format "Expected a Rosette-solvable type, given ~a." 
                          (syntax->datum #'pred?))
    #:fail-when (syntax-e #'f?)
-               (format "Must provide a non-function Rosette type, given ~a." 
+               (format "Expected a non-function Rosette type, given ~a." 
                        (syntax->datum #'pred?))
    --------
    [⊢ [_ ≫ (??/progsrc pred?-) ⇒ : ty]]])
diff --git a/turnstile/examples/rosette/query/debug.rkt b/turnstile/examples/rosette/query/debug.rkt
index a3feed6..19c8a2d 100644
--- a/turnstile/examples/rosette/query/debug.rkt
+++ b/turnstile/examples/rosette/query/debug.rkt
@@ -29,10 +29,10 @@
   [(_ (pred? ...+) e) ≫
    [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]] ...
    #:fail-unless (stx-andmap syntax-e #'(s? ...))
-                 (format "Must provide a Rosette-solvable type, given ~a." 
+                 (format "Expected a Rosette-solvable type, given ~a." 
                          (syntax->datum #'(pred? ...)))
    #:fail-when (stx-ormap syntax-e #'(f? ...))
-               (format "Must provide a non-function Rosette type, given ~a." 
+               (format "Expected a non-function Rosette type, given ~a." 
                        (syntax->datum #'(pred? ...)))
    [⊢ [e ≫ e- ⇒ : τ]]
    --------
diff --git a/turnstile/examples/rosette/rosette-notes.txt b/turnstile/examples/rosette/rosette-notes.txt
index cf85f0d..a032e16 100644
--- a/turnstile/examples/rosette/rosette-notes.txt
+++ b/turnstile/examples/rosette/rosette-notes.txt
@@ -1,4 +1,17 @@
-2016-09-08
+2016-09-08 --------------------
+
+** Problem: Constant is unsound:
+
+(define-symbolic f (~> integer? boolean?))
+(define-symbolic x integer?)
+(define sol (solve (assert (not (equal? (f x) (f 1))))))
+(define res (evaluate x sol))
+
+res has type (Constant Int) but (constant? res) is false
+
+** Workaround: 
+
+2016-09-08 --------------------
 
 Typed Rosette tricky subtyping examples:
 
@@ -122,6 +135,9 @@ TODOs:
 - use variance information in type constructors?
   - instead of special-casing individual constructors
 - ok to say "Rosette type" in type err msgs?
+- 2016-09-08: fix Constant soundness wrt evaluate
+- 2016-09-08: transfer "typefor" and "solvable?" props to id in define
+  - DONE 2016-09-08
 
 2016-08-25 --------------------
 
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
index 7c143cd..a65013d 100644
--- a/turnstile/examples/rosette/rosette2.rkt
+++ b/turnstile/examples/rosette/rosette2.rkt
@@ -155,10 +155,14 @@
     (syntax-property stx 'typefor))
   (define (mark-solvable stx)
     (set-stx-prop/preserved stx 'solvable? #t))
+  (define (set-solvable stx v)
+    (set-stx-prop/preserved stx 'solvable? v))
   (define (solvable? stx)
     (syntax-property stx 'solvable?))
   (define (mark-function stx)
     (set-stx-prop/preserved stx 'function? #t))
+  (define (set-function stx v)
+    (set-stx-prop/preserved stx 'function? v))
   (define (function? stx)
     (syntax-property stx 'function?)))
 
@@ -213,7 +217,7 @@
   [(_ x:id ...+ pred?) ≫
    [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]]
    #:fail-unless (syntax-e #'s?)
-                 (format "Must provide a Rosette-solvable type, given ~a." 
+                 (format "Expected a Rosette-solvable type, given ~a." 
                          (syntax->datum #'pred?))
    #:with (y ...) (generate-temporaries #'(x ...))
    --------
@@ -225,7 +229,7 @@
   [(_ x:id ...+ pred?) ≫
    [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]]
    #:fail-unless (syntax-e #'s?)
-                 (format "Must provide a Rosette-solvable type, given ~a." 
+                 (format "Expected a Rosette-solvable type, given ~a." 
                          (syntax->datum #'pred?))
    #:with (y ...) (generate-temporaries #'(x ...))
    --------
@@ -238,7 +242,7 @@
   [(_ (x:id ...+ pred?) e ...) ≫
    [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]]
    #:fail-unless (syntax-e #'s?)
-                 (format "Must provide a Rosette-solvable type, given ~a." 
+                 (format "Expected a Rosette-solvable type, given ~a." 
                          (syntax->datum #'pred?))
    [([x ≫ x- : (Constant ty)] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]]
    --------
@@ -251,7 +255,7 @@
   [(_ (x:id ...+ pred?) e ...) ≫
    [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]]
    #:fail-unless (syntax-e #'s?)
-                 (format "Must provide a Rosette-solvable type, given ~a." 
+                 (format "Expected a Rosette-solvable type, given ~a." 
                          (syntax->datum #'pred?))
    [([x ≫ x- : (Constant ty)] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]]
    --------
@@ -794,6 +798,7 @@
 
                             [true : CTrue]
                             [false : CFalse]
+                            [real->integer : (C→ Num Int)]
                             [number? : (C→ Any Bool)]
                             [positive? : (Ccase-> (C→ CNum CBool)
                                                   (C→ Num Bool))]
@@ -896,6 +901,7 @@
    [⊢ [_ ≫ (ro:current-bitwidth e-) ⇒ : CUnit]]])
 
 (define-named-type-alias BV (add-predm (U CBV) bv?))
+(define-named-type-alias CPred (C→ Any Bool))
 (define-symbolic-named-type-alias BVPred (C→ Any Bool) #:pred lifted-bitvector?)
 (define-named-type-alias BVMultiArgOp (Ccase-> (C→ BV BV BV)
                                                (C→ BV BV BV BV)))
@@ -979,22 +985,25 @@
 ;; Uninterpreted functions
 
 (define-typed-syntax ~>
-  [(_ pred? ...+) ≫
+  [(_ pred? ...+ out) ≫
    [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]] ...
-   #:fail-unless (stx-andmap syntax-e #'(s? ...))
-                 (format "Must provide a Rosette-solvable type, given ~a." 
-                         (syntax->datum #'(pred? ...)))
-   #:fail-when (stx-ormap syntax-e #'(f? ...))
-               (format "Must provide a non-function Rosette type, given ~a." 
-                       (syntax->datum #'(pred? ...)))
+   [⊢ [out ≫ out- (⇒ : _) (⇒ typefor ty-out) (⇒ solvable? out-s?) (⇒ function? out-f?)]]
+   #:fail-unless (stx-andmap syntax-e #'(s? ... out-s?))
+                 (format "Expected a Rosette-solvable type, given ~a." 
+                         (syntax->datum #'(pred? ... out)))
+   #:fail-when (stx-ormap syntax-e #'(f? ... out-f?))
+               (format "Expected a non-function Rosette type, given ~a." 
+                       (syntax->datum #'(pred? ... out)))
    --------
    [⊢ [_ ≫ (mark-solvablem
             (mark-functionm
              (add-typeform
-              (ro:~> pred?- ...)
-              (→ ty ...))))
+              (ro:~> pred?- ... out-)
+              (→ ty ... ty-out))))
               ⇒ : (C→ Any Bool)]]])
 
+(define-rosette-primop fv? : (C→ Any Bool))
+
 ;; ---------------------------------
 ;; Logic operators
 (provide (rosette-typed-out [! : (C→ Bool Bool)]
@@ -1123,6 +1132,11 @@
    [⊢ [_ ≫ (ro:verify #:assume ae- #:guarantee ge-) ⇒ : CSolution]]])
 
 (define-typed-syntax evaluate
+  [(_ v s) ≫
+   [⊢ [v ≫ v- ⇒ : (~Constant* ty)]]
+   [⊢ [s ≫ s- ⇐ : CSolution]]
+   --------
+   [⊢ [_ ≫ (ro:evaluate v- s-) ⇒ : ty]]]
   [(_ v s) ≫
    [⊢ [v ≫ v- ⇒ : ty]]
    [⊢ [s ≫ s- ⇐ : CSolution]]
@@ -1177,6 +1191,13 @@
    --------
    [⊢ [_ ≫ (ro:optimize #:maximize maxe- #:minimize mine- #:guarantee ge-) ⇒ : CSolution]]])
 
+;; ---------------------------------
+;; Symbolic reflection
+
+(define-rosette-primop term? : CPred)
+(define-rosette-primop expression? : CPred)
+(define-rosette-primop constant? : CPred)
+
 ;; ---------------------------------
 ;; Subtyping
 
diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt
index b6e74d1..f0633a3 100644
--- a/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt
@@ -104,9 +104,9 @@
 
 (define ucore (debug [integer?] (same poly factored/d 12)))
 (typecheck-fail (debug [positive?] (same poly factored/d 12))
- #:with-msg "Must provide a Rosette-solvable type, given.*positive?")
-(typecheck-fail (debug [(~> integer?)] (same poly factored/d 12))
- #:with-msg "Must provide a non-function Rosette type, given.*~> integer?")
+ #:with-msg "Expected a Rosette-solvable type, given.*positive?")
+(typecheck-fail (debug [(~> integer? integer?)] (same poly factored/d 12))
+ #:with-msg "Expected a non-function Rosette type, given.*~> integer\\? integer\\?")
 (check-type ucore : CSolution)
 ;; TESTING TODO: requires visual inspection (in DrRacket)
 (check-type (render ucore) : CPict)
@@ -117,9 +117,9 @@
 (check-type (??) : Int)
 (check-type (?? boolean?) : Bool)
 (typecheck-fail (?? positive?) 
- #:with-msg "Must provide a Rosette-solvable type, given.*positive?")
-(typecheck-fail (?? (~> integer?))
- #:with-msg "Must provide a non-function Rosette type, given.*integer?")
+ #:with-msg "Expected a Rosette-solvable type, given.*positive?")
+(typecheck-fail (?? (~> integer? integer?))
+ #:with-msg "Expected a non-function Rosette type, given.*integer\\? integer\\?")
 
 
 (define (factored/?? [x : Int] -> Int)
diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt
index 068ac6d..f3453a3 100644
--- a/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt
@@ -1,6 +1,5 @@
 #lang s-exp "../../rosette/rosette2.rkt"
-(require "../rackunit-typechecking.rkt"
-         "check-type+asserts.rkt")
+(require "../rackunit-typechecking.rkt")
 
 ;; Examples from the Rosette Guide, Section 4.1 - 4.2
 
@@ -27,10 +26,10 @@
 (check-type (equal? (box n) (box 1)) : Bool -> (= 1 n))
 (check-not-type (equal? n 1) : CBool)
 (check-not-type (equal? (box n) (box 1)) : CBool)
-(typecheck-fail (~> positive?)
- #:with-msg "Must provide a Rosette\\-solvable type, given.*positive?")
-(typecheck-fail (~> (~> integer?))
- #:with-msg "Must provide a non\\-function Rosette type, given.*~> integer?")
+(typecheck-fail (~> positive? positive?)
+ #:with-msg "Expected a Rosette\\-solvable type, given.*positive?")
+(typecheck-fail (~> (~> integer? integer?) integer?)
+ #:with-msg "Expected a non\\-function Rosette type, given.*~> integer?")
 (define-symbolic f g (~> integer? integer?))
 (check-type f : (→ Int Int))
 (check-type g : (→ Int Int))
diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec43-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec43-tests.rkt
index fb8e648..07d97b2 100644
--- a/turnstile/examples/tests/rosette/rosette-guide-sec43-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette-guide-sec43-tests.rkt
@@ -1,6 +1,5 @@
 #lang s-exp "../../rosette/rosette2.rkt"
-(require "../rackunit-typechecking.rkt"
-         "check-type+asserts.rkt")
+(require "../rackunit-typechecking.rkt")
 
 ;; Examples from the Rosette Guide, Section 4.3
 
diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec44-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec44-tests.rkt
new file mode 100644
index 0000000..fd8b551
--- /dev/null
+++ b/turnstile/examples/tests/rosette/rosette-guide-sec44-tests.rkt
@@ -0,0 +1,57 @@
+#lang s-exp "../../rosette/rosette2.rkt"
+(require "../rackunit-typechecking.rkt"
+         "check-type+asserts.rkt")
+
+;; Examples from the Rosette Guide, Section 4.4
+
+;; 4.4 Uninterpreted Functions
+
+;; example demonstrating unsoundness of Constant
+;; (define-symbolic f (~> integer? boolean?))
+;; (define-symbolic x integer?)
+;; (define sol (solve (assert (not (equal? (f x) (f 1))))))
+;; (define res (evaluate x sol))
+;; (check-type res : (Constant Int))
+;; (constant? res)
+
+; an uninterpreted function from integers to booleans:
+(define-symbolic f (~> integer? boolean?))
+; no built-in interpretation for 1
+(check-type (f 1) : Bool -> (f 1))
+(check-not-type (f 1) : CBool)
+(define-symbolic x real?)
+; typed Rosette rejects tis program
+(typecheck-fail (f x) #:with-msg "expected Int, given.*Num")
+(check-type (f (assert-type x : Int)) 
+            : Bool -> (f (assert-type x : Int))) ;(app f (real->integer x)))
+(check-type (asserts) : CAsserts -> (list (integer? x)))
+
+(define sol (solve (assert (not (equal? (f (assert-type x : Int)) (f 1))))))
+(check-type sol : CSolution)
+(define g (evaluate f sol)) ; an interpretation of f
+(check-type g : (→ Int Bool)) ; -> (fv (((1) . #f) ((0) . #t)) #f integer?~>boolean?)
+;; should this be Num or Int?
+;(check-type (evaluate x sol) : Int -> 0)
+(check-type (evaluate x sol) : Num -> 0) ; nondeterministic result
+;; check soundness of Constant
+(check-not-type (evaluate x sol) : (Constant Num))
+; f is a function value
+(check-type (fv? f) : Bool -> #t)
+; and so is g
+(check-type (fv? g) : Bool -> #t)
+; we can apply g to concrete values
+(check-type (g 2) : Bool -> #f)
+; and to symbolic values
+(check-type (g (assert-type x : Int)) : Bool -> (= 0 (real->integer x))) ; nondet result
+;; this should be the only test that is deterministic
+(check-type (equal? (g 1) (g (assert-type (evaluate x sol) : Int))) : Bool -> #f)
+
+;; ~>
+(define t (~> integer? real? boolean? (bitvector 4)))
+(check-type t : (C→ Any Bool) -> (~> integer? real? boolean? (bitvector 4))) ;integer?~>real?~>boolean?~>(bitvector? 4)
+(typecheck-fail (~> t integer?)
+ #:with-msg "Expected a non-function Rosette type, given.*t")
+(define-symbolic b boolean?)
+(typecheck-fail (~> integer? (if b boolean? real?))
+ #:with-msg "Expected a Rosette-solvable type, given")
+(typecheck-fail (~> real?) #:with-msg "expected more terms")
diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt
index 20d9a30..de61ffd 100644
--- a/turnstile/examples/tests/rosette/rosette2-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette2-tests.rkt
@@ -102,7 +102,7 @@
 (define-symbolic b0 boolean?)
 (define-symbolic i0 integer?)
 (typecheck-fail (define-symbolic posint1 positive?) 
- #:with-msg "Must provide a Rosette-solvable type, given positive?")
+ #:with-msg "Expected a Rosette-solvable type, given positive?")
 (typecheck-fail (lambda ([x : (Constant CInt)]) x)
  #:with-msg "Constant requires a symbolic type")
 (check-type b0 : Bool -> b0)
diff --git a/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt b/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt
index ccf640f..f38563a 100644
--- a/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt
+++ b/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt
@@ -6,7 +6,8 @@
           "rosette-guide-sec2-tests.rkt" "Rosette Guide, Section 2"
           "rosette-guide-sec3-tests.rkt" "Rosette Guide, Section 3"
           "rosette-guide-sec4-tests.rkt" "Rosette Guide, Section 4.1-4.2"
-          "rosette-guide-sec43-tests.rkt" "Rosette Guide, Section 4.3")
+          "rosette-guide-sec43-tests.rkt" "Rosette Guide, Section 4.3 BVs"
+          "rosette-guide-sec44-tests.rkt" "Rosette Guide, Section 4.4 Uninterp Fns")
 
 (do-tests "bv-tests.rkt" "BV SDSL - General"
           "bv-ref-tests.rkt" "BV SDSL - Hacker's Delight synthesis")