- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: d1af4f84-b9c6-4b47-8c9a-fa014d69e15d
    creation_time: 2024-03-01T08:12:16Z
    producer:
      name: Goblint
      version: heads/fix-locations-pred-0-g0bf0407c6-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp.json'' ''--disable'' ''witness.graphml.enabled''
        ''--set'' ''witness.yaml.invariant-types[+]'' ''location_invariant'' ''--enable''
        ''witness.invariant.after-lock'' ''--enable'' ''witness.invariant.other''
        ''--enable'' ''witness.invariant.accessed'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  content:
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1836
        column: 4
        function: atomic_fetch_add
      value: 1 == v
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1836
        column: 4
        function: atomic_fetch_add
      value: obj == & stack.count
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1837
        column: 4
        function: atomic_fetch_add
      value: 1 == v
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1837
        column: 4
        function: atomic_fetch_add
      value: obj == & stack.count
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1885
        column: 8
        function: Push
      value: 0 <= index
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1885
        column: 8
        function: Push
      value: 0 <= head1
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1885
        column: 8
        function: Push
      value: index <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1885
        column: 8
        function: Push
      value: head1 <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1870
        column: 16
        function: Pop
      value: 0 <= head1
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1870
        column: 16
        function: Pop
      value: head1 <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1841
        column: 4
        function: atomic_fetch_sub
      value: (2147483647LL + (long long )old) + (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1841
        column: 4
        function: atomic_fetch_sub
      value: (2147483646LL - (long long )old) + (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1841
        column: 4
        function: atomic_fetch_sub
      value: (2147483649LL + (long long )old) - (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1841
        column: 4
        function: atomic_fetch_sub
      value: (2147483648LL - (long long )old) - (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1841
        column: 4
        function: atomic_fetch_sub
      value: 1 == v
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1841
        column: 4
        function: atomic_fetch_sub
      value: obj == & stack.count
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1817
        column: 4
        function: atomic_compare_and_exchange
      value: (long long )desired + (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1817
        column: 4
        function: atomic_compare_and_exchange
      value: (long long )desired - (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1817
        column: 4
        function: atomic_compare_and_exchange
      value: (_Bool)0 == ret
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1817
        column: 4
        function: atomic_compare_and_exchange
      value: obj == & stack.head
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1817
        column: 4
        function: atomic_compare_and_exchange
      value: ret == (_Bool)0
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1845
        column: 4
        function: atomic_fetch_sub
      value: 1 == v
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1845
        column: 4
        function: atomic_fetch_sub
      value: obj == & stack.count
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1851
        column: 4
        function: Init
      value: (2147483645LL + (long long )i) + (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1851
        column: 4
        function: Init
      value: (2147483644LL - (long long )i) + (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1851
        column: 4
        function: Init
      value: (2147483651LL + (long long )i) - (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1851
        column: 4
        function: Init
      value: (2147483650LL - (long long )i) - (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1851
        column: 4
        function: Init
      value: 3 == pushCount
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1898
        column: 12
        function: thread
      value: arg == idx
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1843
        column: 4
        function: atomic_fetch_sub
      value: 1 == v
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1843
        column: 4
        function: atomic_fetch_sub
      value: obj == & stack.count
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1843
        column: 4
        function: atomic_fetch_sub
      value: v == 1
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1902
        column: 8
        function: thread
      value: 0 <= idx
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1902
        column: 8
        function: thread
      value: 0 <= elem
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1902
        column: 8
        function: thread
      value: idx <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1902
        column: 8
        function: thread
      value: elem <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1902
        column: 8
        function: thread
      value: (long long )elem + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1902
        column: 8
        function: thread
      value: (1LL + (long long )elem) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1902
        column: 8
        function: thread
      value: arg == idx
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1809
        column: 4
        function: atomic_exchange
      value: (2147483649LL + (long long )t) + (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1809
        column: 4
        function: atomic_exchange
      value: (2147483648LL - (long long )t) + (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1799
        column: 4
        function: atomic_store
      value: (-1 <= v && v <= 3) || (0 <= v && v <= 2)
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1903
        column: 8
        function: thread
      value: 0 <= idx
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1903
        column: 8
        function: thread
      value: 0 <= elem
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1903
        column: 8
        function: thread
      value: idx <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1903
        column: 8
        function: thread
      value: elem <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1903
        column: 8
        function: thread
      value: (long long )elem + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1903
        column: 8
        function: thread
      value: (1LL + (long long )elem) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1903
        column: 8
        function: thread
      value: arg == idx
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1863
        column: 8
        function: Pop
      value: 0 <= head1
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1863
        column: 8
        function: Pop
      value: head1 <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1903
        column: 47
        function: thread
      value: (long long )elem + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1903
        column: 47
        function: thread
      value: (1LL + (long long )elem) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1903
        column: 47
        function: thread
      value: arg == idx
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1804
        column: 4
        function: atomic_load
      value: 0 <= stack.head
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1804
        column: 4
        function: atomic_load
      value: stack.head <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1804
        column: 4
        function: atomic_load
      value: (obj == & stack.head && (0 <= *obj && *obj <= 2)) || obj == & stack.count
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1816
        column: 4
        function: atomic_compare_and_exchange
      value: (long long )desired + (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1816
        column: 4
        function: atomic_compare_and_exchange
      value: (1LL + (long long )desired) - (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1816
        column: 4
        function: atomic_compare_and_exchange
      value: obj == & stack.head
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1818
        column: 4
        function: atomic_compare_and_exchange
      value: 0 <= stack.head
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1818
        column: 4
        function: atomic_compare_and_exchange
      value: 0 <= *obj
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1818
        column: 4
        function: atomic_compare_and_exchange
      value: stack.head <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1818
        column: 4
        function: atomic_compare_and_exchange
      value: '*obj <= 2'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1818
        column: 4
        function: atomic_compare_and_exchange
      value: (long long )desired + (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1818
        column: 4
        function: atomic_compare_and_exchange
      value: (long long )desired - (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1818
        column: 4
        function: atomic_compare_and_exchange
      value: (_Bool)0 == ret
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1818
        column: 4
        function: atomic_compare_and_exchange
      value: obj == & stack.head
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1818
        column: 4
        function: atomic_compare_and_exchange
      value: (0 <= *expected && *expected <= 2) || (0 <= *expected && *expected <=
        2)
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1857
        column: 0
        function: Init
      value: (-5LL + (long long )i) + (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1857
        column: 0
        function: Init
      value: (-1LL - (long long )i) + (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1857
        column: 0
        function: Init
      value: (1LL + (long long )i) - (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1857
        column: 0
        function: Init
      value: (5LL - (long long )i) - (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1857
        column: 0
        function: Init
      value: 3 == pushCount
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1913
        column: 8
        function: main
      value: (0 == i && i == 0) || (1 <= i && i <= 2)
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1906
        column: 4
        function: thread
      value: (2147483644LL + (long long )elem) + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1906
        column: 4
        function: thread
      value: (2147483648LL + (long long )elem) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1906
        column: 4
        function: thread
      value: arg == idx
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1882
        column: 4
        function: Push
      value: (2147483648LL + (long long )head1) + (long long )index >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1882
        column: 4
        function: Push
      value: (2147483647LL - (long long )head1) + (long long )index >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1864
        column: 8
        function: Pop
      value: -1 <= next1
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1864
        column: 8
        function: Pop
      value: 0 <= head1
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1864
        column: 8
        function: Pop
      value: head1 <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1864
        column: 8
        function: Pop
      value: next1 <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1893
        column: 4
        function: thread
      value: 0 <= idx
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1893
        column: 4
        function: thread
      value: idx <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1893
        column: 4
        function: thread
      value: (2147483648LL + (long long )elem) + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1893
        column: 4
        function: thread
      value: (2147483647LL - (long long )elem) + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1893
        column: 4
        function: thread
      value: (6442450943LL + (long long )elem) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1893
        column: 4
        function: thread
      value: (6442450942LL - (long long )elem) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1893
        column: 4
        function: thread
      value: arg == idx
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1892
        column: 4
        function: thread
      value: (unsigned long )arg <= 2UL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1892
        column: 4
        function: thread
      value: (2147483648LL + (long long )elem) + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1892
        column: 4
        function: thread
      value: (2147483647LL - (long long )elem) + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1892
        column: 4
        function: thread
      value: (6442450943LL + (long long )elem) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1892
        column: 4
        function: thread
      value: (6442450942LL - (long long )elem) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1874
        column: 16
        function: Pop
      value: 0 <= head1
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1874
        column: 16
        function: Pop
      value: 0 <= next1
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1874
        column: 16
        function: Pop
      value: head1 <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1874
        column: 16
        function: Pop
      value: next1 <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1842
        column: 4
        function: atomic_fetch_sub
      value: (2147483647LL + (long long )old) + (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1842
        column: 4
        function: atomic_fetch_sub
      value: (2147483646LL - (long long )old) + (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1842
        column: 4
        function: atomic_fetch_sub
      value: (2147483649LL + (long long )old) - (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1842
        column: 4
        function: atomic_fetch_sub
      value: (2147483648LL - (long long )old) - (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1842
        column: 4
        function: atomic_fetch_sub
      value: 1 == v
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1842
        column: 4
        function: atomic_fetch_sub
      value: obj == & stack.count
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1829
        column: 4
        function: atomic_compare_and_exchange
      value: (long long )desired + (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1829
        column: 4
        function: atomic_compare_and_exchange
      value: (1LL + (long long )desired) - (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1829
        column: 4
        function: atomic_compare_and_exchange
      value: obj == & stack.head
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1829
        column: 4
        function: atomic_compare_and_exchange
      value: ret == (_Bool)0 || ret == (_Bool)1
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1810
        column: 4
        function: atomic_exchange
      value: -1 <= v
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1810
        column: 4
        function: atomic_exchange
      value: -1 <= t
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1810
        column: 4
        function: atomic_exchange
      value: v <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1810
        column: 4
        function: atomic_exchange
      value: t <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1820
        column: 8
        function: atomic_compare_and_exchange
      value: 0 <= desired
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1820
        column: 8
        function: atomic_compare_and_exchange
      value: 0 <= *obj
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1820
        column: 8
        function: atomic_compare_and_exchange
      value: desired <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1820
        column: 8
        function: atomic_compare_and_exchange
      value: '*obj <= 2'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1820
        column: 8
        function: atomic_compare_and_exchange
      value: (long long )desired + (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1820
        column: 8
        function: atomic_compare_and_exchange
      value: (long long )desired - (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1820
        column: 8
        function: atomic_compare_and_exchange
      value: (_Bool)0 == ret
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1820
        column: 8
        function: atomic_compare_and_exchange
      value: obj == & stack.head
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: (2147483645LL + (long long )i) + (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: (2147483644LL - (long long )i) + (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: (2147483651LL + (long long )i) - (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: (2147483650LL - (long long )i) - (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: 3 == pushCount
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1821
        column: 8
        function: atomic_compare_and_exchange
      value: 0 <= stack.head
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1821
        column: 8
        function: atomic_compare_and_exchange
      value: stack.head <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1821
        column: 8
        function: atomic_compare_and_exchange
      value: (long long )desired + (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1821
        column: 8
        function: atomic_compare_and_exchange
      value: (long long )desired - (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1821
        column: 8
        function: atomic_compare_and_exchange
      value: (_Bool)0 == ret
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1821
        column: 8
        function: atomic_compare_and_exchange
      value: obj == & stack.head
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1800
        column: 4
        function: atomic_store
      value: (stack.count == 3 && stack.head == 0) || (0 <= stack.head && stack.head
        <= 2)
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1834
        column: 4
        function: atomic_fetch_add
      value: (2147483647LL + (long long )old) + (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1834
        column: 4
        function: atomic_fetch_add
      value: (2147483646LL - (long long )old) + (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1834
        column: 4
        function: atomic_fetch_add
      value: (2147483649LL + (long long )old) - (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1834
        column: 4
        function: atomic_fetch_add
      value: (2147483648LL - (long long )old) - (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1834
        column: 4
        function: atomic_fetch_add
      value: 1 == v
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1834
        column: 4
        function: atomic_fetch_add
      value: obj == & stack.count
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1828
        column: 4
        function: atomic_compare_and_exchange
      value: (long long )desired + (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1828
        column: 4
        function: atomic_compare_and_exchange
      value: (1LL + (long long )desired) - (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1828
        column: 4
        function: atomic_compare_and_exchange
      value: obj == & stack.head
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1828
        column: 4
        function: atomic_compare_and_exchange
      value: ret == (_Bool)0 || ret == (_Bool)1
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1915
        column: 4
        function: main
      value: i == 3
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1850
        column: 4
        function: Init
      value: (2147483645LL + (long long )i) + (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1850
        column: 4
        function: Init
      value: (2147483644LL - (long long )i) + (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1850
        column: 4
        function: Init
      value: (2147483651LL + (long long )i) - (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1850
        column: 4
        function: Init
      value: (2147483650LL - (long long )i) - (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1850
        column: 4
        function: Init
      value: 3 == pushCount
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1850
        column: 4
        function: Init
      value: pushCount == 3
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1812
        column: 4
        function: atomic_exchange
      value: -1 <= t
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1812
        column: 4
        function: atomic_exchange
      value: t <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1844
        column: 4
        function: atomic_fetch_sub
      value: 1 == v
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1844
        column: 4
        function: atomic_fetch_sub
      value: obj == & stack.count
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1916
        column: 8
        function: main
      value: 0 <= i
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1916
        column: 8
        function: main
      value: i <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1826
        column: 8
        function: atomic_compare_and_exchange
      value: (long long )desired + (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1826
        column: 8
        function: atomic_compare_and_exchange
      value: (long long )desired - (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1826
        column: 8
        function: atomic_compare_and_exchange
      value: (_Bool)0 == ret
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1826
        column: 8
        function: atomic_compare_and_exchange
      value: obj == & stack.head
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1866
        column: 12
        function: Pop
      value: 0 <= head1
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1866
        column: 12
        function: Pop
      value: head1 <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1854
        column: 8
        function: Init
      value: 0 <= i
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1854
        column: 8
        function: Init
      value: i <= 1
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1854
        column: 8
        function: Init
      value: (-3LL + (long long )i) + (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1854
        column: 8
        function: Init
      value: (-2LL - (long long )i) + (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1854
        column: 8
        function: Init
      value: (3LL + (long long )i) - (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1854
        column: 8
        function: Init
      value: (4LL - (long long )i) - (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1854
        column: 8
        function: Init
      value: 3 == pushCount
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1904
        column: 8
        function: thread
      value: 0 <= elem
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1904
        column: 8
        function: thread
      value: elem <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1904
        column: 8
        function: thread
      value: (long long )elem + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1904
        column: 8
        function: thread
      value: (1LL + (long long )elem) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1904
        column: 8
        function: thread
      value: arg == idx
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1835
        column: 4
        function: atomic_fetch_add
      value: 1 == v
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1835
        column: 4
        function: atomic_fetch_add
      value: obj == & stack.count
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1835
        column: 4
        function: atomic_fetch_add
      value: v == 1
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1856
        column: 4
        function: Init
      value: (-5LL + (long long )i) + (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1856
        column: 4
        function: Init
      value: (-1LL - (long long )i) + (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1856
        column: 4
        function: Init
      value: (1LL + (long long )i) - (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1856
        column: 4
        function: Init
      value: (5LL - (long long )i) - (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1856
        column: 4
        function: Init
      value: 3 == pushCount
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1856
        column: 4
        function: Init
      value: pushCount == 3
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1833
        column: 4
        function: atomic_fetch_add
      value: (2147483647LL + (long long )old) + (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1833
        column: 4
        function: atomic_fetch_add
      value: (2147483646LL - (long long )old) + (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1833
        column: 4
        function: atomic_fetch_add
      value: (2147483649LL + (long long )old) - (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1833
        column: 4
        function: atomic_fetch_add
      value: (2147483648LL - (long long )old) - (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1833
        column: 4
        function: atomic_fetch_add
      value: 1 == v
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1833
        column: 4
        function: atomic_fetch_add
      value: obj == & stack.count
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1899
        column: 12
        function: thread
      value: -1 <= elem
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1899
        column: 12
        function: thread
      value: i <= 1U
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1899
        column: 12
        function: thread
      value: elem <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1899
        column: 12
        function: thread
      value: arg == idx
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1825
        column: 8
        function: atomic_compare_and_exchange
      value: 0 <= stack.head
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1825
        column: 8
        function: atomic_compare_and_exchange
      value: 0 <= *obj
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1825
        column: 8
        function: atomic_compare_and_exchange
      value: stack.head <= 2
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1825
        column: 8
        function: atomic_compare_and_exchange
      value: '*obj <= 2'
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1825
        column: 8
        function: atomic_compare_and_exchange
      value: (long long )desired + (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1825
        column: 8
        function: atomic_compare_and_exchange
      value: (long long )desired - (long long )ret >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1825
        column: 8
        function: atomic_compare_and_exchange
      value: (_Bool)0 == ret
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1825
        column: 8
        function: atomic_compare_and_exchange
      value: obj == & stack.head
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1825
        column: 8
        function: atomic_compare_and_exchange
      value: (0 <= *expected && *expected <= 2) || (0 <= *expected && *expected <=
        2)
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1808
        column: 4
        function: atomic_exchange
      value: (2147483649LL + (long long )t) + (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: location_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1808
        column: 4
        function: atomic_exchange
      value: (2147483648LL - (long long )t) + (long long )v >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1896
        column: 8
        function: thread
      value: 0 <= idx
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1896
        column: 8
        function: thread
      value: i <= 1U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1896
        column: 8
        function: thread
      value: idx <= 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1896
        column: 8
        function: thread
      value: (unsigned long )arg <= 2UL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1896
        column: 8
        function: thread
      value: arg == idx
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1912
        column: 4
        function: main
      value: (((0 == i && stack.count == 3) && stack.head == 0) && i == 0) || (1 <=
        i && i <= 3)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1893
        column: 4
        function: thread
      value: 0 <= idx
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1893
        column: 4
        function: thread
      value: i <= 2U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1893
        column: 4
        function: thread
      value: idx <= 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1893
        column: 4
        function: thread
      value: (unsigned long )arg <= 2UL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1893
        column: 4
        function: thread
      value: (2147483648LL + (long long )elem) + (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1893
        column: 4
        function: thread
      value: (2147483648LL + (long long )elem) - (long long )i >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1893
        column: 4
        function: thread
      value: arg == idx
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1883
        column: 4
        function: Push
      value: 0 <= index
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1883
        column: 4
        function: Push
      value: 0 <= head1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1883
        column: 4
        function: Push
      value: index <= 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1883
        column: 4
        function: Push
      value: head1 <= 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: 0 <= i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: i <= 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: (-3LL + (long long )i) + (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: (-1LL - (long long )i) + (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: (3LL + (long long )i) - (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: (5LL - (long long )i) - (long long )pushCount >= 0LL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: 3 == pushCount
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: stack.count == 3
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: stack.head == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1852
        column: 4
        function: Init
      value: pushCount == 3
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1915
        column: 4
        function: main
      value: 0 <= i
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i
        file_hash: 1d61eb304445c3cb39dfadfa4748d680ea5f0f4958f8bc176e8bc3c77c47e674
        line: 1915
        column: 4
        function: main
      value: i <= 3
      format: c_expression
