[ 0:01] + EXTRA_FILES= [ 0:01] + FLAGS= [ 0:01] + . /home/xrockai/src/divine/nightly/test/bricks/4.brick-commandline.bt [ 0:01] + test -z [ 0:01] ++ basename /home/xrockai/src/divine/nightly/test/bricks/4.brick-commandline.bt [ 0:01] ++ sed 's/^[0-9u].\([^.]*\)\..*$/\1/' [ 0:01] + TESTCASE=brick-commandline [ 0:01] + cat [ 0:01] + TESTFILE=/home/xrockai/src/divine/nightly/brick-commandline [ 0:01] + test -f /home/xrockai/src/divine/nightly/brick-commandline [ 0:01] + TESTFILE=/home/xrockai/src/divine/nightly/bricks/brick-commandline [ 0:01] ++ grep 'namespace t_' /home/xrockai/src/divine/nightly/bricks/brick-commandline [ 0:01] ++ sed 's/^.*\(t_[^ ]*\).*$/\1/' [ 0:01] + TESTNS=t_commandline [ 0:01] + divine cc -std=c++14 -DBRICK_UNITTEST_REG -DNVALGRIND -I/home/xrockai/src/divine/nightly/bricks unittest.cpp -o unittest.bc [ 0:01] compiling unittest.cpp [ 0:01] + for NS in $TESTNS [ 0:12] + divine verify --threads 1 -o nofail:malloc unittest.bc t_commandline [ 0:12] + tee verify.out [ 0:12] states per second: 272.602 [ 0:54] state count: 8319 [ 0:54] mips: 0.14 [ 0:54] error found: no [ 0:54] a report was written to unittest.report [ 0:54] + check verify /home/xrockai/src/divine/nightly/test/bricks/4.brick-commandline.bt [ 0:55] + check debris