Hey guys,

It seems that sel4test can only run on 1 domian (with CONFIG_NUM_DOMAINS=1 in .config), I tried to set it to 4 or a larger one (<=16) but when I ran the image with qemu it gave me an error "seL4 failed assertion '_ndks_end - _ndks_start <= NDKS_SIZE' at /home/kenneth/sel4/sel4current/kernel/src/arch/ia32/kernel/boot_sys.c:447 in function try_boot_sys". Is there any other configurations or code that I have to change?

PS: I've been suffering a problem that I can only receive devel digests recently but none of your emails could reach me. This is weird because I set no filter in gmail.

Best regards,

Kun Cheng