From 9240c0dcbd5ca097d34355bfa75d8cdb998534bc Mon Sep 17 00:00:00 2001
From: Christopher Pulte <cp526@cam.ac.uk>
Date: Thu, 13 Aug 2026 22:28:04 +0400
Subject: [PATCH] adjust one test to use derive_constraints command

---
 src/exercises/queue/push_induction.c | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/exercises/queue/push_induction.c b/src/exercises/queue/push_induction.c
index 37b2ad34..62d80851 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;