diff --git a/apps/sel4test-tests/src/tests/fpu.c b/apps/sel4test-tests/src/tests/fpu.c
index bafad72b..5e167bb4 100644
--- a/apps/sel4test-tests/src/tests/fpu.c
+++ b/apps/sel4test-tests/src/tests/fpu.c
@@ -187,4 +187,4 @@ int smp_test_fpu(env_t env)
     return sel4test_get_result();
 }
 DEFINE_TEST(FPU0002, "Test FPU remain valid across core migration", smp_test_fpu,
-            config_set(CONFIG_MAX_NUM_NODES) &&config_set(CONFIG_HAVE_TIMER) &&CONFIG_MAX_NUM_NODES > 1)
+            config_set(CONFIG_HAVE_TIMER) &&(CONFIG_MAX_NUM_NODES > 1))
diff --git a/apps/sel4test-tests/src/tests/ipc.c b/apps/sel4test-tests/src/tests/ipc.c
index e346b056..48cd79f1 100644
--- a/apps/sel4test-tests/src/tests/ipc.c
+++ b/apps/sel4test-tests/src/tests/ipc.c
@@ -1362,5 +1362,5 @@ static int test_sched_donation_cross_core(env_t env)
     return sel4test_get_result();
 }
 DEFINE_TEST(IPC0028, "Cross core sched donation", test_sched_donation_cross_core,
-            config_set(CONFIG_KERNEL_MCS) &&config_set(CONFIG_MAX_NUM_NODES) &&CONFIG_MAX_NUM_NODES > 1);
+            config_set(CONFIG_KERNEL_MCS) &&(CONFIG_MAX_NUM_NODES > 1));
 #endif /* CONFIG_KERNEL_MCS */