Intermittent "Predicate generation failed" error #27
Description
When running the regression test toh-contract-translation/get-1.c it intermittently fails with
java.lang.Exception: Predicate generation failed
(error "Predicate generation failed")
Other Error: Predicate generation failed
Below are logs from a failing run, and logs from a successful run. Nothing has been changed between them, only some time has passed. It is probably not a TriCera thing, but rather Eldarica or Princess. Issue #17 may or may not be related.
Failing run
../../tri -cex -acsl -log -dev -t:60 get-1.c
---------------------------- Reading C/C++ file --------------------------------
Checked properties:
unreach-call
Warning: no definition of function "non_det_int" available
Warning: no definition of function "non_det_int_ptr" available
Using invariants List(1)
Symmetry clauses: 0
Init clauses: 1
Time elapse clauses: 0
Assertion clauses: 2
Local transition clauses: 2
Local non-interference clauses: 0
Send/receive clauses: 0
Send non-interference clauses: 0
Receive non-interference clauses: 0
Send/receive non-interference clauses: 0
Barrier clauses: 0
Background axiom clauses: 9
------------------------------- Preprocessing ----------------------------------
#clauses #relation syms
Initially: 14 11
After eliminating fwd/bwd unreachable clauses (3ms): 14 11
After partial evaluation (8ms): 14 11
After constraint simplification (20ms): 14 11
After clause inlining (21ms): 5 2
After equality propagation (12ms): 5 2
After constant propagation (17ms): 5 2
After constraint simplification (10ms): 5 2
After clause inlining (1ms): 5 2
After eliminating fwd/bwd unreachable clauses (0ms): 5 2
After slicing (11ms): 5 2
After adding heap size arguments (6ms): 5 2
After equality propagation (2ms): 5 2
After constant propagation (1ms): 5 2
After constraint simplification (8ms): 5 2
After clause inlining (1ms): 5 2
After eliminating fwd/bwd unreachable clauses (0ms): 5 2
After slicing (1ms): 5 2
After Boolean clause splitting (69ms): 5 2
After equality propagation (1ms): 5 2
After constant propagation (0ms): 5 2
After constraint simplification (3ms): 5 2
After clause inlining (0ms): 5 2
After eliminating fwd/bwd unreachable clauses (0ms): 5 2
After slicing (0ms): 5 2
After cloning of relation symbols (5ms): 5 2
After shortening of clauses (1ms): 5 2
Total preprocessing time (ms): 226
------------------------------ Analysing loops ---------------------------------
Loop heads:
get11_16_exp/6 (1 clauses, 10 templates)
get_pre_exp/5 (1 clauses, 7 templates)
----------------------------------- CEGAR --------------------------------------
Theories: Types, ADT(O_Int, O_UInt, O_Addr, O_AddrRange, defObj, AllocResHeap, BatchAllocResHeap, AddrRange), HeapTheory
Constant and interval propagation +++++++++
Unique satisfiable clauses: 5
1 clauses with 0 body literals
3 clauses with 1 body literals
1 clauses with 2 body literals
Starting CEGAR ...
..
Found counterexample #1, refining ... 3 clauses ... 69 -> 68 ... adding predicates:
get11_16_exp: \exists HeapObject v0; \exists int v1, v2; !(get11_16_exp_2_0 = 1 & !(v2 != get11_16_exp_1_0 & read(get11_16_exp_3_0, 1) = v0 & getInt(v0) = v2) & !(v1 != 0 & read(get11_16_exp_3_0, 1) = v0 & HeapObject_ctor(v0) = v1))
..
Found counterexample #2, refining ... 5 clauses ... 127 -> 124 ... adding predicates:
get11_16_exp: get11_16_exp_2_0 != 1, \exists Addr v0; (v0 != get11_16_exp_2_0 & counterAddr(get11_16_exp_3_0) = v0)
get_pre_exp: true, counterAddr(get_pre_exp_0_0) = 1, \exists HeapObject v0, v1; !(get_pre_exp_4_0 = 1 & !(v1 = v0 & read(get_pre_exp_0_0, 1) = v0 & O_Int(get_pre_exp_3_0) = v0))
.....
Found counterexample #3, refining ... 6 clauses ... 140 -> 132 ... adding predicates:
get11_16_exp: get11_16_exp_5_0 = 0, \exists HeapObject v0; \exists int v1, v2; !(get11_16_exp_2_0 = 1 & !(v1 != 0 & read(get11_16_exp_3_0, 1) = v0 & HeapObject_ctor(v0) = v1) & !(0 >= v2 & read(get11_16_exp_3_0, 1) = v0 & getInt(v0) = v2)), \exists Addr v0; \exists HeapObject v1, v2; !(get11_16_exp_5_0 != get11_16_exp_1_0 & !(get11_16_exp_2_0 = 1 & v2 != v1 & read(get11_16_exp_3_0, 1) = v1 & O_Int(get11_16_exp_1_0) = v2) & !(v0 != get11_16_exp_2_0 & counterAddr(get11_16_exp_3_0) = v0))
get_pre_exp: get_pre_exp_4_0 = get_pre_exp_1_0 & counterAddr(get_pre_exp_0_0) = 1, get_pre_exp_4_0 = 1
.....
Found counterexample #4, refining ...
Searching for interpolation abstractions ...
Cost bound: 4
Interpolation abstraction: get11_16_exp: <(1 * _5 + -1 * -1 * _3), (1 * _5 + -1 * 1 * _3)> .
Interpolation abstraction: get11_16_exp: <(1 * _5 + -1 * -1 * _2), (1 * _5 + -1 * -1 * _3)> .
Interpolation abstraction: get11_16_exp: <(1 * _5 + -1 * -1 * _3), (1 * _5 + -1 * 1 * _2)> ...
Interpolation abstraction: get11_16_exp: <(1 * _5 + -1 * -1 * _2), (1 * _5 + -1 * 1 * _3)> .
Interpolation abstraction: get11_16_exp: <(1 * _5 + -1 * 1 * _2), (1 * _5 + -1 * 1 * _3)> .
183 -> 166 183 -> 166 183 -> 166 183 -> 166 183 -> 166 8 clauses ... 179 -> 165 ... adding predicates:
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
get11_16_exp: \exists Addr v0; !(get11_16_exp_4_0 = get11_16_exp_2_0 & !(v0 = get11_16_exp_2_0 & counterAddr(get11_16_exp_3_0) = get11_16_exp_2_0)), \exists int v0; \exists HeapObject v1, v2, v3; !(get11_16_exp_4_0 = get11_16_exp_2_0 & !(counterAddr(get11_16_exp_3_0) = v0 & read(get11_16_exp_3_0, 1) = v2 & O_Int(get11_16_exp_1_0) = v1 & !(v0 = 1 & !(get11_16_exp_2_0 = 1 & !(v3 = v1 & v2 = v1) & !(v2 = v1 & v3 != v1))))), \exists HeapObject v0; \exists int v1, v2; !(get11_16_exp_2_0 = 1 & !(v1 != 0 & read(get11_16_exp_3_0, 1) = v0 & HeapObject_ctor(v0) = v1) & !(read(get11_16_exp_3_0, 1) = v0 & getInt(v0) = v2 & !\exists int v3; (v2 - v3 >= -2 & v3 >= 1 & v2 >= 1 & O_Int(v3 - 1) != v0) & !\exists int v3; (v2 - v3 >= -2 & v2 >= 1 & O_Int(v3 - 1) != v0) & !\exists int v3; (0 >= v3 & v2 >= 1 & O_Int(v3 - 1) != v0) & !\exists int v3; (v3 >= 1 & v2 >= 1 & O_Int(v3 - 1) != v0) & !\exists int v3; (v2 >= 1 & O_Int(v3 - 1) != v0) & !(v2 = 0 & O_Int(0) != v0))), get11_16_exp_5_0 = 1
get_pre_exp: \exists HeapObject v0, v1; (get_pre_exp_4_0 = get_pre_exp_1_0 & !(get_pre_exp_1_0 = 1 & !(v1 = v0 & read(get_pre_exp_0_0, 1) = v0 & O_Int(get_pre_exp_3_0) = v0))), \exists HeapObject v0, v1, v2; (read(get_pre_exp_0_0, 1) = v1 & O_Int(get_pre_exp_3_0 - 1) = v2 & O_Int(get_pre_exp_3_0) = v0 & !\exists HeapObject v3; \forall HeapObject v4; (get_pre_exp_4_0 = 1 & !(v4 = v2 & !(v3 = v2 & v1 = v0 & v2 != v0)))), get_pre_exp_4_0 = get_pre_exp_1_0, get_pre_exp_4_0 = 1 & get_pre_exp_1_0 = 1
.......
Found counterexample #5, refining ...
Searching for interpolation abstractions ...
215 -> 193 9 clauses ... 211 -> 196 ... adding predicates:
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
get11_16_exp: \exists HeapObject v0, v1, v2; (read(get11_16_exp_3_0, 1) = v1 & O_Int(get11_16_exp_1_0) = v0 & !(get11_16_exp_2_0 = 1 & !(v2 != v0 & v1 != v0))), \exists int v0; \exists HeapObject v1; \exists int v2, v3; \exists HeapObject v4; \exists int v5; !(get11_16_exp_2_0 >= 2 & !(v2 != 2 & v2 != 1 & v2 != 0 & 0 >= v5 & 0 >= v3 & read(get11_16_exp_3_0, get11_16_exp_2_0) = v1 & HeapObject_ctor(v1) = v2 & getInt(v4) = v5 & getInt(v1) = v3 & defObj = v4) & !(v2 != 0 & 0 >= v3 & read(get11_16_exp_3_0, get11_16_exp_2_0) = v1 & HeapObject_ctor(v1) = v2 & getInt(v1) = v3) & !(v0 != 1 & counterAddr(get11_16_exp_3_0) = v0)), \exists HeapObject v0; \exists int v1, v2, v3; (read(get11_16_exp_3_0, get11_16_exp_2_0) = v0 & !(!(v1 != 0 & HeapObject_ctor(v0) = v1 & !(get11_16_exp_2_0 >= 2 & !(v3 != 1 & counterAddr(get11_16_exp_3_0) = v3) & !(0 >= v2 & getInt(v0) = v2))) & !(0 >= v2 & getInt(v0) = v2 & !(get11_16_exp_2_0 >= 2 & !(v3 != 1 & counterAddr(get11_16_exp_3_0) = v3))))), \exists HeapObject v0; \exists int v1, v2, v3; (read(get11_16_exp_3_0, get11_16_exp_2_0) = v0 & !(!(v1 != 0 & HeapObject_ctor(v0) = v1 & !(get11_16_exp_2_0 >= 2 & !(v3 != 1 & counterAddr(get11_16_exp_3_0) = v3) & !(0 >= v2 & getInt(v0) = v2))) & !(0 >= v2 & getInt(v0) = v2 & !(v2 >= -1 & !(-1*v2 >= get11_16_exp_5_0 & !(v2 + get11_16_exp_5_0 = 0 & get11_16_exp_5_0 >= 1))) & !(get11_16_exp_2_0 >= 2 & !(v3 != 1 & counterAddr(get11_16_exp_3_0) = v3))))), \exists int v0; \exists HeapObject v1; \exists int v2, v3; !(get11_16_exp_4_0 = 1 & !(get11_16_exp_2_0 = 1 & v2 != 0 & read(get11_16_exp_3_0, 1) = v1 & HeapObject_ctor(v1) = v2) & !(get11_16_exp_2_0 = 1 & 1 >= v3 & read(get11_16_exp_3_0, 1) = v1 & getInt(v1) = v3) & !(v0 != 1 & counterAddr(get11_16_exp_3_0) = v0))
get_pre_exp: \exists HeapObject v0; \exists int v1; (get_pre_exp_4_0 = get_pre_exp_1_0 & !(get_pre_exp_1_0 = 1 & !(v1 - get_pre_exp_3_0 != 1 & read(get_pre_exp_0_0, 1) = v0 & getInt(v0) = v1))), \exists HeapObject v0, v1, v2; (read(get_pre_exp_0_0, 1) = v1 & O_Int(get_pre_exp_3_0) = v0 & !(get_pre_exp_4_0 = 1 & !(v2 != v0 & v1 != v0)))
.........
Found counterexample #6, refining ...
Searching for interpolation abstractions ...
10 clauses ... 243 -> 227 ... adding predicates:
get11_16_exp: \exists HeapObject v0; \exists int v1, v2; \exists HeapObject v3, v4; \exists int v5; (read(get11_16_exp_3_0, 1) = v0 & HeapObject_ctor(v0) = v1 & getInt(v0) = v2 & O_Int(v2 - 1) = v3 & !(v1 = 0 & get11_16_exp_2_0 = 1 & !(v5 - v2 = -1 & v4 = v3 & getInt(v3) = v2 - 1))), \exists int v0; \exists HeapObject v1, v2; !(get11_16_exp_2_0 = 1 & !(v2 != v1 & read(get11_16_exp_3_0, 1) = v1 & O_Int(get11_16_exp_1_0) = v2) & !(v0 != 1 & counterAddr(get11_16_exp_3_0) = v0))
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
get_pre_exp: \exists HeapObject v0; \exists int v1; \exists HeapObject v2; (get_pre_exp_4_0 = get_pre_exp_1_0 & read(get_pre_exp_0_0, 1) = v0 & HeapObject_ctor(v0) = v1 & !\exists int v3; (get_pre_exp_1_0 = 1 & v1 != 0 & O_Int(v3 - 1) != v2) & !(get_pre_exp_1_0 = 1 & v2 != v0) & !(get_pre_exp_1_0 = 1 & v1 != 0) & !(get_pre_exp_1_0 = 1 & O_Int(get_pre_exp_3_0 - 1) != v2))
..........
Found counterexample #7, refining ...
Searching for interpolation abstractions ...
11 clauses ... 275 -> 258 ... adding predicates:
get11_16_exp: \exists HeapObject v0, v1; (get11_16_exp_2_0 = 1 & v1 != v0 & read(get11_16_exp_3_0, 1) = v1 & O_Int(get11_16_exp_1_0) = v0)
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
get_pre_exp: \exists HeapObject v0, v1; (get_pre_exp_4_0 = get_pre_exp_1_0 & counterAddr(get_pre_exp_0_0) = 1 & !(get_pre_exp_1_0 = 1 & !(v1 = v0 & read(get_pre_exp_0_0, 1) = v0 & O_Int(get_pre_exp_3_0) = v0))), \exists HeapObject v0, v1, v2; (get_pre_exp_4_0 = get_pre_exp_1_0 & counterAddr(get_pre_exp_0_0) = 1 & read(get_pre_exp_0_0, 1) = v1 & O_Int(get_pre_exp_3_0 - 1) = v0 & !(get_pre_exp_1_0 = 1 & !(v2 = v0 & v1 = v0))), \exists HeapObject v0, v1, v2, v3; \exists int v4; (get_pre_exp_4_0 = 1 & read(get_pre_exp_0_0, 1) = v1 & O_Int(get_pre_exp_3_0 - 1) = v2 & O_Int(get_pre_exp_3_0) = v0 & !(v3 = v0 & !(v4 - get_pre_exp_3_0 != -1 & getInt(v2) = v4)) & !(v1 = v0 & v3 != v0))
...........
Found counterexample #8, refining ...
Searching for interpolation abstractions ...
11 clauses ... 275 -> 258 ... adding predicates:
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
Could not eliminate counterexample, postponing it
.java.lang.Exception: Predicate generation failed
at lazabs.horn.bottomup.CEGAR.liftedTree1$1(CEGAR.scala:177)
at lazabs.horn.bottomup.CEGAR.<init>(CEGAR.scala:171)
at lazabs.horn.bottomup.HornPredAbs.<init>(HornPredAbs.scala:132)
at hornconcurrency.VerificationLoop$$anonfun$16.apply(VerificationLoop.scala:338)
at hornconcurrency.VerificationLoop$$anonfun$16.apply(VerificationLoop.scala:293)
at lazabs.ParallelComputation$.apply(ParallelComputation.scala:46)
at hornconcurrency.VerificationLoop.<init>(VerificationLoop.scala:292)
at tricera.Main$$anonfun$23.apply(Main.scala:495)
at tricera.Main$$anonfun$23.apply(Main.scala:495)
at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
at scala.Console$.withOut(Console.scala:65)
at tricera.Main.run(Main.scala:494)
at tricera.Main$.doMain(Main.scala:122)
at tricera.Main$.main(Main.scala:64)
at tricera.Main.main(Main.scala)
(error "Predicate generation failed")
Other Error: Predicate generation failed
Successful run
../../tri -cex -acsl -log -dev -t:60 get-1.c
---------------------------- Reading C/C++ file --------------------------------
Checked properties:
unreach-call
Warning: no definition of function "non_det_int" available
Warning: no definition of function "non_det_int_ptr" available
Using invariants List(1)
Symmetry clauses: 0
Init clauses: 1
Time elapse clauses: 0
Assertion clauses: 2
Local transition clauses: 2
Local non-interference clauses: 0
Send/receive clauses: 0
Send non-interference clauses: 0
Receive non-interference clauses: 0
Send/receive non-interference clauses: 0
Barrier clauses: 0
Background axiom clauses: 9
------------------------------- Preprocessing ----------------------------------
#clauses #relation syms
Initially: 14 11
After eliminating fwd/bwd unreachable clauses (5ms): 14 11
After partial evaluation (6ms): 14 11
After constraint simplification (21ms): 14 11
After clause inlining (17ms): 5 2
After equality propagation (10ms): 5 2
After constant propagation (15ms): 5 2
After constraint simplification (9ms): 5 2
After clause inlining (0ms): 5 2
After eliminating fwd/bwd unreachable clauses (0ms): 5 2
After slicing (13ms): 5 2
After adding heap size arguments (7ms): 5 2
After equality propagation (1ms): 5 2
After constant propagation (1ms): 5 2
After constraint simplification (8ms): 5 2
After clause inlining (0ms): 5 2
After eliminating fwd/bwd unreachable clauses (0ms): 5 2
After slicing (1ms): 5 2
After Boolean clause splitting (67ms): 5 2
After equality propagation (3ms): 5 2
After constant propagation (1ms): 5 2
After constraint simplification (4ms): 5 2
After clause inlining (1ms): 5 2
After eliminating fwd/bwd unreachable clauses (0ms): 5 2
After slicing (0ms): 5 2
After cloning of relation symbols (9ms): 5 2
After shortening of clauses (0ms): 5 2
Total preprocessing time (ms): 227
------------------------------ Analysing loops ---------------------------------
Loop heads:
get11_16_exp/6 (1 clauses, 10 templates)
get_pre_exp/5 (1 clauses, 7 templates)
----------------------------------- CEGAR --------------------------------------
Theories: Types, ADT(O_Int, O_UInt, O_Addr, O_AddrRange, defObj, AllocResHeap, BatchAllocResHeap, AddrRange), HeapTheory
Constant and interval propagation +++++++++
Unique satisfiable clauses: 5
1 clauses with 0 body literals
3 clauses with 1 body literals
1 clauses with 2 body literals
Starting CEGAR ...
..
Found counterexample #1, refining ... 3 clauses ... 69 -> 68 ... adding predicates:
get11_16_exp: \exists HeapObject v0; \exists int v1, v2; !(get11_16_exp_2_0 = 1 & !(v2 != get11_16_exp_1_0 & read(get11_16_exp_3_0, 1) = v0 & getInt(v0) = v2) & !(v1 != 0 & read(get11_16_exp_3_0, 1) = v0 & HeapObject_ctor(v0) = v1))
..
Found counterexample #2, refining ... 5 clauses ... 127 -> 124 ... adding predicates:
get11_16_exp: get11_16_exp_2_0 != 1, \exists Addr v0; (v0 != get11_16_exp_2_0 & counterAddr(get11_16_exp_3_0) = v0)
get_pre_exp: true, counterAddr(get_pre_exp_0_0) = 1, \exists HeapObject v0, v1; !(get_pre_exp_4_0 = 1 & !(v1 = v0 & read(get_pre_exp_0_0, 1) = v0 & O_Int(get_pre_exp_3_0) = v0))
.....
Found counterexample #3, refining ... 6 clauses ... 140 -> 132 ... adding predicates:
get11_16_exp: get11_16_exp_5_0 = 0, \exists HeapObject v0; \exists int v1, v2; !(get11_16_exp_2_0 = 1 & !(v1 != 0 & read(get11_16_exp_3_0, 1) = v0 & HeapObject_ctor(v0) = v1) & !(0 >= v2 & read(get11_16_exp_3_0, 1) = v0 & getInt(v0) = v2)), \exists Addr v0; \exists HeapObject v1, v2; !(get11_16_exp_5_0 != get11_16_exp_1_0 & !(get11_16_exp_2_0 = 1 & v2 != v1 & read(get11_16_exp_3_0, 1) = v1 & O_Int(get11_16_exp_1_0) = v2) & !(v0 != get11_16_exp_2_0 & counterAddr(get11_16_exp_3_0) = v0))
get_pre_exp: get_pre_exp_4_0 = get_pre_exp_1_0 & counterAddr(get_pre_exp_0_0) = 1, get_pre_exp_4_0 = 1
.....
Found counterexample #4, refining ...
Searching for interpolation abstractions ...
Cost bound: 4
Interpolation abstraction: get11_16_exp: <(1 * _5 + -1 * -1 * _3), (1 * _5 + -1 * 1 * _3)> .
Interpolation abstraction: get11_16_exp: <(1 * _5 + -1 * -1 * _2), (1 * _5 + -1 * -1 * _3)> .
Interpolation abstraction: get11_16_exp: <(1 * _5 + -1 * -1 * _3), (1 * _5 + -1 * 1 * _2)> ...
Interpolation abstraction: get11_16_exp: <(1 * _5 + -1 * -1 * _2), (1 * _5 + -1 * 1 * _3)> .
Interpolation abstraction: get11_16_exp: <(1 * _5 + -1 * 1 * _2), (1 * _5 + -1 * 1 * _3)> .
183 -> 166 183 -> 166 183 -> 166 183 -> 166 183 -> 166 8 clauses ... 179 -> 165 ... adding predicates:
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
Warning: dropping predicate: cannot handle quantifier in predicate
get11_16_exp: \exists Addr v0; !(get11_16_exp_4_0 = get11_16_exp_2_0 & !(v0 = get11_16_exp_2_0 & counterAddr(get11_16_exp_3_0) = get11_16_exp_2_0)), \exists int v0; \exists HeapObject v1, v2, v3; !(get11_16_exp_4_0 = get11_16_exp_2_0 & !(counterAddr(get11_16_exp_3_0) = v0 & read(get11_16_exp_3_0, 1) = v2 & O_Int(get11_16_exp_1_0) = v1 & !(v0 = 1 & !(get11_16_exp_2_0 = 1 & !(v3 = v1 & v2 = v1) & !(v2 = v1 & v3 != v1))))), \exists HeapObject v0; \exists int v1, v2; !(get11_16_exp_2_0 = 1 & !(v1 != 0 & read(get11_16_exp_3_0, 1) = v0 & HeapObject_ctor(v0) = v1) & !(read(get11_16_exp_3_0, 1) = v0 & getInt(v0) = v2 & !\exists int v3; (v2 - v3 >= -2 & v3 >= 1 & v2 >= 1 & O_Int(v3 - 1) != v0) & !\exists int v3; (v2 - v3 >= -2 & v2 >= 1 & O_Int(v3 - 1) != v0) & !\exists int v3; (0 >= v3 & v2 >= 1 & O_Int(v3 - 1) != v0) & !\exists int v3; (v3 >= 1 & v2 >= 1 & O_Int(v3 - 1) != v0) & !\exists int v3; (v2 >= 1 & O_Int(v3 - 1) != v0) & !(v2 = 0 & O_Int(0) != v0))), get11_16_exp_5_0 = 1
get_pre_exp: \exists HeapObject v0, v1; (get_pre_exp_4_0 = get_pre_exp_1_0 & !(get_pre_exp_1_0 = 1 & !(v1 = v0 & read(get_pre_exp_0_0, 1) = v0 & O_Int(get_pre_exp_3_0) = v0))), \exists HeapObject v0, v1, v2; (read(get_pre_exp_0_0, 1) = v1 & O_Int(get_pre_exp_3_0 - 1) = v2 & O_Int(get_pre_exp_3_0) = v0 & !\exists HeapObject v3; \forall HeapObject v4; (get_pre_exp_4_0 = 1 & !(v4 = v2 & !(v3 = v2 & v1 = v0 & v2 != v0)))), get_pre_exp_4_0 = get_pre_exp_1_0, get_pre_exp_4_0 = 1 & get_pre_exp_1_0 = 1
.......
Found counterexample #5, refining ...
Searching for interpolation abstractions ...
219 -> 195 9 clauses ... 211 -> 196 ... adding predicates:
get11_16_exp: \exists HeapObject v0, v1, v2; (read(get11_16_exp_3_0, 1) = v1 & O_Int(get11_16_exp_1_0) = v0 & !(get11_16_exp_2_0 = 1 & !(v2 != v0 & v1 != v0))), \exists int v0; \exists HeapObject v1; \exists int v2, v3; !(get11_16_exp_4_0 = 1 & get11_16_exp_2_0 = 1 & !(v3 = 1 & read(get11_16_exp_3_0, 1) = v1 & getInt(v1) = 1) & !(v2 != 0 & read(get11_16_exp_3_0, 1) = v1 & HeapObject_ctor(v1) = v2) & !(v0 != 1 & counterAddr(get11_16_exp_3_0) = v0)), \exists int v0, v1; \exists HeapObject v2; \exists int v3, v4; !(!(v4 - get11_16_exp_5_0 - get11_16_exp_2_0.\as[int] = -1 & read(get11_16_exp_3_0.\as[int] + get11_16_exp_2_0.\as[int] - 1, 1) = v2 & getInt(v2) = get11_16_exp_5_0 + get11_16_exp_2_0.\as[int] - 1) & !(v3 != 0 & read(get11_16_exp_3_0.\as[int] + get11_16_exp_2_0.\as[int] - 1, 1) = v2 & HeapObject_ctor(v2) = v3) & !(v1 != 1 & counterAddr(get11_16_exp_3_0.\as[int] + get11_16_exp_2_0.\as[int] - 1) = v1) & !(v0 != 1 & counterAddr(get11_16_exp_3_0.\as[int] + get11_16_exp_2_0.\as[int] - 1) = v0))
get_pre_exp: \exists HeapObject v0; \exists int v1; (get_pre_exp_4_0 = get_pre_exp_1_0 & !(get_pre_exp_1_0 = 1 & !(v1 - get_pre_exp_3_0 != 1 & read(get_pre_exp_0_0, 1) = v0 & getInt(v0) = v1))), \exists HeapObject v0, v1, v2; (read(get_pre_exp_0_0, 1) = v1 & O_Int(get_pre_exp_3_0) = v0 & !(get_pre_exp_4_0 = 1 & !(v2 != v0 & v1 != v0))), get_pre_exp_4_0 = 1 & counterAddr(get_pre_exp_0_0) = 1
..........
--------------------------------- Statistics -----------------------------------
CEGAR iterations: 5
Total CEGAR time (ms): 12002
Setup time (ms): 146
Final number of abstract states: 3
Final number of matched abstract states: 7
Final number of abstract edges: 11
Number of generated predicates: 25
Average predicate size (# of sub-formulas): 4.92
Predicate generation time (ms): 10006
Number of implication checks: 295
Number of implication checks (setup): 45
Number of implication checks (positive): 137
Number of implication checks (negative): 113
Time for implication checks (setup, ms): 503
Time for implication checks (positive, ms): 163
Time for implication checks (negative, ms): 602
--------------------------------------------------------------------------------
Solution:
inv_main_6/4: (((((((EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & !(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4)))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)))))))) | ((EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & !(HeapObject_ctor(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0)) & !(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4)))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & !(HeapObject_ctor(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0)) & ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)))))))) | (((((((EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & (!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) & (-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0))) & !(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4)))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & (!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) & (-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0))) & ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)))))))) | (EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & ((!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) & (-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0)) & ALL ((-1 * _0 >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & !(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4)))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & ((!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) & (-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0)) & ALL ((-1 * _0 >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))))))))) | ((EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & ((!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) & ALL (((-1 + _0) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) & (-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0))) & !(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4)))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & ((!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) & ALL (((-1 + _0) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) & (-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0))) & ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)))))))) | (EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & (((!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) & (-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0)) & ALL (((-1 + _0) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) & ALL ((-1 * _0 >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & !(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4)))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & (((!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) & (-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0)) & ALL (((-1 + _0) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) & ALL ((-1 * _0 >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)))))))))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & ((((!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) & (-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0)) & ALL (((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-1 + _0) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL ((-1 * _0 >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))))) & (!(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4) | ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))))))))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & (((((!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) & (-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0)) & ALL ((((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (-1 * _0 >= 0)) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-1 + _0) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL ((-1 * _0 >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))))) & (!(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4) | ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))))))))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & (((((!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) & ALL (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL ((((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (-1 * _0 >= 0)) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-1 + _0) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL ((-1 * _0 >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))))) & (!(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4) | ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))))))))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & !(_4 = nthAddr(1))) & ((((((O_Int(0) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL ((((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (-1 * _0 >= 0)) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-1 + _0) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL ((-1 * _0 >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))))) & (!(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4) | ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))))))))))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & !(_4 = nthAddr(1))) & (!(HeapObject_ctor(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) | (-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0))) & (!(_4 = nthAddr(1)) | (!(HeapObject_ctor(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) | ((((((!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) | (O_Int(0) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL ((((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (-1 * _0 >= 0)) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-1 + _0) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL ((-1 * _0 >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))))))) & (!(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4) | ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))))))))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & !(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))))) & (!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = _3) | !(HeapObject_ctor(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0))) & (!(_4 = nthAddr(1)) | (!(HeapObject_ctor(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) | (-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0)))) & (!(_4 = nthAddr(1)) | (!(HeapObject_ctor(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) | ((((((!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) | (O_Int(0) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL ((((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (-1 * _0 >= 0)) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-1 + _0) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL ((-1 * _0 >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))))))) & (!(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4) | ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))))))))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)) & (!((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) = 0) | (((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) = 0) & !(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3))))) & (!(_4 = nthAddr(1)) | (!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = _3) | !(HeapObject_ctor(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0)))) & (!(_4 = nthAddr(1)) | (!(HeapObject_ctor(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) | (-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0)))) & (!(_4 = nthAddr(1)) | (!(HeapObject_ctor(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) | ((((((!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) | (O_Int(0) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL ((((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (-1 * _0 >= 0)) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-1 + _0) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL ((-1 * _0 >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))))))) & (!(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4) | ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))))))))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (((_2 = 0) & ((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0))) & (((((!(_4 = nthAddr(1)) & (!(_4 = counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) | (!((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) = 0) | (((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) = 0) & !(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)) = O_Int(_3)))))) & (!(_4 = nthAddr(1)) | (!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = _3) | !(HeapObject_ctor(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0)))) & (!(_4 = nthAddr(1)) | (!(HeapObject_ctor(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) | (-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0)))) & (!(_4 = nthAddr(1)) | (!(HeapObject_ctor(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) | ((((((!(getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) = 0) | (O_Int(0) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL ((((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (-1 * _0 >= 0)) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-3 + (_0 + -1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL (((-1 + _0) >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1)))))) & ((-1 * getInt(read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))) >= 0) | ALL ((-1 * _0 >= 0) | (O_Int((-1 + _0)) = read(write(newHeap(alloc(emptyHeap, O_Int(_1))), _5, O_Int(_4)), nthAddr(1))))))))) & (!(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4) | ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1))))))))) | EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & ((((((-1 + _3) >= 0) & ((-1 + _4) >= 0)) & ((-1 + counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))) >= 0)) & (_2 >= 0)) & (((_3 = _2) | (!(counterAddr(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3))) = _4) | ((_4 = nthAddr(1)) & !(O_Int(_3) = read(write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)), nthAddr(1)))))) & (!((-1 + counterAddr((-1 + (_4 + write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))))) = 0) | ((getInt(read((-1 + (_4 + write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))), nthAddr(1))) = (-1 + (_4 + _2))) | !(HeapObject_ctor(read((-1 + (_4 + write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)))), nthAddr(1))) = 0)))))))
get/10: (((write(_5, nthAddr(1), O_Int((-1 + getInt(read(_5, nthAddr(1)))))) = _0) & (((-1 + getInt(read(_5, nthAddr(1)))) >= 0) & ((((-1 + counterAddr(_5)) = 0) & ((-1 + _7) >= 0)) & (counterAddr(_5) = 1)))) & ((((((_6 = _1) & (_7 = _2)) & (nthAddr(1) = _3)) & (nthAddr(1) = _4)) & (nthAddr(1) = _8)) & (nthAddr(1) = _9)))
get_post/10: (((_4 = _3) & ((((_9 = 0) & ((((-1 + _7) >= 0) & ((-1 + _3) >= 0)) & ((-1 + counterAddr(_0)) >= 0))) & ((((((!(read(_0, nthAddr(1)) = O_Int(_7)) | !(_3 = nthAddr(1))) & (!(_3 = counterAddr(_0)) | (!((-1 + counterAddr(_0)) = 0) | (((-1 + counterAddr(_0)) = 0) & !(read(_0, nthAddr(1)) = O_Int(_7)))))) & (!(_3 = nthAddr(1)) | (!(getInt(read(_0, nthAddr(1))) = _7) | !(HeapObject_ctor(read(_0, nthAddr(1))) = 0)))) & (!(_3 = nthAddr(1)) | (!(HeapObject_ctor(read(_0, nthAddr(1))) = 0) | (-1 * getInt(read(_0, nthAddr(1))) >= 0)))) & (!(_3 = nthAddr(1)) | (!(HeapObject_ctor(read(_0, nthAddr(1))) = 0) | ((((((!(getInt(read(_0, nthAddr(1))) = 0) | (O_Int(0) = read(_0, nthAddr(1)))) & ((-1 * getInt(read(_0, nthAddr(1))) >= 0) | ALL (O_Int((-1 + _0)) = read(_1, nthAddr(1))))) & ((-1 * getInt(read(_0, nthAddr(1))) >= 0) | ALL ((((-3 + (_0 + -1 * getInt(read(_1, nthAddr(1))))) >= 0) | (-1 * _0 >= 0)) | (O_Int((-1 + _0)) = read(_1, nthAddr(1)))))) & ((-1 * getInt(read(_0, nthAddr(1))) >= 0) | ALL (((-3 + (_0 + -1 * getInt(read(_1, nthAddr(1))))) >= 0) | (O_Int((-1 + _0)) = read(_1, nthAddr(1)))))) & ((-1 * getInt(read(_0, nthAddr(1))) >= 0) | ALL (((-1 + _0) >= 0) | (O_Int((-1 + _0)) = read(_1, nthAddr(1)))))) & ((-1 * getInt(read(_0, nthAddr(1))) >= 0) | ALL ((-1 * _0 >= 0) | (O_Int((-1 + _0)) = read(_1, nthAddr(1))))))))) & (!(counterAddr(_0) = _3) | ((_3 = nthAddr(1)) & !(O_Int(_7) = read(_0, nthAddr(1))))))) | ((((((-1 + _7) >= 0) & ((-1 + _3) >= 0)) & ((-1 + counterAddr(_0)) >= 0)) & (_9 >= 0)) & (((_7 = _9) | (!(counterAddr(_0) = _3) | ((_3 = nthAddr(1)) & !(O_Int(_7) = read(_0, nthAddr(1)))))) & (!((-1 + counterAddr((-1 + (_3 + _0)))) = 0) | ((getInt(read((-1 + (_3 + _0)), nthAddr(1))) = (-1 + (_3 + _9))) | !(HeapObject_ctor(read((-1 + (_3 + _0)), nthAddr(1))) = 0))))))) & (((_6 = _1) & (_7 = _2)) & (_3 = _8)))
inv_main31_8/5: (EX ((((-1 + _3) >= 0) & (newAddr(alloc(emptyHeap, O_Int(_0))) = _4)) & (write(newHeap(alloc(emptyHeap, O_Int(_0))), _4, O_Int(_3)) = _1)) & (_3 = _4))
get11_20/12: (((write(_5, nthAddr(1), O_Int((-1 + getInt(read(_5, nthAddr(1)))))) = _0) & (((-1 + getInt(read(_5, nthAddr(1)))) >= 0) & ((((-1 + counterAddr(_5)) = 0) & ((-1 + _2) >= 0)) & (counterAddr(_5) = 1)))) & ((((((((nthAddr(1) = _3) & (nthAddr(1) = _4)) & (_1 = _6)) & (_2 = _7)) & (nthAddr(1) = _8)) & (nthAddr(1) = _9)) & (1 = _10)) & (nthAddr(1) = _11)))
inv_main23_3/4: ((((emptyHeap = _0) & (0 = _1)) & (0 = _2)) & (nullAddr = _3))
get7_18/10: (((-1 * getInt(read(_5, nthAddr(1))) >= 0) & (((((-1 + counterAddr(_5)) = 0) & ((-1 + _2) >= 0)) & (counterAddr(_5) = 1)) & ((nthAddr(1) = _3) & (nthAddr(1) = _8)))) & (((((_5 = _0) & (nthAddr(1) = _4)) & (_1 = _6)) & (_2 = _7)) & (nthAddr(1) = _9)))
get9_12/10: ((((-1 + getInt(read(_5, nthAddr(1)))) >= 0) & (((((-1 + counterAddr(_5)) = 0) & ((-1 + _2) >= 0)) & (counterAddr(_5) = 1)) & ((nthAddr(1) = _3) & (nthAddr(1) = _8)))) & (((((_5 = _0) & (nthAddr(1) = _4)) & (_1 = _6)) & (_2 = _7)) & (nthAddr(1) = _9)))
get5_1/10: ((((((-1 + counterAddr(_5)) = 0) & (_9 = nthAddr(1))) & ((-1 + _7) >= 0)) & (counterAddr(_5) = 1)) & ((((((_5 = _0) & (_6 = _1)) & (_7 = _2)) & (_9 = _3)) & (_9 = _4)) & (_9 = _8)))
get11_16/11: ((((((_4 = _3) & (_6 = _1)) & (_7 = _2)) & (_8 = _3)) & (_9 = _3)) & ((((_10 = 0) & ((((-1 + _2) >= 0) & ((-1 + _3) >= 0)) & ((-1 + counterAddr(_5)) >= 0))) & (((((((!(read(_5, nthAddr(1)) = O_Int(_2)) | !(_3 = nthAddr(1))) & (!(_3 = counterAddr(_5)) | (counterAddr(_5) = counterAddr(_5)))) & (!(_3 = counterAddr(_5)) | (!((-1 + counterAddr(_5)) = 0) | (((-1 + counterAddr(_5)) = 0) & !(read(_5, nthAddr(1)) = O_Int(_2)))))) & (!(_3 = nthAddr(1)) | (!(getInt(read(_5, nthAddr(1))) = _2) | !(HeapObject_ctor(read(_5, nthAddr(1))) = 0)))) & (!(_3 = nthAddr(1)) | (!(HeapObject_ctor(read(_5, nthAddr(1))) = 0) | (-1 * getInt(read(_5, nthAddr(1))) >= 0)))) & (!(_3 = nthAddr(1)) | (!(HeapObject_ctor(read(_5, nthAddr(1))) = 0) | ((((((!(getInt(read(_5, nthAddr(1))) = 0) | (O_Int(0) = read(_5, nthAddr(1)))) & ((-1 * getInt(read(_5, nthAddr(1))) >= 0) | ALL (O_Int((-1 + _0)) = read(_6, nthAddr(1))))) & ((-1 * getInt(read(_5, nthAddr(1))) >= 0) | ALL ((((-3 + (_0 + -1 * getInt(read(_6, nthAddr(1))))) >= 0) | (-1 * _0 >= 0)) | (O_Int((-1 + _0)) = read(_6, nthAddr(1)))))) & ((-1 * getInt(read(_5, nthAddr(1))) >= 0) | ALL (((-3 + (_0 + -1 * getInt(read(_6, nthAddr(1))))) >= 0) | (O_Int((-1 + _0)) = read(_6, nthAddr(1)))))) & ((-1 * getInt(read(_5, nthAddr(1))) >= 0) | ALL (((-1 + _0) >= 0) | (O_Int((-1 + _0)) = read(_6, nthAddr(1)))))) & ((-1 * getInt(read(_5, nthAddr(1))) >= 0) | ALL ((-1 * _0 >= 0) | (O_Int((-1 + _0)) = read(_6, nthAddr(1))))))))) & (!(counterAddr(_5) = _3) | ((_3 = nthAddr(1)) & !(O_Int(_2) = read(_5, nthAddr(1))))))) | ((((((-1 + _2) >= 0) & ((-1 + _3) >= 0)) & ((-1 + counterAddr(_5)) >= 0)) & (_10 >= 0)) & (((!(_3 = counterAddr(_5)) | (counterAddr(_5) = counterAddr(_5))) & ((_2 = _10) | (!(counterAddr(_5) = _3) | ((_3 = nthAddr(1)) & !(O_Int(_2) = read(_5, nthAddr(1))))))) & (!((-1 + counterAddr((-1 + (_3 + _5)))) = 0) | ((getInt(read((-1 + (_3 + _5)), nthAddr(1))) = (-1 + (_3 + _10))) | !(HeapObject_ctor(read((-1 + (_3 + _5)), nthAddr(1))) = 0)))))))
get_pre/5: ((_4 = _3) & (((((-1 + counterAddr(_0)) = 0) & (_3 = nthAddr(1))) & ((-1 + _2) >= 0)) & (counterAddr(_0) = 1)))
Inferred ACSL annotations
================================================================================
/* contracts for get */
/*@
requires p == n && n_init >= 1;
ensures ((\result == 0 && 0 >= \old(*n)) || \result >= 0) && r1 == \old(r1) && n_init == \old(n_init) && \old(n) == n;
*/
================================================================================
SAFE