[2017-09-11 11:46:12,021 INFO  L168              Benchmark]: Toolchain (without parser) took 3690.92 ms. Allocated memory was 356.5 MB in the beginning and 372.8 MB in the end (delta: 16.3 MB). Free memory was 279.1 MB in the beginning and 289.9 MB in the end (delta: -10.8 MB). Peak memory consumption was 68.0 MB. Max. memory is 7.6 GB.
[2017-09-11 11:46:12,021 INFO  L168              Benchmark]: Boogie PL CUP Parser took 0.04 ms. Allocated memory is still 356.5 MB. Free memory was 280.8 MB in the beginning and 280.8 MB in the end (delta: 29.8 kB). Peak memory consumption was 29.8 kB. Max. memory is 7.6 GB.
[2017-09-11 11:46:12,022 INFO  L168              Benchmark]: Boogie Preprocessor took 7.85 ms. Allocated memory is still 356.5 MB. Free memory was 278.9 MB in the beginning and 277.8 MB in the end (delta: 1.1 MB). Peak memory consumption was 1.1 MB. Max. memory is 7.6 GB.
[2017-09-11 11:46:12,022 INFO  L168              Benchmark]: RCFGBuilder took 136.32 ms. Allocated memory is still 356.5 MB. Free memory was 277.7 MB in the beginning and 257.7 MB in the end (delta: 20.0 MB). Peak memory consumption was 20.0 MB. Max. memory is 7.6 GB.
[2017-09-11 11:46:12,022 INFO  L168              Benchmark]: TraceAbstraction took 3543.32 ms. Allocated memory was 356.5 MB in the beginning and 372.8 MB in the end (delta: 16.3 MB). Free memory was 257.5 MB in the beginning and 289.9 MB in the end (delta: -32.4 MB). Peak memory consumption was 46.4 MB. Max. memory is 7.6 GB.
[2017-09-11 11:46:12,022 INFO  L344   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
[2017-09-11 11:46:12,023 INFO  L137             ResultUtil]:  --- Results ---
[2017-09-11 11:46:12,023 INFO  L139             ResultUtil]:  * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
[2017-09-11 11:46:12,023 INFO  L164             ResultUtil]:   - PositiveResult [Line: 195]: assertion always holds
[2017-09-11 11:46:12,023 INFO  L168             ResultUtil]:     For all program executions holds that assertion always holds at this location
[2017-09-11 11:46:12,023 INFO  L164             ResultUtil]:   - PositiveResult [Line: 336]: procedure precondition always holds
[2017-09-11 11:46:12,023 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 11:46:12,023 INFO  L164             ResultUtil]:   - PositiveResult [Line: 211]: assertion always holds
[2017-09-11 11:46:12,023 INFO  L168             ResultUtil]:     For all program executions holds that assertion always holds at this location
[2017-09-11 11:46:12,023 INFO  L164             ResultUtil]:   - PositiveResult [Line: 336]: procedure precondition always holds
[2017-09-11 11:46:12,023 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 11:46:12,023 INFO  L164             ResultUtil]:   - PositiveResult [Line: 336]: procedure precondition always holds
[2017-09-11 11:46:12,023 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 11:46:12,023 INFO  L164             ResultUtil]:   - AllSpecificationsHoldResult: All specifications hold
[2017-09-11 11:46:12,023 INFO  L168             ResultUtil]:     5 specifications checked. All of them hold
[2017-09-11 11:46:12,023 INFO  L164             ResultUtil]:   - InvariantResult [Line: 245]: Loop Invariant
[2017-09-11 11:46:12,024 INFO  L168             ResultUtil]:     Derived loop invariant: ((((((((((((((((((((((((((((!_ATOMIC_HAS_OCCURRED_$$numEigenIntervals && !_READ_HAS_OCCURRED_$$numEigenIntervals) && BV32_SLT(group_id_z$1, num_groups_z)) && v0$2 == BV32_ADD(BV32_MUL(group_id_x$2, group_size_x), local_id_x$2)) && BV32_SGE(local_id_y$2, 0bv32)) && BV32_SGE(group_id_z$2, 0bv32)) && BV32_SGE(group_id_z$1, 0bv32)) && !_WRITE_HAS_OCCURRED_$$numEigenIntervals) && BV32_SLT(group_id_y$2, num_groups_y)) && BV32_SLT(group_id_x$2, num_groups_x)) && v0$1 == BV32_ADD(BV32_MUL(group_id_x$1, group_size_x), local_id_x$1)) && BV32_SLT(local_id_x$2, group_size_x)) && BV32_SLT(group_id_z$2, num_groups_z)) && BV32_SGE(group_id_y$1, 0bv32)) && BV32_SLT(group_id_x$1, num_groups_x)) && BV32_SGE(group_id_y$2, 0bv32)) && BV32_SGE(local_id_y$1, 0bv32)) && BV32_SGE(group_id_x$2, 0bv32)) && BV32_SLT(local_id_x$1, group_size_x)) && BV32_SGE(local_id_x$1, 0bv32)) && BV32_SGE(local_id_x$2, 0bv32)) && BV32_SGE(group_id_x$1, 0bv32)) && (!(local_id_x$1 == local_id_x$2) || !(group_id_x$1 == group_id_x$2))) && BV32_SLT(group_id_y$1, num_groups_y)) && BV32_SGE(local_id_z$1, 0bv32)) && BV32_SLT(local_id_z$1, group_size_z)) && BV32_SLT(local_id_y$1, group_size_y)) && BV32_SGE(local_id_z$2, 0bv32)) && BV32_SLT(local_id_y$2, group_size_y)) && BV32_SLT(local_id_z$2, group_size_z)
[2017-09-11 11:46:12,024 INFO  L164             ResultUtil]:   - InvariantResult [Line: 257]: Loop Invariant
[2017-09-11 11:46:12,025 INFO  L168             ResultUtil]:     Derived loop invariant: ((((((((((((((((((((((((((((!_ATOMIC_HAS_OCCURRED_$$numEigenIntervals && !_READ_HAS_OCCURRED_$$numEigenIntervals) && BV32_SLT(group_id_z$1, num_groups_z)) && v0$2 == BV32_ADD(BV32_MUL(group_id_x$2, group_size_x), local_id_x$2)) && BV32_SGE(local_id_y$2, 0bv32)) && BV32_SGE(group_id_z$2, 0bv32)) && BV32_SGE(group_id_z$1, 0bv32)) && !_WRITE_HAS_OCCURRED_$$numEigenIntervals) && BV32_SLT(group_id_y$2, num_groups_y)) && BV32_SLT(group_id_x$2, num_groups_x)) && v0$1 == BV32_ADD(BV32_MUL(group_id_x$1, group_size_x), local_id_x$1)) && BV32_SLT(local_id_x$2, group_size_x)) && BV32_SLT(group_id_z$2, num_groups_z)) && BV32_SGE(group_id_y$1, 0bv32)) && BV32_SLT(group_id_x$1, num_groups_x)) && BV32_SGE(group_id_y$2, 0bv32)) && BV32_SGE(local_id_y$1, 0bv32)) && BV32_SGE(group_id_x$2, 0bv32)) && BV32_SLT(local_id_x$1, group_size_x)) && BV32_SGE(local_id_x$1, 0bv32)) && BV32_SGE(local_id_x$2, 0bv32)) && BV32_SGE(group_id_x$1, 0bv32)) && (!(local_id_x$1 == local_id_x$2) || !(group_id_x$1 == group_id_x$2))) && BV32_SLT(group_id_y$1, num_groups_y)) && BV32_SGE(local_id_z$1, 0bv32)) && BV32_SLT(local_id_z$1, group_size_z)) && BV32_SLT(local_id_y$1, group_size_y)) && BV32_SGE(local_id_z$2, 0bv32)) && BV32_SLT(local_id_y$2, group_size_y)) && BV32_SLT(local_id_z$2, group_size_z)
[2017-09-11 11:46:12,025 INFO  L164             ResultUtil]:   - InvariantResult [Line: 213]: Loop Invariant
[2017-09-11 11:46:12,025 INFO  L168             ResultUtil]:     Derived loop invariant: ((((((((((((((((((((((((((((!_ATOMIC_HAS_OCCURRED_$$numEigenIntervals && !_READ_HAS_OCCURRED_$$numEigenIntervals) && BV32_SLT(group_id_z$1, num_groups_z)) && v0$2 == BV32_ADD(BV32_MUL(group_id_x$2, group_size_x), local_id_x$2)) && BV32_SGE(local_id_y$2, 0bv32)) && BV32_SGE(group_id_z$2, 0bv32)) && BV32_SGE(group_id_z$1, 0bv32)) && !_WRITE_HAS_OCCURRED_$$numEigenIntervals) && BV32_SLT(group_id_y$2, num_groups_y)) && BV32_SLT(group_id_x$2, num_groups_x)) && v0$1 == BV32_ADD(BV32_MUL(group_id_x$1, group_size_x), local_id_x$1)) && BV32_SLT(local_id_x$2, group_size_x)) && BV32_SLT(group_id_z$2, num_groups_z)) && BV32_SGE(group_id_y$1, 0bv32)) && BV32_SLT(group_id_x$1, num_groups_x)) && BV32_SGE(group_id_y$2, 0bv32)) && BV32_SGE(local_id_y$1, 0bv32)) && BV32_SGE(group_id_x$2, 0bv32)) && BV32_SLT(local_id_x$1, group_size_x)) && BV32_SGE(local_id_x$1, 0bv32)) && BV32_SGE(local_id_x$2, 0bv32)) && BV32_SGE(group_id_x$1, 0bv32)) && (!(local_id_x$1 == local_id_x$2) || !(group_id_x$1 == group_id_x$2))) && BV32_SLT(group_id_y$1, num_groups_y)) && BV32_SGE(local_id_z$1, 0bv32)) && BV32_SLT(local_id_z$1, group_size_z)) && BV32_SLT(local_id_y$1, group_size_y)) && BV32_SGE(local_id_z$2, 0bv32)) && BV32_SLT(local_id_y$2, group_size_y)) && BV32_SLT(local_id_z$2, group_size_z)
[2017-09-11 11:46:12,025 INFO  L164             ResultUtil]:   - InvariantResult [Line: 197]: Loop Invariant
[2017-09-11 11:46:12,026 INFO  L168             ResultUtil]:     Derived loop invariant: ((((((((((((((((((((((((((((!_ATOMIC_HAS_OCCURRED_$$numEigenIntervals && !_READ_HAS_OCCURRED_$$numEigenIntervals) && BV32_SLT(group_id_z$1, num_groups_z)) && v0$2 == BV32_ADD(BV32_MUL(group_id_x$2, group_size_x), local_id_x$2)) && BV32_SGE(local_id_y$2, 0bv32)) && BV32_SGE(group_id_z$2, 0bv32)) && BV32_SGE(group_id_z$1, 0bv32)) && !_WRITE_HAS_OCCURRED_$$numEigenIntervals) && BV32_SLT(group_id_y$2, num_groups_y)) && BV32_SLT(group_id_x$2, num_groups_x)) && v0$1 == BV32_ADD(BV32_MUL(group_id_x$1, group_size_x), local_id_x$1)) && BV32_SLT(local_id_x$2, group_size_x)) && BV32_SLT(group_id_z$2, num_groups_z)) && BV32_SGE(group_id_y$1, 0bv32)) && BV32_SLT(group_id_x$1, num_groups_x)) && BV32_SGE(group_id_y$2, 0bv32)) && BV32_SGE(local_id_y$1, 0bv32)) && BV32_SGE(group_id_x$2, 0bv32)) && BV32_SLT(local_id_x$1, group_size_x)) && BV32_SGE(local_id_x$1, 0bv32)) && BV32_SGE(local_id_x$2, 0bv32)) && BV32_SGE(group_id_x$1, 0bv32)) && (!(local_id_x$1 == local_id_x$2) || !(group_id_x$1 == group_id_x$2))) && BV32_SLT(group_id_y$1, num_groups_y)) && BV32_SGE(local_id_z$1, 0bv32)) && BV32_SLT(local_id_z$1, group_size_z)) && BV32_SLT(local_id_y$1, group_size_y)) && BV32_SGE(local_id_z$2, 0bv32)) && BV32_SLT(local_id_y$2, group_size_y)) && BV32_SLT(local_id_z$2, group_size_z)