2017-09-11 12:30:02,082 INFO  L168              Benchmark]: Toolchain (without parser) took 131400.93 ms. Allocated memory was 739.8 MB in the beginning and 816.3 MB in the end (delta: 76.5 MB). Free memory was 546.6 MB in the beginning and 571.8 MB in the end (delta: -25.2 MB). Peak memory consumption was 335.0 MB. Max. memory is 7.6 GB.
[2017-09-11 12:30:02,082 INFO  L168              Benchmark]: Boogie PL CUP Parser took 0.03 ms. Allocated memory is still 739.8 MB. Free memory is still 546.6 MB. There was no memory consumed. Max. memory is 7.6 GB.
[2017-09-11 12:30:02,083 INFO  L168              Benchmark]: Boogie Preprocessor took 6.29 ms. Allocated memory is still 739.8 MB. Free memory is still 546.6 MB. There was no memory consumed. Max. memory is 7.6 GB.
[2017-09-11 12:30:02,083 INFO  L168              Benchmark]: RCFGBuilder took 261.97 ms. Allocated memory is still 739.8 MB. Free memory was 546.6 MB in the beginning and 491.0 MB in the end (delta: 55.6 MB). Peak memory consumption was 55.6 MB. Max. memory is 7.6 GB.
[2017-09-11 12:30:02,083 INFO  L168              Benchmark]: TraceAbstraction took 131130.03 ms. Allocated memory was 739.8 MB in the beginning and 816.3 MB in the end (delta: 76.5 MB). Free memory was 491.0 MB in the beginning and 571.8 MB in the end (delta: -80.8 MB). Peak memory consumption was 279.5 MB. Max. memory is 7.6 GB.
[2017-09-11 12:30:02,083 INFO  L344   ainManager$Toolchain]: #######################  End [Toolchain 3] #######################
[2017-09-11 12:30:02,084 INFO  L137             ResultUtil]:  --- Results ---
[2017-09-11 12:30:02,084 INFO  L139             ResultUtil]:  * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
[2017-09-11 12:30:02,084 INFO  L164             ResultUtil]:   - PositiveResult [Line: 659]: procedure precondition always holds
[2017-09-11 12:30:02,084 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,084 INFO  L164             ResultUtil]:   - PositiveResult [Line: 436]: procedure precondition always holds
[2017-09-11 12:30:02,084 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,084 INFO  L164             ResultUtil]:   - PositiveResult [Line: 226]: assertion always holds
[2017-09-11 12:30:02,084 INFO  L168             ResultUtil]:     For all program executions holds that assertion always holds at this location
[2017-09-11 12:30:02,084 INFO  L164             ResultUtil]:   - PositiveResult [Line: 827]: procedure precondition always holds
[2017-09-11 12:30:02,084 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,084 INFO  L164             ResultUtil]:   - PositiveResult [Line: 743]: procedure precondition always holds
[2017-09-11 12:30:02,085 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,085 INFO  L164             ResultUtil]:   - PositiveResult [Line: 341]: assertion always holds
[2017-09-11 12:30:02,085 INFO  L168             ResultUtil]:     For all program executions holds that assertion always holds at this location
[2017-09-11 12:30:02,085 INFO  L164             ResultUtil]:   - PositiveResult [Line: 743]: procedure precondition always holds
[2017-09-11 12:30:02,085 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,085 INFO  L164             ResultUtil]:   - PositiveResult [Line: 743]: procedure precondition always holds
[2017-09-11 12:30:02,085 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,085 INFO  L164             ResultUtil]:   - PositiveResult [Line: 443]: procedure precondition always holds
[2017-09-11 12:30:02,085 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,085 INFO  L164             ResultUtil]:   - PositiveResult [Line: 827]: procedure precondition always holds
[2017-09-11 12:30:02,085 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,085 INFO  L164             ResultUtil]:   - PositiveResult [Line: 827]: procedure precondition always holds
[2017-09-11 12:30:02,086 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,086 INFO  L164             ResultUtil]:   - PositiveResult [Line: 659]: procedure precondition always holds
[2017-09-11 12:30:02,086 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,086 INFO  L164             ResultUtil]:   - PositiveResult [Line: 827]: procedure precondition always holds
[2017-09-11 12:30:02,086 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,086 INFO  L164             ResultUtil]:   - PositiveResult [Line: 743]: procedure precondition always holds
[2017-09-11 12:30:02,086 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,086 INFO  L164             ResultUtil]:   - PositiveResult [Line: 224]: assertion always holds
[2017-09-11 12:30:02,086 INFO  L168             ResultUtil]:     For all program executions holds that assertion always holds at this location
[2017-09-11 12:30:02,086 INFO  L164             ResultUtil]:   - PositiveResult [Line: 743]: procedure precondition always holds
[2017-09-11 12:30:02,086 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,086 INFO  L164             ResultUtil]:   - PositiveResult [Line: 659]: procedure precondition always holds
[2017-09-11 12:30:02,086 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,087 INFO  L164             ResultUtil]:   - PositiveResult [Line: 659]: procedure precondition always holds
[2017-09-11 12:30:02,087 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,087 INFO  L164             ResultUtil]:   - PositiveResult [Line: 340]: assertion always holds
[2017-09-11 12:30:02,087 INFO  L168             ResultUtil]:     For all program executions holds that assertion always holds at this location
[2017-09-11 12:30:02,087 INFO  L164             ResultUtil]:   - PositiveResult [Line: 743]: procedure precondition always holds
[2017-09-11 12:30:02,087 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,087 INFO  L164             ResultUtil]:   - PositiveResult [Line: 827]: procedure precondition always holds
[2017-09-11 12:30:02,087 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,087 INFO  L164             ResultUtil]:   - PositiveResult [Line: 343]: assertion always holds
[2017-09-11 12:30:02,087 INFO  L168             ResultUtil]:     For all program executions holds that assertion always holds at this location
[2017-09-11 12:30:02,087 INFO  L164             ResultUtil]:   - PositiveResult [Line: 827]: procedure precondition always holds
[2017-09-11 12:30:02,087 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,087 INFO  L164             ResultUtil]:   - PositiveResult [Line: 659]: procedure precondition always holds
[2017-09-11 12:30:02,087 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,087 INFO  L164             ResultUtil]:   - PositiveResult [Line: 827]: procedure precondition always holds
[2017-09-11 12:30:02,088 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,088 INFO  L164             ResultUtil]:   - PositiveResult [Line: 743]: procedure precondition always holds
[2017-09-11 12:30:02,088 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,088 INFO  L164             ResultUtil]:   - PositiveResult [Line: 342]: assertion always holds
[2017-09-11 12:30:02,088 INFO  L168             ResultUtil]:     For all program executions holds that assertion always holds at this location
[2017-09-11 12:30:02,088 INFO  L164             ResultUtil]:   - PositiveResult [Line: 659]: procedure precondition always holds
[2017-09-11 12:30:02,088 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,088 INFO  L164             ResultUtil]:   - PositiveResult [Line: 743]: procedure precondition always holds
[2017-09-11 12:30:02,088 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,089 INFO  L164             ResultUtil]:   - PositiveResult [Line: 827]: procedure precondition always holds
[2017-09-11 12:30:02,089 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,089 INFO  L164             ResultUtil]:   - PositiveResult [Line: 743]: procedure precondition always holds
[2017-09-11 12:30:02,089 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,089 INFO  L164             ResultUtil]:   - PositiveResult [Line: 225]: assertion always holds
[2017-09-11 12:30:02,089 INFO  L168             ResultUtil]:     For all program executions holds that assertion always holds at this location
[2017-09-11 12:30:02,089 INFO  L164             ResultUtil]:   - PositiveResult [Line: 659]: procedure precondition always holds
[2017-09-11 12:30:02,089 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,089 INFO  L164             ResultUtil]:   - PositiveResult [Line: 227]: assertion always holds
[2017-09-11 12:30:02,089 INFO  L168             ResultUtil]:     For all program executions holds that assertion always holds at this location
[2017-09-11 12:30:02,090 INFO  L164             ResultUtil]:   - PositiveResult [Line: 743]: procedure precondition always holds
[2017-09-11 12:30:02,090 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,090 INFO  L164             ResultUtil]:   - PositiveResult [Line: 659]: procedure precondition always holds
[2017-09-11 12:30:02,090 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,090 INFO  L164             ResultUtil]:   - PositiveResult [Line: 827]: procedure precondition always holds
[2017-09-11 12:30:02,090 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,090 INFO  L164             ResultUtil]:   - PositiveResult [Line: 743]: procedure precondition always holds
[2017-09-11 12:30:02,090 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,090 INFO  L164             ResultUtil]:   - PositiveResult [Line: 827]: procedure precondition always holds
[2017-09-11 12:30:02,090 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,090 INFO  L164             ResultUtil]:   - PositiveResult [Line: 659]: procedure precondition always holds
[2017-09-11 12:30:02,090 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,090 INFO  L164             ResultUtil]:   - PositiveResult [Line: 827]: procedure precondition always holds
[2017-09-11 12:30:02,090 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,090 INFO  L164             ResultUtil]:   - PositiveResult [Line: 659]: procedure precondition always holds
[2017-09-11 12:30:02,090 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,090 INFO  L164             ResultUtil]:   - PositiveResult [Line: 743]: procedure precondition always holds
[2017-09-11 12:30:02,090 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,090 INFO  L164             ResultUtil]:   - PositiveResult [Line: 659]: procedure precondition always holds
[2017-09-11 12:30:02,090 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,091 INFO  L164             ResultUtil]:   - PositiveResult [Line: 827]: procedure precondition always holds
[2017-09-11 12:30:02,091 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,091 INFO  L164             ResultUtil]:   - PositiveResult [Line: 436]: procedure precondition always holds
[2017-09-11 12:30:02,091 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,091 INFO  L164             ResultUtil]:   - PositiveResult [Line: 443]: procedure precondition always holds
[2017-09-11 12:30:02,091 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,091 INFO  L164             ResultUtil]:   - PositiveResult [Line: 659]: procedure precondition always holds
[2017-09-11 12:30:02,091 INFO  L168             ResultUtil]:     For all program executions holds that procedure precondition always holds at this location
[2017-09-11 12:30:02,091 INFO  L164             ResultUtil]:   - AllSpecificationsHoldResult: All specifications hold
[2017-09-11 12:30:02,091 INFO  L168             ResultUtil]:     48 specifications checked. All of them hold
[2017-09-11 12:30:02,091 INFO  L164             ResultUtil]:   - InvariantResult [Line: 886]: Loop Invariant
[2017-09-11 12:30:02,092 INFO  L168             ResultUtil]:     Derived loop invariant: (((((((((((((((((((((((((((((((_READ_HAS_OCCURRED_$$localPos || !BV32_SLT(group_id_z$1, num_groups_z)) || !BV32_SGE(local_id_y$2, 0bv32)) || _ATOMIC_HAS_OCCURRED_$$newVelocity) || !BV32_SGE(group_id_z$2, 0bv32)) || _WRITE_HAS_OCCURRED_$$newVelocity) || !BV32_SGE(group_id_z$1, 0bv32)) || !BV32_SLT(group_id_y$2, num_groups_y)) || _WRITE_HAS_OCCURRED_$$newPosition) || !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)) || _ATOMIC_HAS_OCCURRED_$$newPosition) || !BV32_SGE(local_id_x$2, 0bv32)) || ((((!(_WATCHED_OFFSET == BV32_MUL(4bv32, local_id_x$1)) || !(group_id_x$1 == group_id_x$2)) && (!(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 3bv32)) || !(group_id_x$1 == group_id_x$2))) && (!(group_id_x$1 == group_id_x$2) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 1bv32)))) && (!(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 2bv32)) || !(group_id_x$1 == group_id_x$2)))) || _ATOMIC_HAS_OCCURRED_$$localPos) || local_id_x$1 == local_id_x$2) || !BV32_SLT(group_id_y$1, num_groups_y)) || _READ_HAS_OCCURRED_$$newVelocity) || !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)) || _READ_HAS_OCCURRED_$$newPosition) || !BV32_SLT(local_id_z$2, group_size_z)) || $0 == 0bv1 || !_WRITE_HAS_OCCURRED_$$localPos
[2017-09-11 12:30:02,092 INFO  L164             ResultUtil]:   - InvariantResult [Line: 930]: Loop Invariant
[2017-09-11 12:30:02,093 INFO  L168             ResultUtil]:     Derived loop invariant: (((((((((((((((((((((((((((_READ_HAS_OCCURRED_$$localPos || !BV32_SGE(local_id_y$2, 0bv32)) || _ATOMIC_HAS_OCCURRED_$$newVelocity) || _WRITE_HAS_OCCURRED_$$newVelocity) || !BV32_SGE(group_id_z$1, 0bv32)) || _WRITE_HAS_OCCURRED_$$newPosition) || !BV32_SLT(local_id_x$2, group_size_x)) || !BV32_SLT(group_id_z$2, num_groups_z)) || !BV32_SLT(group_id_x$1, num_groups_x)) || !BV32_SGE(group_id_y$2, 0bv32)) || !BV32_SGE(local_id_y$1, 0bv32)) || !BV32_SLT(local_id_x$1, group_size_x)) || !BV32_SGE(local_id_x$1, 0bv32)) || _ATOMIC_HAS_OCCURRED_$$newPosition) || !BV32_SGE(local_id_x$2, 0bv32)) || ((((((!(group_id_z$1 == group_id_z$2) || !(_WATCHED_OFFSET == BV32_MUL(4bv32, local_id_x$1))) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2)) && (((!(group_id_z$1 == group_id_z$2) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 3bv32))) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2))) && (((!(group_id_z$1 == group_id_z$2) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2)) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 1bv32)))) && (((!(group_id_z$1 == group_id_z$2) || !(group_id_y$1 == group_id_y$2)) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 2bv32))) || !(group_id_x$1 == group_id_x$2)))) || _ATOMIC_HAS_OCCURRED_$$localPos) || !BV32_SGE(group_id_x$1, 0bv32)) || local_id_x$1 == local_id_x$2) || !BV32_SLT(group_id_y$1, num_groups_y)) || _READ_HAS_OCCURRED_$$newVelocity) || !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)) || _READ_HAS_OCCURRED_$$newPosition) || !BV32_SLT(local_id_z$2, group_size_z)) || $0 == 0bv1 || !_WRITE_HAS_OCCURRED_$$localPos
[2017-09-11 12:30:02,093 INFO  L164             ResultUtil]:   - InvariantResult [Line: 1000]: Loop Invariant
[2017-09-11 12:30:02,093 INFO  L168             ResultUtil]:     Derived loop invariant: true
[2017-09-11 12:30:02,093 INFO  L164             ResultUtil]:   - InvariantResult [Line: 950]: Loop Invariant
[2017-09-11 12:30:02,093 INFO  L168             ResultUtil]:     Derived loop invariant: true
[2017-09-11 12:30:02,093 INFO  L164             ResultUtil]:   - InvariantResult [Line: 349]: Loop Invariant
[2017-09-11 12:30:02,093 INFO  L168             ResultUtil]:     Derived loop invariant: (((((((((((((((((((((((((((((((((((((!_READ_HAS_OCCURRED_$$localPos && BV32_SLT(group_id_z$1, num_groups_z)) && v2 == group_size_x) && local_id_x$2 == v0$2) && BV32_SGE(local_id_y$2, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$newVelocity) && BV32_SGE(group_id_z$2, 0bv32)) && local_id_x$1 == v0$1) && !_WRITE_HAS_OCCURRED_$$newVelocity) && BV32_SGE(group_id_z$1, 0bv32)) && BV32_SLT(group_id_y$2, num_groups_y)) && BV32_SLT(group_id_x$2, num_groups_x)) && !_WRITE_HAS_OCCURRED_$$newPosition) && 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)) && v1$2 == BV32_ADD(BV32_MUL(group_id_x$2, group_size_x), local_id_x$2)) && BV32_SGE(local_id_y$1, 0bv32)) && BV32_SGE(group_id_x$2, 0bv32)) && BV32_SLT(local_id_x$1, group_size_x)) && v1$1 == BV32_ADD(BV32_MUL(group_id_x$1, group_size_x), local_id_x$1)) && BV32_SGE(local_id_x$1, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$newPosition) && BV32_SGE(local_id_x$2, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$localPos) && BV32_SGE(group_id_x$1, 0bv32)) && !_WRITE_HAS_OCCURRED_$$localPos) && (!(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)) && !_READ_HAS_OCCURRED_$$newVelocity) && 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)) && !_READ_HAS_OCCURRED_$$newPosition) && BV32_SLT(local_id_z$2, group_size_z)
[2017-09-11 12:30:02,093 INFO  L164             ResultUtil]:   - InvariantResult [Line: 356]: Loop Invariant
[2017-09-11 12:30:02,094 INFO  L168             ResultUtil]:     Derived loop invariant: (((((((((((((((((((((((((((((((((((((!_READ_HAS_OCCURRED_$$localPos && BV32_SLT(group_id_z$1, num_groups_z)) && v2 == group_size_x) && local_id_x$2 == v0$2) && BV32_SGE(local_id_y$2, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$newVelocity) && BV32_SGE(group_id_z$2, 0bv32)) && local_id_x$1 == v0$1) && !_WRITE_HAS_OCCURRED_$$newVelocity) && BV32_SGE(group_id_z$1, 0bv32)) && BV32_SLT(group_id_y$2, num_groups_y)) && BV32_SLT(group_id_x$2, num_groups_x)) && !_WRITE_HAS_OCCURRED_$$newPosition) && 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)) && v1$2 == BV32_ADD(BV32_MUL(group_id_x$2, group_size_x), local_id_x$2)) && BV32_SGE(local_id_y$1, 0bv32)) && BV32_SGE(group_id_x$2, 0bv32)) && BV32_SLT(local_id_x$1, group_size_x)) && v1$1 == BV32_ADD(BV32_MUL(group_id_x$1, group_size_x), local_id_x$1)) && BV32_SGE(local_id_x$1, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$newPosition) && BV32_SGE(local_id_x$2, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$localPos) && BV32_SGE(group_id_x$1, 0bv32)) && !_WRITE_HAS_OCCURRED_$$localPos) && (!(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)) && !_READ_HAS_OCCURRED_$$newVelocity) && 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)) && !_READ_HAS_OCCURRED_$$newPosition) && BV32_SLT(local_id_z$2, group_size_z)
[2017-09-11 12:30:02,094 INFO  L164             ResultUtil]:   - InvariantResult [Line: 345]: Loop Invariant
[2017-09-11 12:30:02,094 INFO  L168             ResultUtil]:     Derived loop invariant: (((((((((((((((((((((((((((((((((((((!_READ_HAS_OCCURRED_$$localPos && BV32_SLT(group_id_z$1, num_groups_z)) && v2 == group_size_x) && local_id_x$2 == v0$2) && BV32_SGE(local_id_y$2, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$newVelocity) && BV32_SGE(group_id_z$2, 0bv32)) && local_id_x$1 == v0$1) && !_WRITE_HAS_OCCURRED_$$newVelocity) && BV32_SGE(group_id_z$1, 0bv32)) && BV32_SLT(group_id_y$2, num_groups_y)) && BV32_SLT(group_id_x$2, num_groups_x)) && !_WRITE_HAS_OCCURRED_$$newPosition) && 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)) && v1$2 == BV32_ADD(BV32_MUL(group_id_x$2, group_size_x), local_id_x$2)) && BV32_SGE(local_id_y$1, 0bv32)) && BV32_SGE(group_id_x$2, 0bv32)) && BV32_SLT(local_id_x$1, group_size_x)) && v1$1 == BV32_ADD(BV32_MUL(group_id_x$1, group_size_x), local_id_x$1)) && BV32_SGE(local_id_x$1, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$newPosition) && BV32_SGE(local_id_x$2, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$localPos) && BV32_SGE(group_id_x$1, 0bv32)) && !_WRITE_HAS_OCCURRED_$$localPos) && (!(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)) && !_READ_HAS_OCCURRED_$$newVelocity) && 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)) && !_READ_HAS_OCCURRED_$$newPosition) && BV32_SLT(local_id_z$2, group_size_z)
[2017-09-11 12:30:02,094 INFO  L164             ResultUtil]:   - InvariantResult [Line: 975]: Loop Invariant
[2017-09-11 12:30:02,094 INFO  L168             ResultUtil]:     Derived loop invariant: true
[2017-09-11 12:30:02,094 INFO  L164             ResultUtil]:   - InvariantResult [Line: 899]: Loop Invariant
[2017-09-11 12:30:02,095 INFO  L168             ResultUtil]:     Derived loop invariant: (((((((((((((((((((((((((((_READ_HAS_OCCURRED_$$localPos || !BV32_SGE(local_id_y$2, 0bv32)) || _ATOMIC_HAS_OCCURRED_$$newVelocity) || _WRITE_HAS_OCCURRED_$$newVelocity) || !BV32_SGE(group_id_z$1, 0bv32)) || _WRITE_HAS_OCCURRED_$$newPosition) || !BV32_SLT(local_id_x$2, group_size_x)) || !BV32_SLT(group_id_z$2, num_groups_z)) || !BV32_SLT(group_id_x$1, num_groups_x)) || !BV32_SGE(group_id_y$2, 0bv32)) || !BV32_SGE(local_id_y$1, 0bv32)) || !BV32_SLT(local_id_x$1, group_size_x)) || !BV32_SGE(local_id_x$1, 0bv32)) || _ATOMIC_HAS_OCCURRED_$$newPosition) || !BV32_SGE(local_id_x$2, 0bv32)) || ((((((!(group_id_z$1 == group_id_z$2) || !(_WATCHED_OFFSET == BV32_MUL(4bv32, local_id_x$1))) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2)) && (((!(group_id_z$1 == group_id_z$2) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 3bv32))) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2))) && (((!(group_id_z$1 == group_id_z$2) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2)) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 1bv32)))) && (((!(group_id_z$1 == group_id_z$2) || !(group_id_y$1 == group_id_y$2)) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 2bv32))) || !(group_id_x$1 == group_id_x$2)))) || _ATOMIC_HAS_OCCURRED_$$localPos) || !BV32_SGE(group_id_x$1, 0bv32)) || local_id_x$1 == local_id_x$2) || !BV32_SLT(group_id_y$1, num_groups_y)) || _READ_HAS_OCCURRED_$$newVelocity) || !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)) || _READ_HAS_OCCURRED_$$newPosition) || !BV32_SLT(local_id_z$2, group_size_z)) || $0 == 0bv1 || !_WRITE_HAS_OCCURRED_$$localPos
[2017-09-11 12:30:02,095 INFO  L164             ResultUtil]:   - InvariantResult [Line: 921]: Loop Invariant
[2017-09-11 12:30:02,096 INFO  L168             ResultUtil]:     Derived loop invariant: (((((((((((((((((((((((((((_READ_HAS_OCCURRED_$$localPos || !BV32_SGE(local_id_y$2, 0bv32)) || _ATOMIC_HAS_OCCURRED_$$newVelocity) || _WRITE_HAS_OCCURRED_$$newVelocity) || !BV32_SGE(group_id_z$1, 0bv32)) || _WRITE_HAS_OCCURRED_$$newPosition) || !BV32_SLT(local_id_x$2, group_size_x)) || !BV32_SLT(group_id_z$2, num_groups_z)) || !BV32_SLT(group_id_x$1, num_groups_x)) || !BV32_SGE(group_id_y$2, 0bv32)) || !BV32_SGE(local_id_y$1, 0bv32)) || !BV32_SLT(local_id_x$1, group_size_x)) || !BV32_SGE(local_id_x$1, 0bv32)) || _ATOMIC_HAS_OCCURRED_$$newPosition) || !BV32_SGE(local_id_x$2, 0bv32)) || ((((((!(group_id_z$1 == group_id_z$2) || !(_WATCHED_OFFSET == BV32_MUL(4bv32, local_id_x$1))) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2)) && (((!(group_id_z$1 == group_id_z$2) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 3bv32))) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2))) && (((!(group_id_z$1 == group_id_z$2) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2)) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 1bv32)))) && (((!(group_id_z$1 == group_id_z$2) || !(group_id_y$1 == group_id_y$2)) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 2bv32))) || !(group_id_x$1 == group_id_x$2)))) || _ATOMIC_HAS_OCCURRED_$$localPos) || !BV32_SGE(group_id_x$1, 0bv32)) || local_id_x$1 == local_id_x$2) || !BV32_SLT(group_id_y$1, num_groups_y)) || _READ_HAS_OCCURRED_$$newVelocity) || !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)) || _READ_HAS_OCCURRED_$$newPosition) || !BV32_SLT(local_id_z$2, group_size_z)) || $0 == 0bv1 || !_WRITE_HAS_OCCURRED_$$localPos
[2017-09-11 12:30:02,096 INFO  L164             ResultUtil]:   - InvariantResult [Line: 995]: Loop Invariant
[2017-09-11 12:30:02,096 INFO  L168             ResultUtil]:     Derived loop invariant: true
[2017-09-11 12:30:02,096 INFO  L164             ResultUtil]:   - InvariantResult [Line: 397]: Loop Invariant
[2017-09-11 12:30:02,097 INFO  L168             ResultUtil]:     Derived loop invariant: (((((((((((((((((((((((((((((((((((((((!_READ_HAS_OCCURRED_$$localPos && BV32_SLT(group_id_z$1, num_groups_z)) && v2 == group_size_x) && local_id_x$2 == v0$2) && BV32_SGE(local_id_y$2, 0bv32)) && $j.0 == 0bv32) && !_ATOMIC_HAS_OCCURRED_$$newVelocity) && BV32_SGE(group_id_z$2, 0bv32)) && local_id_x$1 == v0$1) && !_WRITE_HAS_OCCURRED_$$newVelocity) && BV32_SGE(group_id_z$1, 0bv32)) && BV32_SLT(group_id_y$2, num_groups_y)) && BV32_SLT(group_id_x$2, num_groups_x)) && !_WRITE_HAS_OCCURRED_$$newPosition) && 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)) && v1$2 == BV32_ADD(BV32_MUL(group_id_x$2, group_size_x), local_id_x$2)) && BV32_SGE(local_id_y$1, 0bv32)) && BV32_SGE(group_id_x$2, 0bv32)) && BV32_SLT(local_id_x$1, group_size_x)) && v1$1 == BV32_ADD(BV32_MUL(group_id_x$1, group_size_x), local_id_x$1)) && BV32_SGE(local_id_x$1, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$newPosition) && BV32_SGE(local_id_x$2, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$localPos) && BV32_SGE(group_id_x$1, 0bv32)) && !_WRITE_HAS_OCCURRED_$$localPos) && (!(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)) && !_READ_HAS_OCCURRED_$$newVelocity) && 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)) && !_READ_HAS_OCCURRED_$$newPosition) && BV32_SLT(local_id_z$2, group_size_z)) || (((((((((((((((((((((((((((((((((((((((!_READ_HAS_OCCURRED_$$localPos && BV32_SLT(group_id_z$1, num_groups_z)) && v2 == group_size_x) && local_id_x$2 == v0$2) && BV32_SGE(local_id_y$2, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$newVelocity) && BV32_SGE(group_id_z$2, 0bv32)) && local_id_x$1 == v0$1) && !_WRITE_HAS_OCCURRED_$$newVelocity) && BV32_SGE(group_id_z$1, 0bv32)) && BV32_SLT(group_id_y$2, num_groups_y)) && BV32_SLT(group_id_x$2, num_groups_x)) && !_WRITE_HAS_OCCURRED_$$newPosition) && 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)) && v1$2 == BV32_ADD(BV32_MUL(group_id_x$2, group_size_x), local_id_x$2)) && BV32_SGE(local_id_y$1, 0bv32)) && BV32_SGE(group_id_x$2, 0bv32)) && BV32_SLT(local_id_x$1, group_size_x)) && v1$1 == BV32_ADD(BV32_MUL(group_id_x$1, group_size_x), local_id_x$1)) && BV32_SGE(local_id_x$1, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$newPosition) && BV32_SGE(local_id_x$2, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$localPos) && BV32_SGE(group_id_x$1, 0bv32)) && !_WRITE_HAS_OCCURRED_$$localPos) && (!(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)) && !_READ_HAS_OCCURRED_$$newVelocity) && BV32_SGE(local_id_z$1, 0bv32)) && BV32_SLT(local_id_z$1, group_size_z)) && v12) && 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)) && !_READ_HAS_OCCURRED_$$newPosition) && BV32_SLT(local_id_z$2, group_size_z))
[2017-09-11 12:30:02,097 INFO  L164             ResultUtil]:   - InvariantResult [Line: 956]: Loop Invariant
[2017-09-11 12:30:02,097 INFO  L168             ResultUtil]:     Derived loop invariant: true
[2017-09-11 12:30:02,097 INFO  L164             ResultUtil]:   - InvariantResult [Line: 880]: Loop Invariant
[2017-09-11 12:30:02,098 INFO  L168             ResultUtil]:     Derived loop invariant: true
[2017-09-11 12:30:02,098 INFO  L164             ResultUtil]:   - InvariantResult [Line: 934]: Loop Invariant
[2017-09-11 12:30:02,098 INFO  L168             ResultUtil]:     Derived loop invariant: (((((((((((((((((((((((((((_READ_HAS_OCCURRED_$$localPos || !BV32_SGE(local_id_y$2, 0bv32)) || _ATOMIC_HAS_OCCURRED_$$newVelocity) || _WRITE_HAS_OCCURRED_$$newVelocity) || !BV32_SGE(group_id_z$1, 0bv32)) || _WRITE_HAS_OCCURRED_$$newPosition) || !BV32_SLT(local_id_x$2, group_size_x)) || !BV32_SLT(group_id_z$2, num_groups_z)) || !BV32_SLT(group_id_x$1, num_groups_x)) || !BV32_SGE(group_id_y$2, 0bv32)) || !BV32_SGE(local_id_y$1, 0bv32)) || !BV32_SLT(local_id_x$1, group_size_x)) || !BV32_SGE(local_id_x$1, 0bv32)) || _ATOMIC_HAS_OCCURRED_$$newPosition) || !BV32_SGE(local_id_x$2, 0bv32)) || ((((((!(group_id_z$1 == group_id_z$2) || !(_WATCHED_OFFSET == BV32_MUL(4bv32, local_id_x$1))) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2)) && (((!(group_id_z$1 == group_id_z$2) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 3bv32))) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2))) && (((!(group_id_z$1 == group_id_z$2) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2)) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 1bv32)))) && (((!(group_id_z$1 == group_id_z$2) || !(group_id_y$1 == group_id_y$2)) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 2bv32))) || !(group_id_x$1 == group_id_x$2)))) || _ATOMIC_HAS_OCCURRED_$$localPos) || !BV32_SGE(group_id_x$1, 0bv32)) || local_id_x$1 == local_id_x$2) || !BV32_SLT(group_id_y$1, num_groups_y)) || _READ_HAS_OCCURRED_$$newVelocity) || !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)) || _READ_HAS_OCCURRED_$$newPosition) || !BV32_SLT(local_id_z$2, group_size_z)) || $0 == 0bv1 || !_WRITE_HAS_OCCURRED_$$localPos
[2017-09-11 12:30:02,099 INFO  L164             ResultUtil]:   - InvariantResult [Line: 1004]: Loop Invariant
[2017-09-11 12:30:02,099 INFO  L168             ResultUtil]:     Derived loop invariant: true
[2017-09-11 12:30:02,099 INFO  L164             ResultUtil]:   - InvariantResult [Line: 905]: Loop Invariant
[2017-09-11 12:30:02,099 INFO  L168             ResultUtil]:     Derived loop invariant: (((((((((((((((((((((((((((_READ_HAS_OCCURRED_$$localPos || !BV32_SGE(local_id_y$2, 0bv32)) || _ATOMIC_HAS_OCCURRED_$$newVelocity) || _WRITE_HAS_OCCURRED_$$newVelocity) || !BV32_SGE(group_id_z$1, 0bv32)) || _WRITE_HAS_OCCURRED_$$newPosition) || !BV32_SLT(local_id_x$2, group_size_x)) || !BV32_SLT(group_id_z$2, num_groups_z)) || !BV32_SLT(group_id_x$1, num_groups_x)) || !BV32_SGE(group_id_y$2, 0bv32)) || !BV32_SGE(local_id_y$1, 0bv32)) || !BV32_SLT(local_id_x$1, group_size_x)) || !BV32_SGE(local_id_x$1, 0bv32)) || _ATOMIC_HAS_OCCURRED_$$newPosition) || !BV32_SGE(local_id_x$2, 0bv32)) || ((((((!(group_id_z$1 == group_id_z$2) || !(_WATCHED_OFFSET == BV32_MUL(4bv32, local_id_x$1))) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2)) && (((!(group_id_z$1 == group_id_z$2) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 3bv32))) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2))) && (((!(group_id_z$1 == group_id_z$2) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2)) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 1bv32)))) && (((!(group_id_z$1 == group_id_z$2) || !(group_id_y$1 == group_id_y$2)) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 2bv32))) || !(group_id_x$1 == group_id_x$2)))) || _ATOMIC_HAS_OCCURRED_$$localPos) || !BV32_SGE(group_id_x$1, 0bv32)) || local_id_x$1 == local_id_x$2) || !BV32_SLT(group_id_y$1, num_groups_y)) || _READ_HAS_OCCURRED_$$newVelocity) || !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)) || _READ_HAS_OCCURRED_$$newPosition) || !BV32_SLT(local_id_z$2, group_size_z)) || $0 == 0bv1 || !_WRITE_HAS_OCCURRED_$$localPos
[2017-09-11 12:30:02,099 INFO  L164             ResultUtil]:   - InvariantResult [Line: 229]: Loop Invariant
[2017-09-11 12:30:02,100 INFO  L168             ResultUtil]:     Derived loop invariant: (((((((((((((((((((((((((((((((((((((!_READ_HAS_OCCURRED_$$localPos && BV32_SLT(group_id_z$1, num_groups_z)) && v2 == group_size_x) && local_id_x$2 == v0$2) && BV32_SGE(local_id_y$2, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$newVelocity) && BV32_SGE(group_id_z$2, 0bv32)) && local_id_x$1 == v0$1) && !_WRITE_HAS_OCCURRED_$$newVelocity) && BV32_SGE(group_id_z$1, 0bv32)) && BV32_SLT(group_id_y$2, num_groups_y)) && BV32_SLT(group_id_x$2, num_groups_x)) && !_WRITE_HAS_OCCURRED_$$newPosition) && 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)) && v1$2 == BV32_ADD(BV32_MUL(group_id_x$2, group_size_x), local_id_x$2)) && BV32_SGE(local_id_y$1, 0bv32)) && BV32_SGE(group_id_x$2, 0bv32)) && BV32_SLT(local_id_x$1, group_size_x)) && v1$1 == BV32_ADD(BV32_MUL(group_id_x$1, group_size_x), local_id_x$1)) && BV32_SGE(local_id_x$1, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$newPosition) && BV32_SGE(local_id_x$2, 0bv32)) && BV32_SGE(group_id_x$1, 0bv32)) && !_WRITE_HAS_OCCURRED_$$localPos) && (!(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)) && !_READ_HAS_OCCURRED_$$newVelocity) && BV32_SGE(local_id_z$1, 0bv32)) && BV32_SLT(local_id_z$1, group_size_z)) && !_ATOMIC_HAS_OCCURRED_$$localPos) && 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)) && !_READ_HAS_OCCURRED_$$newPosition) && BV32_SLT(local_id_z$2, group_size_z)
[2017-09-11 12:30:02,100 INFO  L164             ResultUtil]:   - InvariantResult [Line: 329]: Loop Invariant
[2017-09-11 12:30:02,100 INFO  L168             ResultUtil]:     Derived loop invariant: (((((((((((((((((((((((((((((((((((((!_READ_HAS_OCCURRED_$$localPos && BV32_SLT(group_id_z$1, num_groups_z)) && v2 == group_size_x) && local_id_x$2 == v0$2) && BV32_SGE(local_id_y$2, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$newVelocity) && BV32_SGE(group_id_z$2, 0bv32)) && local_id_x$1 == v0$1) && !_WRITE_HAS_OCCURRED_$$newVelocity) && BV32_SGE(group_id_z$1, 0bv32)) && BV32_SLT(group_id_y$2, num_groups_y)) && BV32_SLT(group_id_x$2, num_groups_x)) && !_WRITE_HAS_OCCURRED_$$newPosition) && 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)) && v1$2 == BV32_ADD(BV32_MUL(group_id_x$2, group_size_x), local_id_x$2)) && BV32_SGE(local_id_y$1, 0bv32)) && BV32_SGE(group_id_x$2, 0bv32)) && BV32_SLT(local_id_x$1, group_size_x)) && v1$1 == BV32_ADD(BV32_MUL(group_id_x$1, group_size_x), local_id_x$1)) && BV32_SGE(local_id_x$1, 0bv32)) && !_ATOMIC_HAS_OCCURRED_$$newPosition) && BV32_SGE(local_id_x$2, 0bv32)) && (((((_WATCHED_OFFSET == BV32_MUL(4bv32, local_id_x$1) && group_id_x$1 == group_id_x$2) || (_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 3bv32) && group_id_x$1 == group_id_x$2)) || (group_id_x$1 == group_id_x$2 && _WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 1bv32))) || (_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 2bv32) && group_id_x$1 == group_id_x$2)) || !_WRITE_HAS_OCCURRED_$$localPos)) && !_ATOMIC_HAS_OCCURRED_$$localPos) && 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)) && !_READ_HAS_OCCURRED_$$newVelocity) && 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)) && !_READ_HAS_OCCURRED_$$newPosition) && BV32_SLT(local_id_z$2, group_size_z)
[2017-09-11 12:30:02,100 INFO  L164             ResultUtil]:   - InvariantResult [Line: 872]: Loop Invariant
[2017-09-11 12:30:02,100 INFO  L168             ResultUtil]:     Derived loop invariant: true
[2017-09-11 12:30:02,100 INFO  L164             ResultUtil]:   - InvariantResult [Line: 991]: Loop Invariant
[2017-09-11 12:30:02,100 INFO  L168             ResultUtil]:     Derived loop invariant: true
[2017-09-11 12:30:02,100 INFO  L164             ResultUtil]:   - InvariantResult [Line: 969]: Loop Invariant
[2017-09-11 12:30:02,101 INFO  L168             ResultUtil]:     Derived loop invariant: true
[2017-09-11 12:30:02,101 INFO  L164             ResultUtil]:   - InvariantResult [Line: 942]: Loop Invariant
[2017-09-11 12:30:02,101 INFO  L168             ResultUtil]:     Derived loop invariant: true
[2017-09-11 12:30:02,101 INFO  L164             ResultUtil]:   - InvariantResult [Line: 925]: Loop Invariant
[2017-09-11 12:30:02,101 INFO  L168             ResultUtil]:     Derived loop invariant: (((((((((((((((((((((((((((_READ_HAS_OCCURRED_$$localPos || !BV32_SGE(local_id_y$2, 0bv32)) || _ATOMIC_HAS_OCCURRED_$$newVelocity) || _WRITE_HAS_OCCURRED_$$newVelocity) || !BV32_SGE(group_id_z$1, 0bv32)) || _WRITE_HAS_OCCURRED_$$newPosition) || !BV32_SLT(local_id_x$2, group_size_x)) || !BV32_SLT(group_id_z$2, num_groups_z)) || !BV32_SLT(group_id_x$1, num_groups_x)) || !BV32_SGE(group_id_y$2, 0bv32)) || !BV32_SGE(local_id_y$1, 0bv32)) || !BV32_SLT(local_id_x$1, group_size_x)) || !BV32_SGE(local_id_x$1, 0bv32)) || _ATOMIC_HAS_OCCURRED_$$newPosition) || !BV32_SGE(local_id_x$2, 0bv32)) || ((((((!(group_id_z$1 == group_id_z$2) || !(_WATCHED_OFFSET == BV32_MUL(4bv32, local_id_x$1))) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2)) && (((!(group_id_z$1 == group_id_z$2) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 3bv32))) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2))) && (((!(group_id_z$1 == group_id_z$2) || !(group_id_y$1 == group_id_y$2)) || !(group_id_x$1 == group_id_x$2)) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 1bv32)))) && (((!(group_id_z$1 == group_id_z$2) || !(group_id_y$1 == group_id_y$2)) || !(_WATCHED_OFFSET == BV32_ADD(BV32_MUL(4bv32, local_id_x$1), 2bv32))) || !(group_id_x$1 == group_id_x$2)))) || _ATOMIC_HAS_OCCURRED_$$localPos) || !BV32_SGE(group_id_x$1, 0bv32)) || local_id_x$1 == local_id_x$2) || !BV32_SLT(group_id_y$1, num_groups_y)) || _READ_HAS_OCCURRED_$$newVelocity) || !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)) || _READ_HAS_OCCURRED_$$newPosition) || !BV32_SLT(local_id_z$2, group_size_z)) || $0 == 0bv1 || !_WRITE_HAS_OCCURRED_$$localPos
[2017-09-11 12:30:02,101 INFO  L164             ResultUtil]:   - StatisticsResult: Ultimate Automizer benchmark data
[2017-09-11 12:30:02,102 INFO  L168             ResultUtil]:     CFG has 23 procedures, 210 locations, 48 error locations. SAFE Result, 131.1s OverallTime, 32 OverallIterations, 10 TraceHistogramMax, 52.2s AutomataDifference, 0.0s DeadEndRemovalTime, 28.0s HoareAnnotationTime, HoareTripleCheckerStatistics: 3760 SDtfs, 4535 SDslu, 9207 SDs, 0 SdLazy, 7595 SolverSat, 1577 SolverUnsat, 0 SolverUnknown, 0 SolverNotchecked, 27.2s Time, PredicateUnifierStatistics: 0 DeclaredPredicates, 2679 GetRequests, 2279 SyntacticMatches, 53 SemanticMatches, 347 ConstructedPredicates, 0 IntricatePredicates, 0 DeprecatedPredicates, 1039 ImplicationChecksByTransitivity, 49.2s Time, 0.0s BasicInterpolantAutomatonTime, BiggestAbstraction: size=273occurred in iteration=31, TraceCheckerStatistics: 0.3s SsaConstructionTime, 2.0s SatisfiabilityAnalysisTime, 39.2s InterpolantComputationTime, 2597 NumberOfCodeBlocks, 2372 NumberOfCodeBlocksAsserted, 43 NumberOfCheckSat, 2565 ConstructedInterpolants, 0 QuantifiedInterpolants, 9748908 SizeOfPredicates, 150 NumberOfNonLiveVariables, 7467 ConjunctsInSsa, 681 ConjunctsInUnsatCore, 32 InterpolantComputations, 11 PerfectInterpolantSequences, 2440/3292 InterpolantCoveringCapability, InterpolantConsolidationStatistics: No data available, PathInvariantsStatistics: No data available, 0/0 InterpolantCoveringCapability, TotalInterpolationStatistics: No data available, 0.0s AbstIntTime, 0 AbstIntIterations, 0 AbstIntStrong, AutomataMinimizationStatistics: 7.8s AutomataMinimizationTime, 32 MinimizatonAttempts, 544 StatesRemovedByMinimization, 20 NontrivialMinimizations, HoareAnnotationStatistics: 0.0s HoareAnnotationTime, 56 LocationsWithAnnotation, 498 PreInvPairs, 565 NumberOfFragments, 6460 HoareAnnotationTreeSize, 498 FomulaSimplifications, 355517 FormulaSimplificationTreeSizeReduction, 0.9s HoareSimplificationTime, 56 FomulaSimplificationsInter, 262036 FormulaSimplificationTreeSizeReductionInter, 27.0s HoareSimplificationTimeInter