- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 8179439a-de26-4d44-92d5-76048f205e9b
    creation_time: 2025-03-22T10:13:33Z
    producer:
      name: Goblint
      version: heads/master-0-g66dff5a90-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp.json'' ''--disable'' ''witness.graphml.enabled''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/valid-memsafety.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i: 7cc273f13a619f37768d5108c297b75ab7c37145fe391daced9c134730721251
      data_model: ILP32
      language: C
      specification: 'CHECK( init(main()), LTL(G valid-free) )

        CHECK( init(main()), LTL(G valid-deref) )

        CHECK( init(main()), LTL(G valid-memtrack) )'
  content:
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1011
        column: 5
        function: t1
      value: 0 <= queue.head
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1011
        column: 5
        function: t1
      value: 0 <= ((QType *)arg)->head
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1011
        column: 5
        function: t1
      value: queue.head <= 20
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1011
        column: 5
        function: t1
      value: ((QType *)arg)->head <= 20
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1011
        column: 5
        function: t1
      value: enqueue_flag == (_Bool)1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1011
        column: 5
        function: t1
      value: arg == (void *)(& queue)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1011
        column: 5
        function: t1
      value: (((((((((((((((((((((((((((-2147483628 <= queue.amount && -2147483628
        <= ((QType *)arg)->amount) && (2147483628LL + (long long )i) + (long long
        )value >= 0LL) && (2147483668LL - (long long )i) + (long long )value >= 0LL)
        && (2147483627LL + (long long )i) - (long long )value >= 0LL) && (2147483667LL
        - (long long )i) - (long long )value >= 0LL) && queue.tail == 20) && i ==
        20) && ((QType *)arg)->tail == 20) || ((((((((-2147483629 <= queue.amount
        && -2147483629 <= ((QType *)arg)->amount) && (2147483629LL + (long long )i)
        + (long long )value >= 0LL) && (2147483667LL - (long long )i) + (long long
        )value >= 0LL) && (2147483628LL + (long long )i) - (long long )value >= 0LL)
        && (2147483666LL - (long long )i) - (long long )value >= 0LL) && queue.tail
        == 19) && i == 19) && ((QType *)arg)->tail == 19)) || ((((((((-2147483630
        <= queue.amount && -2147483630 <= ((QType *)arg)->amount) && (2147483630LL
        + (long long )i) + (long long )value >= 0LL) && (2147483666LL - (long long
        )i) + (long long )value >= 0LL) && (2147483629LL + (long long )i) - (long
        long )value >= 0LL) && (2147483665LL - (long long )i) - (long long )value
        >= 0LL) && queue.tail == 18) && i == 18) && ((QType *)arg)->tail == 18)) ||
        ((((((((-2147483631 <= queue.amount && -2147483631 <= ((QType *)arg)->amount)
        && (2147483631LL + (long long )i) + (long long )value >= 0LL) && (2147483665LL
        - (long long )i) + (long long )value >= 0LL) && (2147483630LL + (long long
        )i) - (long long )value >= 0LL) && (2147483664LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 17) && i == 17) && ((QType *)arg)->tail
        == 17)) || ((((((((-2147483632 <= queue.amount && -2147483632 <= ((QType *)arg)->amount)
        && (2147483632LL + (long long )i) + (long long )value >= 0LL) && (2147483664LL
        - (long long )i) + (long long )value >= 0LL) && (2147483631LL + (long long
        )i) - (long long )value >= 0LL) && (2147483663LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 16) && i == 16) && ((QType *)arg)->tail
        == 16)) || ((((((((-2147483633 <= queue.amount && -2147483633 <= ((QType *)arg)->amount)
        && (2147483633LL + (long long )i) + (long long )value >= 0LL) && (2147483663LL
        - (long long )i) + (long long )value >= 0LL) && (2147483632LL + (long long
        )i) - (long long )value >= 0LL) && (2147483662LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 15) && i == 15) && ((QType *)arg)->tail
        == 15)) || ((((((((-2147483634 <= queue.amount && -2147483634 <= ((QType *)arg)->amount)
        && (2147483634LL + (long long )i) + (long long )value >= 0LL) && (2147483662LL
        - (long long )i) + (long long )value >= 0LL) && (2147483633LL + (long long
        )i) - (long long )value >= 0LL) && (2147483661LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 14) && i == 14) && ((QType *)arg)->tail
        == 14)) || ((((((((-2147483635 <= queue.amount && -2147483635 <= ((QType *)arg)->amount)
        && (2147483635LL + (long long )i) + (long long )value >= 0LL) && (2147483661LL
        - (long long )i) + (long long )value >= 0LL) && (2147483634LL + (long long
        )i) - (long long )value >= 0LL) && (2147483660LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 13) && i == 13) && ((QType *)arg)->tail
        == 13)) || ((((((((-2147483636 <= queue.amount && -2147483636 <= ((QType *)arg)->amount)
        && (2147483636LL + (long long )i) + (long long )value >= 0LL) && (2147483660LL
        - (long long )i) + (long long )value >= 0LL) && (2147483635LL + (long long
        )i) - (long long )value >= 0LL) && (2147483659LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 12) && i == 12) && ((QType *)arg)->tail
        == 12)) || ((((((((-2147483637 <= queue.amount && -2147483637 <= ((QType *)arg)->amount)
        && (2147483637LL + (long long )i) + (long long )value >= 0LL) && (2147483659LL
        - (long long )i) + (long long )value >= 0LL) && (2147483636LL + (long long
        )i) - (long long )value >= 0LL) && (2147483658LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 11) && i == 11) && ((QType *)arg)->tail
        == 11)) || ((((((((-2147483638 <= queue.amount && -2147483638 <= ((QType *)arg)->amount)
        && (2147483638LL + (long long )i) + (long long )value >= 0LL) && (2147483658LL
        - (long long )i) + (long long )value >= 0LL) && (2147483637LL + (long long
        )i) - (long long )value >= 0LL) && (2147483657LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 10) && i == 10) && ((QType *)arg)->tail
        == 10)) || ((((((((-2147483639 <= queue.amount && -2147483639 <= ((QType *)arg)->amount)
        && (2147483639LL + (long long )i) + (long long )value >= 0LL) && (2147483657LL
        - (long long )i) + (long long )value >= 0LL) && (2147483638LL + (long long
        )i) - (long long )value >= 0LL) && (2147483656LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 9) && i == 9) && ((QType *)arg)->tail
        == 9)) || ((((((((-2147483640 <= queue.amount && -2147483640 <= ((QType *)arg)->amount)
        && (2147483640LL + (long long )i) + (long long )value >= 0LL) && (2147483656LL
        - (long long )i) + (long long )value >= 0LL) && (2147483639LL + (long long
        )i) - (long long )value >= 0LL) && (2147483655LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 8) && i == 8) && ((QType *)arg)->tail
        == 8)) || ((((((((-2147483641 <= queue.amount && -2147483641 <= ((QType *)arg)->amount)
        && (2147483641LL + (long long )i) + (long long )value >= 0LL) && (2147483655LL
        - (long long )i) + (long long )value >= 0LL) && (2147483640LL + (long long
        )i) - (long long )value >= 0LL) && (2147483654LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 7) && i == 7) && ((QType *)arg)->tail
        == 7)) || ((((((((-2147483642 <= queue.amount && -2147483642 <= ((QType *)arg)->amount)
        && (2147483642LL + (long long )i) + (long long )value >= 0LL) && (2147483654LL
        - (long long )i) + (long long )value >= 0LL) && (2147483641LL + (long long
        )i) - (long long )value >= 0LL) && (2147483653LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 6) && i == 6) && ((QType *)arg)->tail
        == 6)) || ((((((((-2147483643 <= queue.amount && -2147483643 <= ((QType *)arg)->amount)
        && (2147483643LL + (long long )i) + (long long )value >= 0LL) && (2147483653LL
        - (long long )i) + (long long )value >= 0LL) && (2147483642LL + (long long
        )i) - (long long )value >= 0LL) && (2147483652LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 5) && i == 5) && ((QType *)arg)->tail
        == 5)) || ((((((((-2147483644 <= queue.amount && -2147483644 <= ((QType *)arg)->amount)
        && (2147483644LL + (long long )i) + (long long )value >= 0LL) && (2147483652LL
        - (long long )i) + (long long )value >= 0LL) && (2147483643LL + (long long
        )i) - (long long )value >= 0LL) && (2147483651LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 4) && i == 4) && ((QType *)arg)->tail
        == 4)) || ((((((((-2147483645 <= queue.amount && -2147483645 <= ((QType *)arg)->amount)
        && (2147483645LL + (long long )i) + (long long )value >= 0LL) && (2147483651LL
        - (long long )i) + (long long )value >= 0LL) && (2147483644LL + (long long
        )i) - (long long )value >= 0LL) && (2147483650LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 3) && i == 3) && ((QType *)arg)->tail
        == 3)) || ((((((((-2147483646 <= queue.amount && -2147483646 <= ((QType *)arg)->amount)
        && (2147483646LL + (long long )i) + (long long )value >= 0LL) && (2147483650LL
        - (long long )i) + (long long )value >= 0LL) && (2147483645LL + (long long
        )i) - (long long )value >= 0LL) && (2147483649LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 2) && i == 2) && ((QType *)arg)->tail
        == 2)) || ((((((((-2147483647 <= queue.amount && -2147483647 <= ((QType *)arg)->amount)
        && (2147483647LL + (long long )i) + (long long )value >= 0LL) && (2147483649LL
        - (long long )i) + (long long )value >= 0LL) && (2147483646LL + (long long
        )i) - (long long )value >= 0LL) && (2147483648LL - (long long )i) - (long
        long )value >= 0LL) && queue.tail == 1) && i == 1) && ((QType *)arg)->tail
        == 1)) || ((((((((2147483648LL + (long long )i) + (long long )value >= 0LL
        && (2147483648LL - (long long )i) + (long long )value >= 0LL) && (2147483647LL
        + (long long )i) - (long long )value >= 0LL) && (2147483647LL - (long long
        )i) - (long long )value >= 0LL) && 0 == i) && i == 0) && (queue.tail == 0
        || queue.tail == 20)) && (((QType *)arg)->tail == 0 || ((QType *)arg)->tail
        == 20))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1029
        column: 5
        function: t2
      value: 0 <= queue.head
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1029
        column: 5
        function: t2
      value: 0 <= ((QType *)arg)->head
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1029
        column: 5
        function: t2
      value: queue.head <= 20
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1029
        column: 5
        function: t2
      value: ((QType *)arg)->head <= 20
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1029
        column: 5
        function: t2
      value: dequeue_flag == (_Bool)1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1029
        column: 5
        function: t2
      value: arg == (void *)(& queue)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1029
        column: 5
        function: t2
      value: queue.tail == 0 || queue.tail == 20
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1029
        column: 5
        function: t2
      value: ((QType *)arg)->tail == 0 || ((QType *)arg)->tail == 20
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/queue_ok.i
        line: 1029
        column: 5
        function: t2
      value: (((((((((((((((((((i == 1 || i == 14) || (0 == i && i == 0)) || i ==
        13) || i == 12) || i == 11) || i == 10) || i == 9) || i == 8) || i == 7) ||
        i == 20) || i == 6) || i == 19) || i == 5) || i == 18) || i == 4) || i ==
        17) || i == 3) || i == 16) || i == 2) || i == 15
      format: c_expression
