- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 4cd35c8f-b079-48de-9a7d-7a7481199925
    creation_time: 2025-03-22T10:13:48Z
    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/triangular-longest-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-1.i: 81809963fcaff21fd6241cde97e522447f695a8b323a0a16c5a31b7f82b0f683
      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/triangular-longest-1.i
        line: 696
        column: 3
        function: t1
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-1.i
        line: 696
        column: 3
        function: t1
      value: (((((((((((((((((((k == 13 || k == 12) || k == 11) || k == 10) || k ==
        9) || k == 8) || k == 7) || k == 6) || k == 5) || k == 20) || k == 4) || k
        == 19) || k == 3) || k == 18) || k == 2) || k == 17) || k == 1) || k == 16)
        || (0 == k && k == 0)) || k == 15) || k == 14
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-1.i
        line: 704
        column: 3
        function: t2
      value: (unsigned int )arg == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/triangular-longest-1.i
        line: 704
        column: 3
        function: t2
      value: (((((((((((((((((((k == 7 || k == 6) || k == 5) || k == 20) || k == 4)
        || k == 19) || k == 3) || k == 2) || k == 18) || k == 1) || k == 17) || (0
        == k && k == 0)) || k == 16) || k == 15) || k == 14) || k == 13) || k == 12)
        || k == 11) || k == 10) || k == 9) || k == 8
      format: c_expression
