- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 75319196-b740-40ec-9290-16478b6b4b35
    creation_time: 2025-03-21T01:24: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/forester-heap/sll-reverse_simple.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-reverse_simple.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-reverse_simple.i: a7651578256dc791e0a036690d99e12094845a58f582fb99f9abee48c7c5dfba
      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-reverse_simple.i
        line: 1046
        column: 3
        function: main
      value: head == prev
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-reverse_simple.i
        line: 1046
        column: 3
        function: main
      value: ((((((((t1 == 0 || t1 == 1) || t1 == 2) && ((((t2 == 0 || t2 == 1) ||
        t2 == 2) || (next == 0 && (t2 == 0 || t2 == 1))) || ((t2 == 0 || t2 == 1)
        || t2 == 2))) || (((0 == t2 && next == 0) && t2 == 0) && (t1 == 0 || t1 ==
        1))) || (((t1 == 0 || t1 == 1) || t1 == 2) && ((t2 == 0 || t2 == 1) || t2
        == 2))) || (((t1 == 0 || t1 == 1) || t1 == 2) && ((t2 == 0 || t2 == 1) ||
        t2 == 2))) || ((head == x && x == prev) && ((((t1 == 0 || t1 == 1) || t1 ==
        2) && ((((t2 == 0 || t2 == 1) || t2 == 2) || (next == 0 && (t2 == 0 || t2
        == 1))) || ((t2 == 0 || t2 == 1) || t2 == 2))) || ((next == 0 && t1 == 2)
        && t2 == 1)))) || (((((((t1 == 0 || t1 == 1) || t1 == 2) && ((t2 == 0 || t2
        == 1) || t2 == 2)) || (((0 == t2 && next == 0) && t2 == 0) && (t1 == 0 ||
        t1 == 1))) || (((t1 == 0 || t1 == 1) || t1 == 2) && ((t2 == 0 || t2 == 1)
        || t2 == 2))) || (((t1 == 0 || t1 == 1) || t1 == 2) && ((t2 == 0 || t2 ==
        1) || t2 == 2))) || (((t1 == 0 || t1 == 1) || t1 == 2) && ((t2 == 0 || t2
        == 1) || t2 == 2)))) || ((((((t1 == 0 || t1 == 1) || t1 == 2) && ((((t2 ==
        0 || t2 == 1) || t2 == 2) || (next == 0 && (t2 == 0 || t2 == 1))) || ((t2
        == 0 || t2 == 1) || t2 == 2))) || (((0 == t2 && next == 0) && t2 == 0) &&
        (t1 == 0 || t1 == 1))) || (((t1 == 0 || t1 == 1) || t1 == 2) && ((t2 == 0
        || t2 == 1) || t2 == 2))) || (((t1 == 0 || t1 == 1) || t1 == 2) && ((t2 ==
        0 || t2 == 1) || t2 == 2)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-reverse_simple.i
        line: 1057
        column: 2
        function: main
      value: (((t1 == 0 || t1 == 1) || t1 == 2) && (((((t2 == 0 || t2 == 1) || t2
        == 2) || ((((((((((((((((((((x == 0 && next == 0) && (t2 == 0 || t2 == 1))
        || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2))
        || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2))
        || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2))
        || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2))
        || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2))
        || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2))
        || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2))
        || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2))
        || ((t2 == 0 || t2 == 1) || t2 == 2)) || (next == 0 && ((t2 == 0 || t2 ==
        1) || t2 == 2)))) || (((((((((((((((((((((x == 0 && next == 0) && (t2 == 0
        || t2 == 1)) || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1)
        || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1)
        || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1)
        || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1)
        || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1)
        || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1)
        || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1)
        || t2 == 2)) || ((t2 == 0 || t2 == 1) || t2 == 2)) || ((t2 == 0 || t2 == 1)
        || t2 == 2)) || (next == 0 && ((t2 == 0 || t2 == 1) || t2 == 2))) || ((t2
        == 0 || t2 == 1) || t2 == 2)) || (next == 0 && (t2 == 0 || t2 == 1)))) ||
        (head == prev && (((((t2 == 0 || t2 == 1) || t2 == 2) || (next == 0 && (t2
        == 0 || t2 == 1))) || ((t2 == 0 || t2 == 1) || t2 == 2)) || (next == 0 &&
        (t2 == 0 || t2 == 1)))))) || (((head == x && head == prev) && x == prev) &&
        ((((t1 == 0 || t1 == 1) || t1 == 2) && ((((((t2 == 0 || t2 == 1) || t2 ==
        2) || (next == 0 && (t2 == 0 || t2 == 1))) || ((t2 == 0 || t2 == 1) || t2
        == 2)) || (next == 0 && (t2 == 0 || t2 == 1))) || ((t2 == 0 || t2 == 1) ||
        t2 == 2))) || ((next == 0 && t1 == 2) && t2 == 1)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-reverse_simple.i
        line: 1025
        column: 2
        function: main
      value: x == next || ((0 == prev && head == x) && prev == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-reverse_simple.i
        line: 1040
        column: 2
        function: main
      value: head == prev
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/sll-reverse_simple.i
        line: 1040
        column: 2
        function: main
      value: (((((((t1 == 0 || t1 == 1) || t1 == 2) && ((((t2 == 0 || t2 == 1) ||
        t2 == 2) || (next == 0 && (t2 == 0 || t2 == 1))) || ((t2 == 0 || t2 == 1)
        || t2 == 2))) || (((x == 0 && next == 0) && t1 == 2) && t2 == 1)) || (((((((t1
        == 0 || t1 == 1) || t1 == 2) && ((t2 == 0 || t2 == 1) || t2 == 2)) || ((((0
        == t2 && x == 0) && next == 0) && t2 == 0) && (t1 == 0 || t1 == 1))) || (((t1
        == 0 || t1 == 1) || t1 == 2) && ((t2 == 0 || t2 == 1) || t2 == 2))) || (((t1
        == 0 || t1 == 1) || t1 == 2) && ((t2 == 0 || t2 == 1) || t2 == 2))) || (((t1
        == 0 || t1 == 1) || t1 == 2) && ((t2 == 0 || t2 == 1) || t2 == 2)))) || (head
        == x && x == prev)) || ((((((t1 == 0 || t1 == 1) || t1 == 2) && ((((t2 ==
        0 || t2 == 1) || t2 == 2) || (next == 0 && (t2 == 0 || t2 == 1))) || ((t2
        == 0 || t2 == 1) || t2 == 2))) || ((((0 == t2 && x == 0) && next == 0) &&
        t2 == 0) && (t1 == 0 || t1 == 1))) || (((t1 == 0 || t1 == 1) || t1 == 2) &&
        ((t2 == 0 || t2 == 1) || t2 == 2))) || (((t1 == 0 || t1 == 1) || t1 == 2)
        && ((t2 == 0 || t2 == 1) || t2 == 2)))) || (((((t1 == 0 || t1 == 1) || t1
        == 2) && ((((t2 == 0 || t2 == 1) || t2 == 2) || (next == 0 && (t2 == 0 ||
        t2 == 1))) || ((t2 == 0 || t2 == 1) || t2 == 2))) || ((((0 == t2 && x == 0)
        && next == 0) && t2 == 0) && (t1 == 0 || t1 == 1))) || (((t1 == 0 || t1 ==
        1) || t1 == 2) && ((t2 == 0 || t2 == 1) || t2 == 2)))
      format: c_expression
