diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
index c213a5c..5c75d70 100644
--- a/turnstile/examples/rosette/rosette2.rkt
+++ b/turnstile/examples/rosette/rosette2.rkt
@@ -213,14 +213,18 @@
 
 (define-rosette-primop bvnot : (C→ BV BV))
 
-;; TODO: bvand, bvor, bvxor
+(define-rosette-primop bvand : (C→ BV BV BV))
+(define-rosette-primop bvor : (C→ BV BV BV))
+(define-rosette-primop bvxor : (C→ BV BV BV))
 
 (define-rosette-primop bvshl : (C→ BV BV BV))
 (define-rosette-primop bvlshr : (C→ BV BV BV))
 (define-rosette-primop bvashr : (C→ BV BV BV))
 (define-rosette-primop bvneg : (C→ BV BV))
 
-;; TODO: bvadd, bvsub, bvmul
+(define-rosette-primop bvadd : (C→ BV BV BV))
+(define-rosette-primop bvsub : (C→ BV BV BV))
+(define-rosette-primop bvmul : (C→ BV BV BV))
 
 (define-rosette-primop bvsdiv : (C→ BV BV BV))
 (define-rosette-primop bvudiv : (C→ BV BV BV))
diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt
index 29062e7..aec4011 100644
--- a/turnstile/examples/tests/rosette/rosette2-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette2-tests.rkt
@@ -124,18 +124,18 @@
 (check-type (bveq (bv 1 2) (bv 1 3)) : Bool) ; -> runtime exn
 (check-runtime-exn (bveq (bv 1 2) (bv 1 3)))
 
-;; ;; non-primop bvops
-;; (check-type (bvand (bv -1 (bvpred 4)) (bv 2 (bvpred 4))) : BV 
-;;             -> (bv 2 (bvpred 4)))
-;; (check-type (bvor  (bv 0 (bvpred 3))  (bv 1 (bvpred 3))) : BV 
-;;             -> (bv 1 (bvpred 3)))
-;; (check-type (bvxor (bv -1 (bvpred 5)) (bv 1 (bvpred 5))) : BV 
-;;             -> (bv -2 (bvpred 5)))
 
-;; ;; examples from rosette guide
-;; (check-type (bvand (bv -1 4) (bv 2 4)) : BV -> (bv 2 4))
-;; (check-type (bvor  (bv 0 3)  (bv 1 3)) : BV -> (bv 1 3))
-;; (check-type (bvxor (bv -1 5) (bv 1 5)) : BV -> (bv -2 5))
+(check-type (bvand (bv -1 4) (bv 2 4)) : BV 
+            -> (bv 2 4))
+(check-type (bvor  (bv 0 3)  (bv 1 3)) : BV 
+            -> (bv 1 3))
+(check-type (bvxor (bv -1 5) (bv 1 5)) : BV 
+            -> (bv -2 5))
+
+;; examples from rosette guide
+(check-type (bvand (bv -1 4) (bv 2 4)) : BV -> (bv 2 4))
+(check-type (bvor  (bv 0 3)  (bv 1 3)) : BV -> (bv 1 3))
+(check-type (bvxor (bv -1 5) (bv 1 5)) : BV -> (bv -2 5))
 
 ;; (define-symbolic b boolean? : Bool)
 ;; (check-type (bvand (bv -1 4) (if b (bv 3 4) (bv 2 4))) : BV