/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: 29468
Started: 2020-04-28 17:55:59
BEGIN searcher description
DFSSearcher
END searcher description
KLEE: done: Total number of single time Visited Basic Blocks: 140
KLEE: done: Total number of Basic Blocks: 343
Finished: 2020-04-28 17:57:39
Elapsed: 00:01:40
KLEE: done: explored paths = 4054
KLEE: done: avg. constructs per query = 200
KLEE: done: total queries = 4941
KLEE: done: valid queries = 4098
KLEE: done: invalid queries = 826
KLEE: done: query cex = 62
KLEE: done: Total reduced symbolic execution tree nodes = 8107
KLEE: done: Total number of visited basic blocks = 37331

KLEE: done: Subsumption statistics
KLEE: done:     Time for actual solver calls in subsumption check (ms) = 88662.2
KLEE: done:     Number of solver calls for subsumption check (failed) = 4879 (786)
KLEE: done:     Concrete store expression build time (ms) = 309.479
KLEE: done:     Symbolic store expression build time (ms) = 1.496
KLEE: done:     Solver access time (ms) = 91618.6
KLEE: done:     Average table entries per subsumption checkpoint = 71.31
KLEE: done:     Number of subsumption checks = 8092
KLEE: done:     Average solver calls per subsumption check = 0.60

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 47.517
KLEE: done:     remove = 367.432
KLEE: done:     subsumptionCheck = 94901.4
KLEE: done:     markPathCondition = 0.005
KLEE: done:     split = 113.014
KLEE: done:     executeOnNode = 310.183
KLEE: done:     executeMemoryOperation = 1396.78

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 5.553
KLEE: done:     addConstraintTime = 12.191
KLEE: done:     splitTime = 111.67
KLEE: done:     execute = 295.475
KLEE: done:     bindCallArguments = 2.732
KLEE: done:     bindReturnValue = 2.278
KLEE: done:     getStoredExpressions = 98.663
KLEE: done:     getStoredCoreExpressions = 167.803

KLEE: done: total instructions = 202583
KLEE: done: completed paths = 4037, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 19.3548
KLEE: done:     average branching depth of subsumed paths = 18.9264
KLEE: done:     average instructions of completed paths = 551.871
KLEE: done:     average instructions of subsumed paths = 416.239
KLEE: done:     subsumed paths = 4006
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 31
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|  202583|   100.10|    44.87|    30.87|    1491|        0.87|
---------------------------------------------------------------------------------------------------------------------