[ 0:00] + cat
[ 0:00] + result=0
[ 0:00] + check_help default
[ 0:00] + divine run -o help -o config:default test.c
[ 0:00] compiling test.c
[ 0:00] + grep 'config: run' trace.out
[ 0:12] - config: run DiOS in a given configuration
[ 0:12] + check_help passthrough
[ 0:12] + divine run -o help -o config:passthrough test.c
[ 0:12] compiling test.c
[ 0:12] + grep 'config: run' trace.out
[ 0:24] - config: run DiOS in a given configuration
[ 0:24] + check_help synchronous
[ 0:24] + divine run -o help -o config:synchronous test.c
[ 0:24] compiling test.c
[ 0:24] + grep 'config: run' trace.out
[ 0:37] - config: run DiOS in a given configuration
[ 0:37] + check_help replay
[ 0:37] + divine run -o help -o config:replay test.c
[ 0:37] compiling test.c
[ 0:37] + grep 'config: run' trace.out
[ 0:51] - config: run DiOS in a given configuration
[ 0:51] + exit 0
[ 0:51] + check debris