/home/xuanlinhha/TracerX/tracerx/Release+Asserts/bin/klee --max-memory=32000 --max-time=100 -solver-backend=z3 --search=dfs -allow-external-sym-calls --watchdog -dump-states-on-halt=0 -write-BB-cov=4 -no-output -spec-strategy=custom -spec-type=coverage -output-dir=/home/xuanlinhha/TracerX/run-test/output/Mpals6-B2-cil /home/xuanlinhha/TracerX/run-test/output/Mpals6-B2-cil.bc
PID: 28475
Started: 2020-04-28 17:48:31
BEGIN searcher description
DFSSearcher
END searcher description
KLEE: done: Total number of single time Visited Basic Blocks: 283
KLEE: done: Total number of Basic Blocks: 343
Finished: 2020-04-28 17:49:28
Elapsed: 00:00:57
KLEE: done: explored paths = 392
KLEE: done: avg. constructs per query = 38
KLEE: done: total queries = 98
KLEE: done: valid queries = 6
KLEE: done: invalid queries = 92
KLEE: done: query cex = 98
KLEE: done: Total reduced symbolic execution tree nodes = 783
KLEE: done: Total number of visited basic blocks = 3204

KLEE: done: Subsumption statistics
KLEE: done:     Time for actual solver calls in subsumption check (ms) = 0
KLEE: done:     Number of solver calls for subsumption check (failed) = 0 (0)
KLEE: done:     Concrete store expression build time (ms) = 0.589
KLEE: done:     Symbolic store expression build time (ms) = 0.027
KLEE: done:     Solver access time (ms) = 0.861
KLEE: done:     Average table entries per subsumption checkpoint = 1.48
KLEE: done:     Number of subsumption checks = 766
KLEE: done:     Average solver calls per subsumption check = 0.00

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 1.33
KLEE: done:     remove = 10.863
KLEE: done:     subsumptionCheck = 6.716
KLEE: done:     markPathCondition = 0.013
KLEE: done:     split = 8.934
KLEE: done:     executeOnNode = 2.28
KLEE: done:     executeMemoryOperation = 51.985

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.055
KLEE: done:     addConstraintTime = 0.591
KLEE: done:     splitTime = 8.829
KLEE: done:     execute = 1.748
KLEE: done:     bindCallArguments = 0.067
KLEE: done:     bindReturnValue = 0.111
KLEE: done:     getStoredExpressions = 2.946
KLEE: done:     getStoredCoreExpressions = 3.845

KLEE: done: total instructions = 8607
KLEE: done: completed paths = 374, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 35.8889
KLEE: done:     average branching depth of subsumed paths = 26.1041
KLEE: done:     average instructions of completed paths = 485.444
KLEE: done:     average instructions of subsumed paths = 283.118
KLEE: done:     subsumed paths = 365
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 9
KLEE: done: generated tests = 0, among which
KLEE: done:     early-terminating tests (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     error tests = 0
KLEE: done:     program exit tests = 0

KLEE: done: NOTE:
KLEE: done:     Subsumed paths / tests counts are nondeterministic for
KLEE: done:     programs with dynamically-allocated memory such as those
KLEE: done:     using malloc, since KLEE may reuse the address of the
KLEE: done:     same malloc calls in different paths. This nondeterminism
KLEE: done:     does not cause loss of error reports.
---------------------------------------------------------------------------------------------------------------------
|                         Path                         |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
---------------------------------------------------------------------------------------------------------------------
|/home/xuanlinhha/TracerX/run-test/output/Mpals6-B2-cil|    8607|    57.24|    82.43|    77.85|    1491|       99.55|
---------------------------------------------------------------------------------------------------------------------