/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 -debug-subsumption=0 -output-dir=/home/xuanlinhha/TracerX/run-test/output/i367 /home/xuanlinhha/TracerX/run-test/output/i367.bc
PID: 3263
Started: 2020-05-08 10:35:01
BEGIN searcher description
DFSSearcher
END searcher description
KLEE: done: Total number of single time Visited Basic Blocks: 10
KLEE: done: Total number of Basic Blocks: 12
Finished: 2020-05-08 10:35:01
Elapsed: 00:00:00
KLEE: done: explored paths = 260
KLEE: done: avg. constructs per query = 11
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 = 2345

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) = 15.815
KLEE: done:     Symbolic store expression build time (ms) = 0.025
KLEE: done:     Solver access time (ms) = 0.462
KLEE: done:     Average table entries per subsumption checkpoint = 117.00
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 = 3.391
KLEE: done:     remove = 7.168
KLEE: done:     subsumptionCheck = 22.171
KLEE: done:     markPathCondition = 1.242
KLEE: done:     split = 2.445
KLEE: done:     executeOnNode = 8.054
KLEE: done:     executeMemoryOperation = 42.151

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 0.091
KLEE: done:     get WP Interpolant = 1.12
KLEE: done:     addConstraintTime = 5.519
KLEE: done:     splitTime = 1.797
KLEE: done:     execute = 7.289
KLEE: done:     bindCallArguments = 0
KLEE: done:     bindReturnValue = 0
KLEE: done:     getStoredExpressions = 0.802
KLEE: done:     getStoredCoreExpressions = 1.673

KLEE: done: total instructions = 9597
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 = 300.087
KLEE: done:     average instructions of subsumed paths = 237.5
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|    9597|     0.21|    14.15|     8.11|     311|       11.59|
------------------------------------------------------------------------------------------------------------