From a56250b26e9ef4056223279e9984b73e09158f66 Mon Sep 17 00:00:00 2001
From: AlexKnauth <alexander@knauth.org>
Date: Wed, 31 Aug 2016 18:59:54 -0400
Subject: [PATCH] start on tests from section 3 of the Guide

---
 .../rosette/rosette-guide-sec3-tests.rkt      | 20 +++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt

diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt
new file mode 100644
index 0000000..5e9ecdf
--- /dev/null
+++ b/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt
@@ -0,0 +1,20 @@
+#lang s-exp "../../rosette/rosette2.rkt"
+(require "../rackunit-typechecking.rkt"
+         "check-type+asserts.rkt")
+
+;; Examples from the Rosette Guide, Section 3
+
+;; Symbolic effects
+(define y1 (ann 0 : Nat))
+(check-type (if #t (void) (set! y1 3)) : CUnit -> (void))
+;; y1 unchanged: 0
+(check-type y1 : Nat -> 0)
+(check-type (if #f (set! y1 3) (void)) : CUnit -> (void))
+;; y1 unchanged: 0
+(check-type y1 : Nat -> 0)
+;; symbolic effect!
+(define-symbolic x1 boolean? : Bool)
+(check-type (if x1 (void) (set! y1 3)) : Unit -> (void))
+;; y1 symbolic: (ite x1 0 3)
+(check-type y1 : Nat -> (if x1 0 3))
+