From 1b0869dac0dc4ae8d1514fe8cc7af61cb487bf50 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Fri, 30 Dec 2022 14:49:00 -0500 Subject: [PATCH] Fixed invalid characters in formula. --- Test/VeriFast/tasks/vTaskSwitchContext/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/README.md b/Test/VeriFast/tasks/vTaskSwitchContext/README.md index f5004f4e4..30d5213de 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/README.md +++ b/Test/VeriFast/tasks/vTaskSwitchContext/README.md @@ -39,8 +39,8 @@ Proof Assumptions: ==> Unbounded memory & thread safety guarantees: - ∀ #tasks. ∀ task interleavings. ∀ interrupt schedules. ∀ data sizes. ∀ cores C1, …, Cn. - vTaskSwitchContext(C1) || … || vTaskSwitchContext(Cn) + ∀ #tasks. ∀ task interleavings. ∀ interrupt schedules. ∀ data sizes. ∀ cores C1, …, Cn. + vTaskSwitchContext(C1) || … || vTaskSwitchContext(Cn) => (no memory error ∧ no race condition) ```