diff --git a/turnstile/examples/rosette/rosette-notes.txt b/turnstile/examples/rosette/rosette-notes.txt
index ff297b5..691eea2 100644
--- a/turnstile/examples/rosette/rosette-notes.txt
+++ b/turnstile/examples/rosette/rosette-notes.txt
@@ -53,7 +53,8 @@ TODOs:
 - fix type of Vector and List to differentiate homogeneous/hetero
   - 2016-09-01: add CList for hetero lists
 - variable arity polymorphism
-- CSolution?
+- CSolution
+   - DONE 2016-08-30
 - make libs have appropriate require paths
   - eg typed/rosette/query/debug
 - make typed/rosette a separate pkg
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
index 789c7ca..8be107b 100644
--- a/turnstile/examples/rosette/rosette2.rkt
+++ b/turnstile/examples/rosette/rosette2.rkt
@@ -562,6 +562,18 @@
                                           (C→ Num Num Num)
                                           (C→ Num Num Num Num)
                                           (C→ Num Num Num Num Num))]
+                            [- : (Ccase-> (C→ CInt CInt CInt)
+                                          (C→ CInt CInt CInt CInt)
+                                          (C→ CInt CInt CInt CInt CInt)
+                                          (C→ Int Int Int)
+                                          (C→ Int Int Int Int)
+                                          (C→ Int Int Int Int Int)
+                                          (C→ CNum CNum CNum)
+                                          (C→ CNum CNum CNum CNum)
+                                          (C→ CNum CNum CNum CNum CNum)
+                                          (C→ Num Num Num)
+                                          (C→ Num Num Num Num)
+                                          (C→ Num Num Num Num Num))]
                             [* : (Ccase-> (C→ CNat CNat CNat)
                                           (C→ CNat CNat CNat CNat)
                                           (C→ CNat CNat CNat CNat CNat)
@@ -611,6 +623,12 @@
                             [real? : (C→ Any Bool)]
                             [positive? : (Ccase-> (C→ CNum CBool)
                                                   (C→ Num Bool))]
+                            [even? : (Ccase-> (C→ CInt CBool)
+                                              (C→ Int Bool))]
+                            [odd? : (Ccase-> (C→ CInt CBool)
+                                             (C→ Int Bool))]
+                            [remainder : (Ccase-> (C→ CInt CInt CInt)
+                                                  (C→ Int Int Int))]
 
                             ;; rosette-specific
                             [asserts : (C→ (CListof Bool))]
@@ -702,6 +720,17 @@
    --------
    [⊢ [_ ≫ (ro:|| e- ...) ⇒ : Bool]]])
 
+(define-typed-syntax and
+  [(_ e ...) ≫
+   [⊢ [e ≫ e- ⇐ : Bool] ...]
+   --------
+   [⊢ [_ ≫ (ro:and e- ...) ⇒ : Bool]]])
+(define-typed-syntax or
+  [(_ e ...) ≫
+   [⊢ [e ≫ e- ⇐ : Bool] ...]
+   --------
+   [⊢ [_ ≫ (ro:or e- ...) ⇒ : Bool]]])
+
 ;; ---------------------------------
 ;; solver forms
 
@@ -753,6 +782,34 @@
    --------
    [⊢ [_ ≫ (ro:solve e-) ⇒ : CSolution]]])
 
