From 947ba8ea21e7494d5707d9f4966238fdb39cce4c Mon Sep 17 00:00:00 2001
From: Christopher Pulte <cp526@cam.ac.uk>
Date: Mon, 30 Jun 2025 13:15:02 +0100
Subject: [PATCH 1/2] fix recursive predicate definitions

---
 src/exercises/queue/headers.test.h  | 4 ++--
 src/exercises/queue/headers.verif.h | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/exercises/queue/headers.test.h b/src/exercises/queue/headers.test.h
index 3b1a4a7f..cc336e12 100644
--- a/src/exercises/queue/headers.test.h
+++ b/src/exercises/queue/headers.test.h
@@ -5,8 +5,8 @@
 #include "../list/snoc.h"
 
 #include "./c_types.h"
-#include "./cn_types_1.test.h"
-#include "./cn_types_2.test.h"
 #include "./cn_types_3.test.h"
+#include "./cn_types_2.test.h"
+#include "./cn_types_1.test.h"
 
 #include "./allocation.test.h"
diff --git a/src/exercises/queue/headers.verif.h b/src/exercises/queue/headers.verif.h
index 333fc077..1d19ab3d 100644
--- a/src/exercises/queue/headers.verif.h
+++ b/src/exercises/queue/headers.verif.h
@@ -5,8 +5,8 @@
 #include "../list/snoc.h"
 
 #include "./c_types.h"
-#include "./cn_types_1.verif.h"
-#include "./cn_types_2.verif.h"
 #include "./cn_types_3.verif.h"
+#include "./cn_types_2.verif.h"
+#include "./cn_types_1.verif.h"
 
 #include "./allocation.verif.h"

From f0f5434c6d3beea90e7d02e2826aa037b1660259 Mon Sep 17 00:00:00 2001
From: Christopher Pulte <cp526@cam.ac.uk>
Date: Mon, 30 Jun 2025 13:38:13 +0100
Subject: [PATCH 2/2] fix recursive predicate definitions

---
 src/example-archive/simple-examples/working/list_3.c     | 2 +-
 src/example-archive/simple-examples/working/list_preds.h | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/example-archive/simple-examples/working/list_3.c b/src/example-archive/simple-examples/working/list_3.c
index 662b7973..f6caead3 100644
--- a/src/example-archive/simple-examples/working/list_3.c
+++ b/src/example-archive/simple-examples/working/list_3.c
@@ -7,7 +7,7 @@
 // must store this value. 
 
 /*@
-predicate (datatype seq) IntListSegVal(pointer p, pointer tail, i32 tval) {
+predicate [rec] (datatype seq) IntListSegVal(pointer p, pointer tail, i32 tval) {
   if (addr_eq(p,tail)) {
     return Seq_Nil{};
   } else {
diff --git a/src/example-archive/simple-examples/working/list_preds.h b/src/example-archive/simple-examples/working/list_preds.h
index 66b0ec04..7b0b4c2e 100644
--- a/src/example-archive/simple-examples/working/list_preds.h
+++ b/src/example-archive/simple-examples/working/list_preds.h
@@ -24,7 +24,7 @@ datatype seq {
 // a pure sequence of values.
 
 /*@
-predicate (datatype seq) IntListSeg(pointer p, pointer tail) {
+predicate [rec] (datatype seq) IntListSeg(pointer p, pointer tail) {
   if (ptr_eq(p,tail)) {
     return Seq_Nil{};
   } else {