From 02e019fe452db50c5430461dd96faa07f210257a Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Fri, 18 Nov 2022 13:44:53 -0500
Subject: [PATCH] Highlighted that reused list proofs assume single-core
 setting.

---
 verification/verifast/proof/nathan/README.md                   | 3 ---
 verification/verifast/proof/single_core_proofs/README.md       | 3 +++
 .../proof/{nathan => single_core_proofs}/list_predicates.h     | 0
 verification/verifast/proof/task_predicates.h                  | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)
 delete mode 100644 verification/verifast/proof/nathan/README.md
 create mode 100644 verification/verifast/proof/single_core_proofs/README.md
 rename verification/verifast/proof/{nathan => single_core_proofs}/list_predicates.h (100%)

diff --git a/verification/verifast/proof/nathan/README.md b/verification/verifast/proof/nathan/README.md
deleted file mode 100644
index d8b83cacb..000000000
--- a/verification/verifast/proof/nathan/README.md
+++ /dev/null
@@ -1,3 +0,0 @@
-This directory contains proof artifacts written by Nathan Chong.
-See the following pull request:
-https://github.com/FreeRTOS/FreeRTOS/pull/836
diff --git a/verification/verifast/proof/single_core_proofs/README.md b/verification/verifast/proof/single_core_proofs/README.md
new file mode 100644
index 000000000..b74905862
--- /dev/null
+++ b/verification/verifast/proof/single_core_proofs/README.md
@@ -0,0 +1,3 @@
+This directory contains proof artifacts written by Aalok Thakkar and Nathan Chong.
+See the following pull request:
+https://github.com/FreeRTOS/FreeRTOS/pull/836
diff --git a/verification/verifast/proof/nathan/list_predicates.h b/verification/verifast/proof/single_core_proofs/list_predicates.h
similarity index 100%
rename from verification/verifast/proof/nathan/list_predicates.h
rename to verification/verifast/proof/single_core_proofs/list_predicates.h
diff --git a/verification/verifast/proof/task_predicates.h b/verification/verifast/proof/task_predicates.h
index df199649c..02fc7c806 100644
--- a/verification/verifast/proof/task_predicates.h
+++ b/verification/verifast/proof/task_predicates.h
@@ -2,7 +2,7 @@
 
 #define TASKS_GH
 
-#include "nathan/list_predicates.h"
+#include "single_core_proofs/list_predicates.h"
 
 
 /*@