diff --git a/turnstile/examples/tests/rosette/rosette3/ifc3-tests.rkt b/turnstile/examples/tests/rosette/rosette3/ifc3-tests.rkt
index 2644566..1444e0c 100644
--- a/turnstile/examples/tests/rosette/rosette3/ifc3-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette3/ifc3-tests.rkt
@@ -1,7 +1,7 @@
 #lang s-exp "../../../rosette/ifc3.rkt"
 (require "../../rackunit-typechecking.rkt")
 
-;; verify-EENI-demo.rkt
+;; tests from verify-EENI-demo.rkt (same as rosette/sdsl/ifc/test.rkt)
 
 ;; takes ~90min to run
 
@@ -515,63 +515,3 @@
         
 (check-type (mem≈ (step (init fig17-p0) 13)
                   (step (init fig17-p1) 13)) : CBool -> #f)
-
-;; (define (valid-case name ended? prog [k #f])
-;;   (test-case name (check-true (verify-EENI* init ended? mem≈ prog k))))
-
-;; (define-syntax-rule (define-tests id desc expr ...)
-;;   (define id
-;;     (test-suite+ 
-;;      desc 
-;;      (begin expr ...))))
-
-;; ; Checks for counterexamples for bugs in basic semantics. 
-;; (define-tests basic-bugs "IFC: counterexamples for bugs in basic semantics"
-;;   (cex-case "Fig. 1" halted? (program 3 (list Halt Noop Push Pop Add* Load* Store*AB))) 
-;;   (cex-case "Fig. 2" halted? (program 3 (list Halt Noop Push Pop Add* Load* Store*B)))  
-;;   (cex-case "Fig. 3" halted? (program 5 (list Halt Noop Push Pop Add* Load* Store)))  
-;;   (cex-case "Fig. 4" halted? (program 7 (list Halt Noop Push Pop Add Load* Store))))  
-
-;; (define-tests basic-correct "IFC: no bounded counterexamples for correct basic semantics"
-;;   (valid-case "*" halted? (program 7 (list Halt Noop Push Pop Add Load Store)))  
-;;   (valid-case "+" halted? (program 8 (list Halt Noop Push Pop Add Load Store))))  
-
-;; (define-tests jump-bugs "IFC: counterexamples for bugs in jump+basic semantics"
-;;   (cex-case "11" halted? (program 6 (list Halt Noop Push Pop Add Load Store Jump*AB)))  
-;;   (cex-case "12" halted? (program 4 (list Halt Noop Push Pop Add Load Store Jump*B)))) 
-
-;; (define-tests jump-correct "IFC: no bounded counterexamples for correct jump+basic semantics"
-;;   (valid-case "**" halted? (program 7 (list Halt Noop Push Pop Add Load Store Jump)))    
-;;   (valid-case "++" halted? (program 8 (list Halt Noop Push Pop Add Load Store Jump))))    
-
-;; (define-tests call-return-bugs "IFC: counterexamples for buggy call+return+basic semantics"
-;;   (cex-case "Fig. 13" halted∩low? (program 7 (list Halt Noop Push Pop Add Load Store Call*B Return*AB)))
-;;   (cex-case "Fig. 15" halted∩low? (program 8 (list Halt Noop Push Pop Add Load StoreCR Call*B Return*AB)))
-;;   (cex-case "Fig. 16" halted∩low? (program 8 (list Halt Noop Push Pop Add Load StoreCR Call*B Return*B)))
-;;   (cex-case "Fig. 17" halted∩low? (program 10 (list Halt Noop Push Pop Add Load StoreCR Call Return))))
-
-;; (define-tests reproduce-bugs "IFC: counterexamples that are structurally similar to those in prior work"
-;;   (cex-case "Fig. 13*" halted∩low? (program (list Push Call*B Halt Push Push Store Return*AB)))
-;;   (cex-case "Fig. 15*" halted∩low? (program (list Push Push Call*B Push StoreCR Halt Push Return*AB)))
-;;   (cex-case "Fig. 16*" halted∩low? (program (list Push Push Call*B Push StoreCR Halt Return*B Push Return*B)))
-;;   (cex-case "Fig. 17*" 
-;;             halted∩low? 
-;;             (program (list Push Call Push StoreCR Halt Push Push Call Pop Push Return))
-;;             13))
-
-;; (define (fast-tests)
-;;   (time (run-tests basic-bugs))       ; ~10 sec
-;;   (time (run-tests basic-correct))    ; ~20 sec
-;;   (time (run-tests jump-bugs)))       ; ~7 sec
-
-;; (define (slow-tests)
-;;   (time (run-tests jump-correct))     ; ~52 sec
-;;   (time (run-tests call-return-bugs)) ; ~440 sec
-;;   (time (run-tests reproduce-bugs)))  ; ~256 sec
-
-;; (module+ fast
-;;   (fast-tests))
-
-;; (module+ test
-;;   (fast-tests)
-;;   (slow-tests))
diff --git a/turnstile/examples/tests/rosette/rosette3/run-all-rosette-tests-script.rkt b/turnstile/examples/tests/rosette/rosette3/run-all-rosette-tests-script.rkt
index c201625..d9bdee8 100644
--- a/turnstile/examples/tests/rosette/rosette3/run-all-rosette-tests-script.rkt
+++ b/turnstile/examples/tests/rosette/rosette3/run-all-rosette-tests-script.rkt
@@ -20,5 +20,6 @@
 
 (do-tests "bv-tests.rkt" "BV SDSL - General"
           "fsm3-tests.rkt" "FSM"
+          "ifc3-tests.rkt" "IFC"
           "bv-ref-tests.rkt" "BV SDSL - Hacker's Delight synthesis")