- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: f4f1ee17-53da-44fd-b94b-6d73f75b8af8
    creation_time: 2025-03-21T01:21:49Z
    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/sll-queue-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-queue-1.i: a9a441ad5f70efa202eb02609b90cbc83f5bf4487618c2a09bffcfe320d65f90
      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/sll-queue-1.i
        line: 1058
        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) || (2 == status && 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))) || ((((((((((((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)) || (2 == status && status == 2)) || (3 == status && status == 3)) || (1
        == status && status == 1))) || (((((3 == status && status == 3) || (2 == status
        && status == 2)) || (3 == status && status == 3)) || (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/sll-queue-1.i
        line: 1037
        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/sll-queue-1.i
        line: 1037
        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/sll-queue-1.i
        line: 1038
        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/sll-queue-1.i
        line: 1038
        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/sll-queue-1.i
        line: 1032
        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/sll-queue-1.i
        line: 1032
        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/sll-queue-1.i
        line: 1028
        column: 2
        function: main
      value: ((((3 == status && status == 3) || (2 == status && status == 2)) || (3
        == status && status == 3)) || (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/sll-queue-1.i
        line: 1025
        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/sll-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/sll-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/sll-queue-1.i
        line: 1051
        column: 2
        function: main
      value: ((((((((3 == status && status == 3) || (2 == status && status == 2))
        || (3 == status && status == 3)) || (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))) ||
        ((((3 == status && status == 3) || (2 == status && status == 2)) || (3 ==
        status && status == 3)) || ((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/sll-queue-1.i
        line: 1042
        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/sll-queue-1.i
        line: 1042
        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/sll-queue-1.i
        line: 1036
        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/sll-queue-1.i
        line: 1036
        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/sll-queue-1.i
        line: 1053
        column: 3
        function: main
      value: (((((((3 == status && status == 3) || (2 == status && status == 2)) ||
        (3 == status && status == 3)) || (1 == status && status == 1)) || (3 == status
        && status == 3)) || (3 == status && status == 3)) || (3 == status && status
        == 3)) || (((3 == status && status == 3) || (2 == status && status == 2))
        || (3 == status && status == 3))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-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/sll-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/sll-queue-1.i
        line: 1044
        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/sll-queue-1.i
        line: 1044
        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/sll-queue-1.i
        line: 1024
        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/sll-queue-1.i
        line: 1002
        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/sll-queue-1.i
        line: 1031
        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/sll-queue-1.i
        line: 1031
        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/sll-queue-1.i
        line: 1043
        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/sll-queue-1.i
        line: 1043
        column: 3
        function: main
      value: status == 3
      format: c_expression
