diff --git a/src/example-archive/simple-examples/working/power_1.c b/src/example-archive/simple-examples/working/power_1.c
index cf84ca2..e76feba 100644
--- a/src/example-archive/simple-examples/working/power_1.c
+++ b/src/example-archive/simple-examples/working/power_1.c
@@ -7,6 +7,8 @@
 //   1. the base case - power_uf(2,0) = 1 
 //   2. the inductive case - power(2,y+1) == 2 * power_uf(2,y)
 
+/*@ function (i32) power_uf(i32 x, i32 y) @*/
+
 void lemma_power_uf_def(int y)
 /*@ trusted;
     requires y >= 0i32;
diff --git a/src/example-archive/simple-examples/working/power_2.c b/src/example-archive/simple-examples/working/power_2.c
index caf3e1d..3d7d344 100644
--- a/src/example-archive/simple-examples/working/power_2.c
+++ b/src/example-archive/simple-examples/working/power_2.c
@@ -1,5 +1,8 @@
 // Compute 2^1
 
+/*@ function (i32) power_uf(i32 x, i32 y) @*/
+
+
 /*@
 lemma LemmaPowerUFDef(i32 y)
   requires 
diff --git a/src/exercises/queue/push_induction.c b/src/exercises/queue/push_induction.c
index 37b2ad3..62d8085 100644
--- a/src/exercises/queue/push_induction.c
+++ b/src/exercises/queue/push_induction.c
@@ -19,9 +19,11 @@ void push_induction(struct queue_cell* front
 @*/
 {
     if (front == second_last) {
+        /*@ derive_constraints(RW(second_last), RW(last)); @*/
         /*@ unfold Snoc(Q, Second_last.first); @*/
         return;
     } else {
+        /*@ derive_constraints(RW(front), RW(second_last), RW(last)); @*/
         push_induction(front->next, second_last, last);
         /*@ unfold Snoc(Q, Second_last.first); @*/
         return;