- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 4ec12266-ac33-4954-aecc-57352064c1a9
    creation_time: 2025-03-21T01:07:34Z
    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/forester-heap/dll-queue-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i: c858394bc83ab2c402eb20052f936c0a6aa98b2b6b6c704be79c039778bcff97
      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/forester-heap/dll-queue-1.i
        line: 1039
        column: 3
        function: main
      value: 2 == status
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1039
        column: 3
        function: main
      value: status == 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1027
        column: 3
        function: main
      value: ((3 == status && status == 3) || (2 == status && status == 2)) || (1
        == status && status == 1)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1028
        column: 3
        function: main
      value: ((3 == status && status == 3) || (2 == status && status == 2)) || (1
        == status && status == 1)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1045
        column: 3
        function: main
      value: 3 == status
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1045
        column: 3
        function: main
      value: status == 3
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1053
        column: 2
        function: main
      value: (((((((3 == status && status == 3) || (2 == status && status == 2)) ||
        (1 == status && status == 1)) || ((0 == status && item == 0) && status ==
        0)) || (3 == status && status == 3)) || (3 == status && status == 3)) || ((3
        == status && status == 3) || ((2 == status && item == 0) && status == 2)))
        || (((3 == status && status == 3) || (2 == status && status == 2)) || ((1
        == status && item == 0) && status == 1))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1048
        column: 3
        function: main
      value: 3 == status
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1048
        column: 3
        function: main
      value: status == 3
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1034
        column: 3
        function: main
      value: 1 == status
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1034
        column: 3
        function: main
      value: status == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1055
        column: 3
        function: main
      value: ((((((3 == status && status == 3) || (2 == status && status == 2)) ||
        (1 == status && status == 1)) || (3 == status && status == 3)) || (3 == status
        && status == 3)) || (3 == status && status == 3)) || ((3 == status && status
        == 3) || (2 == status && status == 2))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1060
        column: 2
        function: main
      value: ((((3 == status && status == 3) || ((((((((((2 == status && head == 0)
        && status == 2) || (3 == status && status == 3)) || (3 == status && status
        == 3)) || (3 == status && status == 3)) || (3 == status && status == 3)) ||
        (3 == status && status == 3)) || (3 == status && status == 3)) || (3 == status
        && status == 3)) || (3 == status && status == 3))) || (((((((((((1 == status
        && head == 0) && status == 1) || (3 == status && status == 3)) || (3 == status
        && status == 3)) || (3 == status && status == 3)) || (3 == status && status
        == 3)) || (3 == status && status == 3)) || (3 == status && status == 3)) ||
        (3 == status && status == 3)) || (2 == status && status == 2)) || (3 == status
        && status == 3))) || ((((((((((((0 == status && head == 0) && status == 0)
        || (3 == status && status == 3)) || (3 == status && status == 3)) || (3 ==
        status && status == 3)) || (3 == status && status == 3)) || (3 == status &&
        status == 3)) || (3 == status && status == 3)) || (3 == status && status ==
        3)) || (3 == status && status == 3)) || (2 == status && status == 2)) || (1
        == status && status == 1))) || ((((3 == status && status == 3) || (2 == status
        && status == 2)) || (1 == status && status == 1)) || ((0 == status && item
        == 0) && status == 0))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1047
        column: 3
        function: main
      value: 3 == status
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1047
        column: 3
        function: main
      value: status == 3
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1046
        column: 3
        function: main
      value: 3 == status
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1046
        column: 3
        function: main
      value: status == 3
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1004
        column: 2
        function: main
      value: (((3 == status && status == 3) || (2 == status && status == 2)) || (1
        == status && status == 1)) || ((0 == status && head == item) && status ==
        0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1031
        column: 2
        function: main
      value: (((3 == status && status == 3) || (2 == status && status == 2)) || (1
        == status && status == 1)) || ((0 == status && head == item) && status ==
        0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1040
        column: 3
        function: main
      value: 2 == status
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1040
        column: 3
        function: main
      value: status == 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1035
        column: 3
        function: main
      value: 1 == status
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1035
        column: 3
        function: main
      value: status == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1049
        column: 3
        function: main
      value: 3 == status
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1049
        column: 3
        function: main
      value: status == 3
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1041
        column: 3
        function: main
      value: 2 == status
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-queue-1.i
        line: 1041
        column: 3
        function: main
      value: status == 2
      format: c_expression
