diff --git a/languages/source.nim b/languages/source.nim
index 91564a7..070cd49 100644
--- a/languages/source.nim
+++ b/languages/source.nim
@@ -733,12 +733,6 @@ const lang* = language:
     rule "E-builtin-concat":
       conclusion Call("concat", `array`(*val_1), val_2), `array`(...val_1, val_2)
 
-    rule "E-builtin-readFile":
-      # TODO: implement unknown but bounded values (the `such` clause)
-      #such val_1, `array`(*ch)
-      where val_2, 1 # XXX: temporary hack to make the code valid
-      conclusion Call("readFile", val_1), val_2
-
     rule "E-call-reduce":
       # the call is replaced with the procedure's body (in which all
       # occurrences of the parameters were substituted with a copy of the
@@ -794,6 +788,16 @@ const lang* = language:
       where C_2, C_1 + {"errOutput": `array`(...val_2, ...val_1)}
       conclusion C_1, Call("writeErr", val_1), C_2, TupleCons()
 
+    rule "E-builtin-readFile":
+      # the extra time parameter is used to model the fact that the file
+      # access doesn't always yield the same result, even when the program
+      # does nothing
+      where val_2, C_1.files(val_1, C_1.time)
+      where `array`(*ch), val_2
+      where n_1, C_1.time + 1
+      where C_2, C_1 + {"time": n_1}
+      conclusion C_1, Call("readFile", val_1), C_2, val_2
+
   inductive step(inp, inp, out, out), "$1; $2 \\rightarrow $3; $4":
     rule "E-reduce-pure":
       premise pReducesTo(e_1, e_2)