/home/xuanlinhha/TracerX/tracerx/Release+Asserts/bin/klee -solver-backend=z3 --search=dfs -output-tree -write-pcs -use-query-log=all:pc,all:smt2 -debug-subsumption=0 -debug-state=0 -spec-strategy=custom -spec-type=coverage -output-dir=/home/xuanlinhha/TracerX/run-test/output/sp-bug3 /home/xuanlinhha/TracerX/run-test/output/sp-bug3.bc
PID: 14723
Started: 2020-04-06 12:30:28
BEGIN searcher description
DFSSearcher
END searcher description
Finished: 2020-04-06 12:31:48
Elapsed: 00:01:20
KLEE: done: explored paths = 39016
KLEE: done: avg. constructs per query = 6
KLEE: done: total queries = 50
KLEE: done: valid queries = 0
KLEE: done: invalid queries = 50
KLEE: done: query cex = 50
KLEE: done: Total reduced symbolic execution tree nodes = 78031
KLEE: done: Total number of visited basic blocks = 139059

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) = 12930.3
KLEE: done:     Symbolic store expression build time (ms) = 5.666
KLEE: done:     Solver access time (ms) = 183.105
KLEE: done:     Average table entries per subsumption checkpoint = 418.79
KLEE: done:     Number of subsumption checks = 78031
KLEE: done:     Average solver calls per subsumption check = 0.00

KLEE: done: TxTree method execution times (ms):
KLEE: done:     setCurrentINode = 349.066
KLEE: done:     remove = 2327.39
KLEE: done:     subsumptionCheck = 18884.6
KLEE: done:     markPathCondition = 9.953
KLEE: done:     split = 2042.47
KLEE: done:     executeOnNode = 257.543
KLEE: done:     executeMemoryOperation = 16378.8

KLEE: done: TxTreeNode method execution times (ms):
KLEE: done:     getInterpolant = 11.552
KLEE: done:     addConstraintTime = 682.235
KLEE: done:     splitTime = 1869.26
KLEE: done:     execute = 224.403
KLEE: done:     bindCallArguments = 3.742
KLEE: done:     bindReturnValue = 0.388
KLEE: done:     getStoredExpressions = 1374.02
KLEE: done:     getStoredCoreExpressions = 1285.74

KLEE: done: total instructions = 406495
KLEE: done: completed paths = 39016, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 49
KLEE: done:     average branching depth of subsumed paths = 37.5849
KLEE: done:     average instructions of completed paths = 604.946
KLEE: done:     average instructions of subsumed paths = 484.066
KLEE: done:     subsumed paths = 36570
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 2446
KLEE: done: generated tests = 2446, 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 = 2446

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/sp-bug3|  406495|    79.91|    75.77|    60.47|    1106|       34.97|
---------------------------------------------------------------------------------------------------------------