MIN_BUDGET definition in sel4test breaks test for TK1

[lsf37]

We introduced a MIN_BUDGET test in https://github.com/seL4/sel4test/commit/b572953ffd41949c15afdfa611de140377dca59f which succeeded for everything tested at the time, but since then the TK1 board has come online.

The TK1 board is defined with a kernel WCET of 100 instead of 10 as most other boards, which affects MIN_BUDGET, which in turn means the MIN_BUDGET here in sel4test is out of sync with the one in seL4.

See eg here for a test failure log.

We either need to define this conditionally in sel4test, which is ugly, but which I will submit as a quick fix for now, or we need to properly export MIN_BUDGET so that sel4test can make use of the value directly.