[ 0:01] + EXTRA_FILES=
[ 0:01] + FLAGS=
[ 0:01] + . /home/xrockai/src/divine/nightly/test/bricks/4.brick-rpc.bt
[ 0:01] + test -z
[ 0:01] ++ basename /home/xrockai/src/divine/nightly/test/bricks/4.brick-rpc.bt
[ 0:01] ++ sed 's/^[0-9u].\([^.]*\)\..*$/\1/'
[ 0:01] + TESTCASE=brick-rpc
[ 0:01] + cat
[ 0:01] + TESTFILE=/home/xrockai/src/divine/nightly/brick-rpc
[ 0:01] + test -f /home/xrockai/src/divine/nightly/brick-rpc
[ 0:01] + TESTFILE=/home/xrockai/src/divine/nightly/bricks/brick-rpc
[ 0:01] ++ grep 'namespace t_' /home/xrockai/src/divine/nightly/bricks/brick-rpc
[ 0:01] ++ sed 's/^.*\(t_[^ ]*\).*$/\1/'
[ 0:01] + TESTNS=t_rpc
[ 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:08] + divine verify --threads 1 -o nofail:malloc unittest.bc t_rpc
[ 0:08] + tee verify.out
[ 0:08] states per second: 260.534
[ 0:35] state count: 4483
[ 0:35] mips: 0.15
[ 0:35] error found: no
[ 0:35] a report was written to unittest.report
[ 0:35] + check verify /home/xrockai/src/divine/nightly/test/bricks/4.brick-rpc.bt
[ 0:36] + check debris