+(define-typed-syntax optimize
+  [(_ #:guarantee ge) ≫
+   [⊢ [ge ≫ ge- ⇒ : _]]
+   --------
+   [⊢ [_ ≫ (ro:optimize #:guarantee ge-) ⇒ : CSolution]]]
+  [(_ #:minimize mine #:guarantee ge) ≫
+   [⊢ [ge ≫ ge- ⇒ : _]]
+   [⊢ [mine ≫ mine- ⇐ : (CListof (U Num BV))]]
+   --------
+   [⊢ [_ ≫ (ro:optimize #:minimize mine- #:guarantee ge-) ⇒ : CSolution]]]
+  [(_ #:maximize maxe #:guarantee ge) ≫
+   [⊢ [ge ≫ ge- ⇒ : _]]
+   [⊢ [maxe ≫ maxe- ⇐ : (CListof (U Num BV))]]
+   --------
+   [⊢ [_ ≫ (ro:optimize #:maximize maxe- #:guarantee ge-) ⇒ : CSolution]]]
+  [(_ #:minimize mine #:maximize maxe #:guarantee ge) ≫
+   [⊢ [ge ≫ ge- ⇒ : _]]
+   [⊢ [maxe ≫ maxe- ⇐ : (CListof (U Num BV))]]
+   [⊢ [mine ≫ mine- ⇐ : (CListof (U Num BV))]]
+   --------
+   [⊢ [_ ≫ (ro:optimize #:minimize mine- #:maximize maxe- #:guarantee ge-) ⇒ : CSolution]]]
+  [(_ #:maximize maxe #:minimize mine #:guarantee ge) ≫
+   [⊢ [ge ≫ ge- ⇒ : _]]
+   [⊢ [maxe ≫ maxe- ⇐ : (CListof (U Num BV))]]
+   [⊢ [mine ≫ mine- ⇐ : (CListof (U Num BV))]]
+   --------
+   [⊢ [_ ≫ (ro:optimize #:maximize maxe- #:minimize mine- #:guarantee ge-) ⇒ : CSolution]]])
+
 ;; ---------------------------------
 ;; Subtyping
 
@@ -772,12 +829,12 @@
        [((~CList . tys1) (~CList . tys2))
         (and (stx-length=? #'tys1 #'tys2)
              (typechecks? #'tys1 #'tys2))]
-       [((~CList . tys) (~CListof . ty))
+       [((~CList . tys) (~CListof ty))
         (for/and ([t (stx->list #'tys)])
           (typecheck? t #'ty))]
        ;; vectors, only immutable vectors are invariant
-       [((~CIVectorof . tys1) (~CIVectorof . tys2))
-        (stx-andmap (current-sub?) #'tys1 #'tys2)]
+       [((~CIVectorof ty1) (~CIVectorof ty2))
+        (typecheck? #'ty1 #'ty2)]
        ; 2 U types, subtype = subset
        [((~CU* . ts1) _)
         (for/and ([t (stx->list #'ts1)])
diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt
index 3b54720..b3d4d94 100644
--- a/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt
@@ -34,3 +34,84 @@
 
 (check-type (second res) : Nat -> (if (first res) 0 3))
  
+;; 3.2 Solver-Aided Forms
+
+;; 3.2.1 Symbolic Constants
+
+(define (always-same -> Int)
+  (let-symbolic ([(x) integer? : Int])
+    x))
+(check-type (always-same) : Int)
+(check-type (eq? (always-same) (always-same)) : Bool -> #t)
+
+(define (always-different -> Int)
+  (let-symbolic* ([(x) integer? : Int])
+    x))
+(check-type (always-different) : Int)
+(define diff-sym*1 (always-different))
+(define diff-sym*2 (always-different))
+(check-type (eq? diff-sym*1 diff-sym*2) : Bool -> (= diff-sym*1 diff-sym*2))
+
+;; 3.2.2 Assertions
+
+(check-type+asserts (assert #t) : Unit -> (void) (list))
+(check-type+asserts (assert 1) : Unit -> (void) (list))
+(define-symbolic x123 boolean? : Bool)
+(check-type+asserts (assert x123) : Unit -> (void) (list x123))
+(check-runtime-exn (assert #f "bad value"))
+
+(check-type (asserts) : (CListof Bool) -> (list #f))
+(check-type (clear-asserts!) : Unit -> (void))
+(check-type (asserts) : (CListof Bool) -> (list))
+
+;; 3.2.3 Angelic Execution
+(define-symbolic x y boolean? : Bool)
+(check-type (assert x) : Unit -> (void)) 
+(check-type (asserts) : (CListof Bool) -> (list x))
+(define solve-sol (solve (assert y)))
+(check-type solve-sol : CSolution)
+(check-type (sat? solve-sol) : Bool -> #t)
+(check-type (evaluate x solve-sol) : Bool -> #t) ; x must be true
+(check-type (evaluate y solve-sol) : Bool -> #t) ; y must be true
+(check-type (solve (assert (not x))) : CSolution -> (unsat))
+(clear-asserts!)
+
+;; 3.2.4 Verification
+(check-type (assert x) : Unit -> (void)) 
+(check-type (asserts) : (CListof Bool) -> (list x))
+(define verif-sol (verify (assert y)))
+(check-type (asserts) : (CListof Bool) -> (list x))
+(check-type (evaluate x verif-sol) : Bool -> #t) ; x must be true
+(check-type (evaluate y verif-sol) : Bool -> #f) ; y must be false
+(check-type (verify #:assume (assert y) #:guarantee (assert (and x y))) 
+            : CSolution -> (unsat))
+(clear-asserts!)
+
+;; 3.2.5 Synthesis
+(define-symbolic synth-x synth-c integer? : Int)
+(check-type (assert (even? synth-x)) : Unit -> (void))
+(check-type (asserts) : (CListof Bool) -> (list (= 0 (remainder synth-x 2))))
+(define synth-sol
+  (synthesize #:forall (list synth-x)
+              #:guarantee (assert (odd? (+ synth-x synth-c)))))
+(check-type (asserts) : (CListof Bool) -> (list (= 0 (remainder synth-x 2))))
+(check-type (evaluate synth-x synth-sol) : Int -> synth-x) ; x is unbound
+(check-type (evaluate synth-c synth-sol) : Int -> 1) ; c must an odd integer
+(clear-asserts!)
+
+;; 3.2.6 Optimization
+(current-bitwidth #f) ; use infinite-precision arithmetic
+(define-symbolic opt-x opt-y integer? : Int)
+(check-type (assert (< opt-x 2)) : Unit -> (void))
+(check-type (asserts) : (CListof Bool) -> (list (< opt-x 2)))
+(define opt-sol
+  (optimize #:maximize (list (+ opt-x opt-y))
+            #:guarantee (assert (< (- opt-y opt-x) 1))))
+; assertion store same as before
+(check-type (asserts) : (CListof Bool) -> (list (< opt-x 2))) 
+; x + y is maximal at x = 1 and y = 1
+(check-type (evaluate opt-x opt-sol) : Int -> 1) 
+(check-type (evaluate opt-y opt-sol) : Int -> 1)
+
+;; 3.2.8 Reasoning Precision
+;; see rosette-guide-sec2-tests.rkt, Sec 2.4 Symbolic Reasoning
diff --git a/turnstile/examples/tests/rosette/run-all-rosette-tests.rkt b/turnstile/examples/tests/rosette/run-all-rosette-tests.rkt
index 4799da3..d67c792 100644
--- a/turnstile/examples/tests/rosette/run-all-rosette-tests.rkt
+++ b/turnstile/examples/tests/rosette/run-all-rosette-tests.rkt
@@ -4,10 +4,15 @@
 (require "rosette-guide-sec2-tests.rkt")
 (require "rosette-guide-sec3-tests.rkt")
 (require "bv-tests.rkt")
+
 ;(require "bv-ref-tests.rkt")
 ; visit but dont instantiate, o.w. will get unsat
 ;(dynamic-require "fsm-test.rkt" #f)
+<<<<<<< HEAD
 (require "ifc-tests.rkt")
 
 ; don't run this file for testing:
 (module test racket/base)
+=======
+;(require "ifc-tests.rkt")
+>>>>>>> add optimize, remaining sec3 tests; fix CList-CListof subtyping