diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/verifast_RP2040_axioms.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/verifast_RP2040_axioms.h
deleted file mode 100644
index b6dbda41f..000000000
--- a/Test/VeriFast/tasks/vTaskSwitchContext/proof_setup/verifast_RP2040_axioms.h
+++ /dev/null
@@ -1,19 +0,0 @@
-#ifndef VERIFAST_RP2040_AXIOMS_H
-#define VERIFAST_RP2040_AXIOMS_H
-
-#include "stdint.h"
-
-/*
- * The lemmas in this file axiomatize that the RP2040 architecture uses
- * 32bit pointers.
- */
-
-/*@
-// Axiomatizes that: 0 <= ptr <= 2^32 - 1
-lemma void ptr_range(void* ptr);
-requires true;
-ensures (void*) 0 <= ptr &*& ptr <= (void*) 4294967295;
-@*/
-
-
-#endif
\ No newline at end of file
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
index 917960863..045f0c034 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
@@ -78,7 +78,6 @@
     #include "stack_predicates.h"
     #include "task_predicates.h"
     #include "ready_list_predicates.h"
-    #include "verifast_RP2040_axioms.h"
     #include "asm.h"
     #include "port_contracts.h"
     #include "lock_predicates.h"