sel4test: fix SCHED_CONTEXT_0001 budget < MIN_BUDGET does not work

The code uses "1" for budget to supply a value < MIN_BUDGET nothing
checks MIN_BUDGET is > 1. Use MIN_BUDGET - 1 instead.

Bug: 250072589

Change-Id: I1c5a4571bf6dae918e4aeee75bd23b2cd8d71614

apps/sel4test-tests/src/tests/schedcontext.c

diff --git a/apps/sel4test-tests/src/tests/schedcontext.c b/apps/sel4test-tests/src/tests/schedcontext.c
index dedea94..cf79ce8 100644
--- a/apps/sel4test-tests/src/tests/schedcontext.c
+++ b/apps/sel4test-tests/src/tests/schedcontext.c
@@ -56,7 +56,7 @@
     test_eq(error, seL4_RangeError);
 
     /* test budget < MIN_BUDGET doesn't work */
-    error = api_sched_ctrl_configure(simple_get_sched_ctrl(&env->simple, 0), sc, 1, 5000, 0, 0);
+    error = api_sched_ctrl_configure(simple_get_sched_ctrl(&env->simple, 0), sc, MIN_BUDGET_US - 1, 5000, 0, 0);
     test_eq(error, seL4_RangeError);
 
     /* test budget == MIN_BUDGET does work */