diff --git a/examples/S/S.lean b/examples/S/S.lean
index a442f6e..64a2fc2 100644
--- a/examples/S/S.lean
+++ b/examples/S/S.lean
@@ -26,7 +26,7 @@ static S g_s = {0, 0, NULL};
 end
 
 alloy c opaque_extern_type S => S where
-  foreach(s, f) := lean_apply_1(f, s->m_s)
+  foreach(s, f) := lean_inc(f); lean_apply_1(f, s->m_s)
   finalize(s) := lean_dec(s->m_s); free(s)
 
 --------------------------------------------------------------------------------
diff --git a/examples/S/lakefile.lean b/examples/S/lakefile.lean
index 36dccb9..d1ede42 100644
--- a/examples/S/lakefile.lean
+++ b/examples/S/lakefile.lean
@@ -1,9 +1,8 @@
 import Lake
 open Lake DSL
 
-package s {
+package s where
   buildType := .debug
-}
 
 require alloy from ".."/".."
 
diff --git a/examples/S/test.sh b/examples/S/test.sh
index f944740..1d6b89a 100755
--- a/examples/S/test.sh
+++ b/examples/S/test.sh
@@ -3,4 +3,4 @@ rm -rf .lake
 LAKE=${LAKE:-lake}
 $LAKE build -U
 $LAKE build Test -v
-#.lake/build/bin/s # TODO: Segfaults for some reason
+.lake/build/bin/s