/home/xuanlinhha/TracerX/tracerx/Release+Asserts/bin/klee -solver-backend=z3 --search=dfs --max-memory=32000 -output-tree --max-time=100 -allow-external-sym-calls --watchdog -dump-states-on-halt=0 -write-BB-cov=4 -no-output -wp-interpolant -output-dir=/home/xuanlinhha/TracerX/run-test/output/i367 /home/xuanlinhha/TracerX/run-test/output/i367.bc
PID: 29770
Started: 2020-05-08 08:44:00
BEGIN searcher description
DFSSearcher
END searcher description
KLEE: done: Total number of single time Visited Basic Blocks: 23
KLEE: done: Total number of Basic Blocks: 25
Finished: 2020-05-08 08:44:00
Elapsed: 00:00:00
KLEE: done: explored paths = 260
KLEE: done: avg. constructs per query = 12
KLEE: done: total queries = 11
KLEE: done: valid queries = 0
KLEE: done: invalid queries = 11
KLEE: done: query cex = 11
KLEE: done: Total reduced symbolic execution tree nodes = 519
KLEE: done: Total number of visited basic blocks = 3822

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.778
KLEE: done:     Symbolic store expression build time (ms) = 0.02
KLEE: done:     Solver access time (ms) = 1.551
KLEE: done:     Average table entries per subsumption checkpoint = 70.20
KLEE: done:     Number of subsumption checks = 519
KLEE: done:     Average solver calls per subsumption check = 0.00

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 7.815
KLEE: done:     remove = 18.467
KLEE: done:     subsumptionCheck = 22.247
KLEE: done:     markPathCondition = 4.272
KLEE: done:     split = 8.328
KLEE: done:     executeOnNode = 18.059
KLEE: done:     executeMemoryOperation = 70.242

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.112
KLEE: done:     get WP Interpolant = 0.887
KLEE: done:     addConstraintTime = 5.882
KLEE: done:     splitTime = 7.602
KLEE: done:     execute = 16.417
KLEE: done:     bindCallArguments = 3.009
KLEE: done:     bindReturnValue = 1.286
KLEE: done:     getStoredExpressions = 6.109
KLEE: done:     getStoredCoreExpressions = 5.491

KLEE: done: total instructions = 22989
KLEE: done: completed paths = 260, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 10
KLEE: done:     average branching depth of subsumed paths = 8.5
KLEE: done:     average instructions of completed paths = 733.543
KLEE: done:     average instructions of subsumed paths = 583.536
KLEE: done:     subsumed paths = 168
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 92
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/i367|   22989|     0.42|    27.22|    16.25|     360|       14.64|
------------------------------------------------------------------------------------------------------------