- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 5c092f62-eca4-4396-bc98-298af1ad9ca2
    creation_time: 2025-03-21T01:25:29Z
    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/list-ext3-properties/sll_of_sll_nondet_append-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i: fabf091179f48b7141dc193b5040f4974c042bd8a2afb03b99137d693bf63ce7
      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/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 599
        column: 3
        function: sll_length
      value: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((4 <=
        len || (head == 0 && len == 4)) || 4 <= len) || 4 <= len) || (head == 0 &&
        len == 4)) || (head == 0 && len == 4)) || 4 <= len) || (head == 0 && len ==
        4)) || 4 <= len) || 4 <= len) || 4 <= len) || 4 <= len) || 4 <= len) || 4
        <= len) || 4 <= len) || 4 <= len) || 4 <= len) || 4 <= len) || 4 <= len) ||
        (head == 0 && len == 4)) || (head == 0 && len == 4)) || 4 <= len) || (head
        == 0 && len == 4)) || 4 <= len) || 4 <= len) || 4 <= len) || 4 <= len) ||
        4 <= len) || 4 <= len) || 4 <= len) || 4 <= len) || (head == 0 && len == 4))
        || 4 <= len) || (head == 0 && len == 4)) || 4 <= len) || (head == 0 && len
        == 4)) || 4 <= len) || 4 <= len) || (head == 0 && len == 4)) || 4 <= len)
        || (head == 0 && len == 4)) || 4 <= len) || 4 <= len) || (head == 0 && len
        == 4)) || 4 <= len) || (head == 0 && len == 4)) || 4 <= len) || 4 <= len)
        || 4 <= len) || 4 <= len) || (head == 0 && len == 4)) || 4 <= len) || (head
        == 0 && len == 4)) || 4 <= len) || (head == 0 && len == 4)) || 4 <= len) ||
        (head == 0 && len == 4)) || 4 <= len) || (head == 0 && len == 4)) || 4 <=
        len) || (head == 0 && len == 4)) || 4 <= len) || (head == 0 && len == 4))
        || len == 3) || len == 2) || len == 1) || (0 == len && len == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 637
        column: 5
        function: main
      value: 3 == min
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 637
        column: 5
        function: main
      value: 5 == max
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 637
        column: 5
        function: main
      value: (int )min == 3
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 637
        column: 5
        function: main
      value: (int )max == 5
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 637
        column: 5
        function: main
      value: (((((((((((((((((((((((((((3 == i && min == i) && i == 3) && (((((((j
        == 7 || j == 6) || j == 5) || j == 4) || j == 3) || j == 2) || j == 1) ||
        ((((0 == j && 0 == head) && j == 0) && j == head) && head == 0))) || (i ==
        5 && j == 10)) || (i == 5 && j == 9)) || (i == 5 && j == 8)) || (i == 5 &&
        j == 7)) || (i == 5 && j == 6)) || (i == 5 && j == 5)) || (i == 5 && j ==
        4)) || (i == 5 && j == 3)) || (i == 5 && j == 2)) || (i == 5 && j == 1)) ||
        ((0 == j && i == 5) && j == 0)) || (i == 4 && j == 10)) || (i == 4 && j ==
        9)) || (i == 4 && j == 8)) || (i == 4 && j == 7)) || (i == 4 && j == 6)) ||
        (i == 4 && j == 5)) || (i == 4 && j == 4)) || (i == 4 && j == 3)) || (i ==
        4 && j == 2)) || (i == 4 && j == 1)) || ((0 == j && i == 4) && j == 0)) ||
        (((3 == i && min == i) && i == 3) && j == 10)) || (((3 == i && min == i) &&
        i == 3) && j == 9)) || (((3 == i && min == i) && i == 3) && j == 8)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 646
        column: 5
        function: main
      value: 3 == min
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 646
        column: 5
        function: main
      value: 5 == max
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 646
        column: 5
        function: main
      value: (int )min == 3
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 646
        column: 5
        function: main
      value: (int )max == 5
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 646
        column: 5
        function: main
      value: ((((((((((i == 5 && ((count == 5 && (((((((((((((((((((((((((((((((j
        == 6 || j == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) ||
        j == 4) || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3)
        || j == 2) || j == 2) || j == 3) || j == 2) || j == 1) || j == 1) || j ==
        1) || j == 1) || j == 5) || (j == 4 && ptr == 0)) || (j == 4 && ptr == 0))
        || (j == 4 && ptr == 0)) || j == 2) || j == 1) || j == 1) || ((((((((((((((((((((((((((((((((((j
        == 6 || j == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) ||
        j == 4) || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3)
        || j == 2) || j == 2) || j == 3) || j == 2) || j == 1) || j == 1) || j ==
        1) || j == 1) || j == 5) || j == 4) || j == 4) || (j == 3 && ptr == 0)) ||
        (j == 3 && ptr == 0)) || (j == 3 && ptr == 0)) || j == 4) || (j == 3 && ptr
        == 0)) || (j == 3 && ptr == 0)) || (j == 3 && ptr == 0)) || j == 2) || j ==
        1) || j == 1)) || ((((((((((((((((((((((((((((((((((((((((((((j == 6 || j
        == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) || j == 4) ||
        j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3) || j == 2)
        || j == 2) || j == 3) || j == 2) || j == 1) || j == 1) || j == 1) || j ==
        1) || j == 5) || j == 4) || j == 4) || j == 3) || j == 3) || (j == 2 && ptr
        == 0)) || (j == 2 && ptr == 0)) || j == 3) || (j == 2 && ptr == 0)) || j ==
        4) || j == 3) || (j == 2 && ptr == 0)) || j == 3) || (j == 2 && ptr == 0))
        || j == 3) || (j == 2 && ptr == 0)) || j == 2) || j == 1) || j == 1) || (j
        == 2 && ptr == 0)) || (j == 2 && ptr == 0)) || (j == 2 && ptr == 0)) || (j
        == 2 && ptr == 0))) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((j
        == 6 || j == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) ||
        j == 4) || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3)
        || j == 2) || j == 2) || j == 3) || j == 2) || j == 1) || j == 1) || j ==
        1) || j == 1) || j == 5) || j == 4) || j == 4) || j == 3) || j == 3) || j
        == 2) || j == 2) || j == 3) || j == 2) || (j == 1 && ptr == 0)) || (j == 1
        && ptr == 0)) || (j == 1 && ptr == 0)) || j == 4) || j == 3) || j == 2) ||
        j == 3) || j == 2) || j == 3) || j == 2) || (j == 1 && ptr == 0)) || (j ==
        1 && ptr == 0)) || (j == 1 && ptr == 0)) || j == 2) || j == 1) || j == 1)
        || j == 2) || (j == 1 && ptr == 0)) || (j == 1 && ptr == 0)) || j == 2) ||
        j == 2) || j == 2) || (j == 1 && ptr == 0)) || (j == 1 && ptr == 0)) || (j
        == 1 && ptr == 0)) || (j == 1 && ptr == 0)) || (j == 1 && ptr == 0)) || (j
        == 1 && ptr == 0)) || (j == 1 && ptr == 0)))) || (((((((((((((((((((((((((((((((((((((((4
        <= count && count <= 6) && ((((((((((((((((((((((j == 6 || j == 7) || j ==
        8) || j == 9) || j == 10) || j == 5) || j == 5) || j == 4) || j == 3) || j
        == 2) || j == 4) || j == 4) || j == 3) || j == 3) || j == 2) || j == 2) ||
        j == 3) || j == 2) || j == 1) || j == 1) || j == 1) || j == 1) || j == 5))
        || (j == 4 && (count == 4 || count == 5))) || ((4 <= count && count <= 6)
        && j == 4)) || (j == 3 && (count == 4 || count == 5))) || (j == 3 && (count
        == 4 || count == 5))) || (j == 2 && (count == 4 || count == 5))) || (j ==
        2 && (count == 4 || count == 5))) || ((4 <= count && count <= 6) && j == 3))
        || (j == 2 && (count == 4 || count == 5))) || (j == 1 && (count == 4 || count
        == 5))) || (j == 1 && (count == 4 || count == 5))) || (j == 1 && (count ==
        4 || count == 5))) || ((4 <= count && count <= 6) && j == 4)) || (j == 3 &&
        (count == 4 || count == 5))) || (j == 2 && (count == 4 || count == 5))) ||
        ((4 <= count && count <= 6) && j == 3)) || (j == 2 && (count == 4 || count
        == 5))) || ((4 <= count && count <= 6) && j == 3)) || (j == 2 && (count ==
        4 || count == 5))) || (j == 1 && (count == 4 || count == 5))) || (j == 1 &&
        (count == 4 || count == 5))) || (j == 1 && (count == 4 || count == 5))) ||
        ((4 <= count && count <= 6) && j == 2)) || ((4 <= count && count <= 6) &&
        j == 1)) || ((4 <= count && count <= 6) && j == 1)) || ((4 <= count && count
        <= 6) && j == 2)) || (j == 1 && (count == 4 || count == 5))) || ((4 <= count
        && count <= 6) && j == 1)) || ((4 <= count && count <= 6) && j == 2)) || ((4
        <= count && count <= 6) && j == 2)) || ((4 <= count && count <= 6) && j ==
        2)) || (j == 1 && (count == 4 || count == 5))) || (j == 1 && (count == 4 ||
        count == 5))) || ((4 <= count && count <= 6) && j == 1)) || ((4 <= count &&
        count <= 6) && j == 1)) || (j == 1 && (count == 4 || count == 5))) || ((4
        <= count && count <= 6) && j == 1)) || ((4 <= count && count <= 6) && j ==
        1)))) || ((((((((((((((((((((((((((((((((4 <= i && 4 <= count) && i <= 5)
        && count <= 5) && ((((((((((((((((((j == 6 || j == 7) || j == 8) || j == 9)
        || j == 10) || j == 5) || j == 5) || j == 4) || j == 3) || j == 2) || j ==
        4) || j == 4) || j == 3) || j == 3) || j == 2) || j == 2) || j == 3) || j
        == 2) || j == 1)) || (((0 == j && i == 4) && j == 0) && count == 4)) || ((((4
        <= i && 4 <= count) && i <= 5) && count <= 5) && j == 1)) || ((((4 <= i &&
        4 <= count) && i <= 5) && count <= 5) && j == 1)) || (((0 == j && i == 4)
        && j == 0) && count == 4)) || (((0 == j && i == 4) && j == 0) && count ==
        4)) || ((((4 <= i && 4 <= count) && i <= 5) && count <= 5) && j == 1)) ||
        (((0 == j && i == 4) && j == 0) && count == 4)) || ((((4 <= i && 4 <= count)
        && i <= 5) && count <= 5) && j == 5)) || ((i == 4 && j == 4) && count == 4))
        || (((((4 <= i && 4 <= count) && i <= 5) && count <= 5) && j == 4) && ptr
        == 0)) || ((i == 4 && j == 3) && count == 4)) || (((i == 4 && j == 3) && ptr
        == 0) && count == 4)) || ((i == 4 && j == 2) && count == 4)) || (((i == 4
        && j == 2) && ptr == 0) && count == 4)) || ((i == 4 && j == 1) && count ==
        4)) || (((i == 4 && j == 1) && ptr == 0) && count == 4)) || (((0 == j && i
        == 4) && j == 0) && count == 4)) || ((((0 == j && i == 4) && j == 0) && ptr
        == 0) && count == 4)) || (((((4 <= i && 4 <= count) && i <= 5) && count <=
        5) && j == 4) && ptr == 0)) || (((i == 4 && j == 3) && ptr == 0) && count
        == 4)) || (((i == 4 && j == 2) && ptr == 0) && count == 4)) || (((i == 4 &&
        j == 1) && ptr == 0) && count == 4)) || ((((0 == j && i == 4) && j == 0) &&
        ptr == 0) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5) && count
        <= 5) && j == 2)) || ((((4 <= i && 4 <= count) && i <= 5) && count <= 5) &&
        j == 1)) || (((0 == j && i == 4) && j == 0) && count == 4)) || ((((4 <= i
        && 4 <= count) && i <= 5) && count <= 5) && j == 1)) || (((0 == j && i ==
        4) && j == 0) && count == 4))) || ((((((((((((((((((((((((((((((((((((((((((((4
        <= i && 4 <= count) && i <= 5) && count <= 5) && ((((((((((((((((((j == 6
        || j == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) || j ==
        4) || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3) || j
        == 2) || j == 2) || j == 3) || j == 2) || j == 1)) || (((0 == j && i == 4)
        && j == 0) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5) && count
        <= 5) && j == 1)) || ((((4 <= i && 4 <= count) && i <= 5) && count <= 5) &&
        j == 1)) || (((0 == j && i == 4) && j == 0) && count == 4)) || (((0 == j &&
        i == 4) && j == 0) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5)
        && count <= 5) && j == 1)) || (((0 == j && i == 4) && j == 0) && count ==
        4)) || ((((4 <= i && 4 <= count) && i <= 5) && count <= 5) && j == 5)) ||
        ((i == 4 && j == 4) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5)
        && count <= 5) && j == 4)) || ((i == 4 && j == 3) && count == 4)) || ((i ==
        4 && j == 3) && count == 4)) || ((i == 4 && j == 2) && count == 4)) || ((i
        == 4 && j == 2) && count == 4)) || (((((4 <= i && 4 <= count) && i <= 5) &&
        count <= 5) && j == 3) && ptr == 0)) || (((i == 4 && j == 2) && ptr == 0)
        && count == 4)) || ((i == 4 && j == 1) && count == 4)) || ((i == 4 && j ==
        1) && count == 4)) || (((0 == j && i == 4) && j == 0) && count == 4)) || (((0
        == j && i == 4) && j == 0) && count == 4)) || (((i == 4 && j == 1) && ptr
        == 0) && count == 4)) || ((((0 == j && i == 4) && j == 0) && ptr == 0) &&
        count == 4)) || ((((4 <= i && 4 <= count) && i <= 5) && count <= 5) && j ==
        4)) || ((i == 4 && j == 3) && count == 4)) || ((i == 4 && j == 2) && count
        == 4)) || (((((4 <= i && 4 <= count) && i <= 5) && count <= 5) && j == 3)
        && ptr == 0)) || (((i == 4 && j == 2) && ptr == 0) && count == 4)) || (((((4
        <= i && 4 <= count) && i <= 5) && count <= 5) && j == 3) && ptr == 0)) ||
        (((i == 4 && j == 2) && ptr == 0) && count == 4)) || ((i == 4 && j == 1) &&
        count == 4)) || (((0 == j && i == 4) && j == 0) && count == 4)) || (((i ==
        4 && j == 1) && ptr == 0) && count == 4)) || ((((0 == j && i == 4) && j ==
        0) && ptr == 0) && count == 4)) || (((i == 4 && j == 1) && ptr == 0) && count
        == 4)) || ((((0 == j && i == 4) && j == 0) && ptr == 0) && count == 4)) ||
        ((((4 <= i && 4 <= count) && i <= 5) && count <= 5) && j == 2)) || ((((4 <=
        i && 4 <= count) && i <= 5) && count <= 5) && j == 1)) || (((0 == j && i ==
        4) && j == 0) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5) && count
        <= 5) && j == 1)) || (((0 == j && i == 4) && j == 0) && count == 4))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((4
        <= i && 4 <= count) && i <= 5) && count <= 5) && ((((((((((((((((((j == 6
        || j == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) || j ==
        4) || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3) || j
        == 2) || j == 2) || j == 3) || j == 2) || j == 1)) || (((0 == j && i == 4)
        && j == 0) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5) && count
        <= 5) && j == 1)) || ((((4 <= i && 4 <= count) && i <= 5) && count <= 5) &&
        j == 1)) || (((0 == j && i == 4) && j == 0) && count == 4)) || (((0 == j &&
        i == 4) && j == 0) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5)
        && count <= 5) && j == 1)) || (((0 == j && i == 4) && j == 0) && count ==
        4)) || ((((4 <= i && 4 <= count) && i <= 5) && count <= 5) && j == 5)) ||
        ((i == 4 && j == 4) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5)
        && count <= 5) && j == 4)) || ((i == 4 && j == 3) && count == 4)) || ((i ==
        4 && j == 3) && count == 4)) || ((i == 4 && j == 2) && count == 4)) || ((i
        == 4 && j == 2) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5) &&
        count <= 5) && j == 3)) || ((i == 4 && j == 2) && count == 4)) || ((i == 4
        && j == 1) && count == 4)) || ((i == 4 && j == 1) && count == 4)) || (((0
        == j && i == 4) && j == 0) && count == 4)) || (((0 == j && i == 4) && j ==
        0) && count == 4)) || ((i == 4 && j == 1) && count == 4)) || (((0 == j &&
        i == 4) && j == 0) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5)
        && count <= 5) && j == 4)) || ((i == 4 && j == 3) && count == 4)) || ((i ==
        4 && j == 2) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5) && count
        <= 5) && j == 3)) || ((i == 4 && j == 2) && count == 4)) || ((((4 <= i &&
        4 <= count) && i <= 5) && count <= 5) && j == 3)) || ((i == 4 && j == 2) &&
        count == 4)) || ((i == 4 && j == 1) && count == 4)) || (((0 == j && i == 4)
        && j == 0) && count == 4)) || ((i == 4 && j == 1) && count == 4)) || (((0
        == j && i == 4) && j == 0) && count == 4)) || ((i == 4 && j == 1) && count
        == 4)) || (((0 == j && i == 4) && j == 0) && count == 4)) || ((((4 <= i &&
        4 <= count) && i <= 5) && count <= 5) && j == 2)) || ((((4 <= i && 4 <= count)
        && i <= 5) && count <= 5) && j == 1)) || (((0 == j && i == 4) && j == 0) &&
        count == 4)) || ((((4 <= i && 4 <= count) && i <= 5) && count <= 5) && j ==
        1)) || (((0 == j && i == 4) && j == 0) && count == 4)) || (((((4 <= i && 4
        <= count) && i <= 5) && count <= 5) && j == 2) && ptr == 0)) || (((i == 4
        && j == 1) && ptr == 0) && count == 4)) || ((((0 == j && i == 4) && j == 0)
        && ptr == 0) && count == 4)) || (((((4 <= i && 4 <= count) && i <= 5) && count
        <= 5) && j == 2) && ptr == 0)) || (((((4 <= i && 4 <= count) && i <= 5) &&
        count <= 5) && j == 2) && ptr == 0)) || (((((4 <= i && 4 <= count) && i <=
        5) && count <= 5) && j == 2) && ptr == 0)) || (((i == 4 && j == 1) && ptr
        == 0) && count == 4)) || ((((0 == j && i == 4) && j == 0) && ptr == 0) &&
        count == 4)) || (((i == 4 && j == 1) && ptr == 0) && count == 4)) || ((((0
        == j && i == 4) && j == 0) && ptr == 0) && count == 4)) || (((i == 4 && j
        == 1) && ptr == 0) && count == 4)) || ((((0 == j && i == 4) && j == 0) &&
        ptr == 0) && count == 4))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((4
        <= i && 4 <= count) && i <= 5) && count <= 5) && ((((((((((((((((((j == 6
        || j == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) || j ==
        4) || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3) || j
        == 2) || j == 2) || j == 3) || j == 2) || j == 1)) || (((0 == j && i == 4)
        && j == 0) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5) && count
        <= 5) && j == 1)) || ((((4 <= i && 4 <= count) && i <= 5) && count <= 5) &&
        j == 1)) || (((0 == j && i == 4) && j == 0) && count == 4)) || (((0 == j &&
        i == 4) && j == 0) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5)
        && count <= 5) && j == 1)) || (((0 == j && i == 4) && j == 0) && count ==
        4)) || ((((4 <= i && 4 <= count) && i <= 5) && count <= 5) && j == 5)) ||
        ((i == 4 && j == 4) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5)
        && count <= 5) && j == 4)) || ((i == 4 && j == 3) && count == 4)) || ((i ==
        4 && j == 3) && count == 4)) || ((i == 4 && j == 2) && count == 4)) || ((i
        == 4 && j == 2) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5) &&
        count <= 5) && j == 3)) || ((i == 4 && j == 2) && count == 4)) || ((i == 4
        && j == 1) && count == 4)) || ((i == 4 && j == 1) && count == 4)) || (((0
        == j && i == 4) && j == 0) && count == 4)) || (((0 == j && i == 4) && j ==
        0) && count == 4)) || ((i == 4 && j == 1) && count == 4)) || (((0 == j &&
        i == 4) && j == 0) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5)
        && count <= 5) && j == 4)) || ((i == 4 && j == 3) && count == 4)) || ((i ==
        4 && j == 2) && count == 4)) || ((((4 <= i && 4 <= count) && i <= 5) && count
        <= 5) && j == 3)) || ((i == 4 && j == 2) && count == 4)) || ((((4 <= i &&
        4 <= count) && i <= 5) && count <= 5) && j == 3)) || ((i == 4 && j == 2) &&
        count == 4)) || ((i == 4 && j == 1) && count == 4)) || (((0 == j && i == 4)
        && j == 0) && count == 4)) || ((i == 4 && j == 1) && count == 4)) || (((0
        == j && i == 4) && j == 0) && count == 4)) || ((i == 4 && j == 1) && count
        == 4)) || (((0 == j && i == 4) && j == 0) && count == 4)) || ((((4 <= i &&
        4 <= count) && i <= 5) && count <= 5) && j == 2)) || ((((4 <= i && 4 <= count)
        && i <= 5) && count <= 5) && j == 1)) || (((0 == j && i == 4) && j == 0) &&
        count == 4)) || ((((4 <= i && 4 <= count) && i <= 5) && count <= 5) && j ==
        1)) || (((0 == j && i == 4) && j == 0) && count == 4)) || ((((4 <= i && 4
        <= count) && i <= 5) && count <= 5) && j == 2)) || ((i == 4 && j == 1) &&
        count == 4)) || (((0 == j && i == 4) && j == 0) && count == 4)) || (((((4
        <= i && 4 <= count) && i <= 5) && count <= 5) && j == 1) && ptr == 0)) ||
        ((((0 == j && i == 4) && j == 0) && ptr == 0) && count == 4)) || ((((4 <=
        i && 4 <= count) && i <= 5) && count <= 5) && j == 2)) || ((((4 <= i && 4
        <= count) && i <= 5) && count <= 5) && j == 2)) || ((((4 <= i && 4 <= count)
        && i <= 5) && count <= 5) && j == 2)) || ((i == 4 && j == 1) && count == 4))
        || (((0 == j && i == 4) && j == 0) && count == 4)) || ((i == 4 && j == 1)
        && count == 4)) || (((0 == j && i == 4) && j == 0) && count == 4)) || (((((4
        <= i && 4 <= count) && i <= 5) && count <= 5) && j == 1) && ptr == 0)) ||
        ((((0 == j && i == 4) && j == 0) && ptr == 0) && count == 4)) || (((((4 <=
        i && 4 <= count) && i <= 5) && count <= 5) && j == 1) && ptr == 0)) || ((((0
        == j && i == 4) && j == 0) && ptr == 0) && count == 4)) || ((i == 4 && j ==
        1) && count == 4)) || (((0 == j && i == 4) && j == 0) && count == 4)) || (((((4
        <= i && 4 <= count) && i <= 5) && count <= 5) && j == 1) && ptr == 0)) ||
        ((((0 == j && i == 4) && j == 0) && ptr == 0) && count == 4)) || (((((4 <=
        i && 4 <= count) && i <= 5) && count <= 5) && j == 1) && ptr == 0)) || ((((0
        == j && i == 4) && j == 0) && ptr == 0) && count == 4))) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((4
        <= i && i <= 5) && ((count == 3 || count == 4) || count == 5)) && ((((((((((((((((((j
        == 6 || j == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) ||
        j == 4) || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3)
        || j == 2) || j == 2) || j == 3) || j == 2) || j == 1)) || (((0 == j && i
        == 4) && j == 0) && (count == 3 || count == 4))) || (((4 <= i && i <= 5) &&
        j == 1) && ((count == 3 || count == 4) || count == 5))) || (((4 <= i && i
        <= 5) && j == 1) && ((count == 3 || count == 4) || count == 5))) || (((0 ==
        j && i == 4) && j == 0) && (count == 3 || count == 4))) || (((0 == j && i
        == 4) && j == 0) && (count == 3 || count == 4))) || (((4 <= i && i <= 5) &&
        j == 1) && ((count == 3 || count == 4) || count == 5))) || (((0 == j && i
        == 4) && j == 0) && (count == 3 || count == 4))) || ((((4 <= i && i <= 5)
        && j == 5) && head == ptr) && (count == 4 || count == 5))) || (((i == 4 &&
        j == 4) && head == ptr) && count == 4)) || (((4 <= i && i <= 5) && j == 4)
        && (count == 4 || count == 5))) || (((i == 4 && j == 3) && head == ptr) &&
        count == 4)) || ((i == 4 && j == 3) && count == 4)) || (((i == 4 && j == 2)
        && head == ptr) && count == 4)) || ((i == 4 && j == 2) && count == 4)) ||
        (((4 <= i && i <= 5) && j == 3) && (count == 4 || count == 5))) || ((i ==
        4 && j == 2) && count == 4)) || (((i == 4 && j == 1) && head == ptr) && count
        == 4)) || ((i == 4 && j == 1) && count == 4)) || ((((0 == j && i == 4) &&
        j == 0) && head == ptr) && count == 4)) || (((0 == j && i == 4) && j == 0)
        && count == 4)) || ((i == 4 && j == 1) && count == 4)) || (((0 == j && i ==
        4) && j == 0) && count == 4)) || ((((4 <= i && i <= 5) && j == 4) && head
        == ptr) && (count == 4 || count == 5))) || (((i == 4 && j == 3) && head ==
        ptr) && count == 4)) || (((i == 4 && j == 2) && head == ptr) && count == 4))
        || (((4 <= i && i <= 5) && j == 3) && (count == 4 || count == 5))) || ((i
        == 4 && j == 2) && count == 4)) || ((((4 <= i && i <= 5) && j == 3) && head
        == ptr) && (count == 4 || count == 5))) || (((i == 4 && j == 2) && head ==
        ptr) && count == 4)) || (((i == 4 && j == 1) && head == ptr) && count == 4))
        || ((((0 == j && i == 4) && j == 0) && head == ptr) && count == 4)) || ((i
        == 4 && j == 1) && count == 4)) || (((0 == j && i == 4) && j == 0) && count
        == 4)) || (((i == 4 && j == 1) && head == ptr) && count == 4)) || ((((0 ==
        j && i == 4) && j == 0) && head == ptr) && count == 4)) || (((4 <= i && i
        <= 5) && j == 2) && ((count == 3 || count == 4) || count == 5))) || (((4 <=
        i && i <= 5) && j == 1) && ((count == 3 || count == 4) || count == 5))) ||
        (((0 == j && i == 4) && j == 0) && (count == 3 || count == 4))) || (((4 <=
        i && i <= 5) && j == 1) && ((count == 3 || count == 4) || count == 5))) ||
        (((0 == j && i == 4) && j == 0) && (count == 3 || count == 4))) || (((4 <=
        i && i <= 5) && j == 2) && (count == 4 || count == 5))) || ((i == 4 && j ==
        1) && count == 4)) || (((0 == j && i == 4) && j == 0) && count == 4)) || (((4
        <= i && i <= 5) && j == 1) && (count == 4 || count == 5))) || (((0 == j &&
        i == 4) && j == 0) && count == 4)) || (((4 <= i && i <= 5) && j == 2) && (count
        == 4 || count == 5))) || (((4 <= i && i <= 5) && j == 2) && (count == 4 ||
        count == 5))) || ((((4 <= i && i <= 5) && j == 2) && head == ptr) && (count
        == 4 || count == 5))) || ((i == 4 && j == 1) && count == 4)) || (((0 == j
        && i == 4) && j == 0) && count == 4)) || ((i == 4 && j == 1) && count == 4))
        || (((0 == j && i == 4) && j == 0) && count == 4)) || (((4 <= i && i <= 5)
        && j == 1) && (count == 4 || count == 5))) || (((0 == j && i == 4) && j ==
        0) && count == 4)) || (((4 <= i && i <= 5) && j == 1) && (count == 4 || count
        == 5))) || (((0 == j && i == 4) && j == 0) && count == 4)) || (((i == 4 &&
        j == 1) && head == ptr) && count == 4)) || ((((0 == j && i == 4) && j == 0)
        && head == ptr) && count == 4)) || (((4 <= i && i <= 5) && j == 1) && (count
        == 4 || count == 5))) || (((0 == j && i == 4) && j == 0) && count == 4)) ||
        ((((4 <= i && i <= 5) && j == 1) && head == ptr) && (count == 4 || count ==
        5))) || ((((0 == j && i == 4) && j == 0) && head == ptr) && count == 4)))
        || ((((3 == i && min == i) && i == 3) && count == 3) && (((((((((((((((((((((((((((((((((((j
        == 6 || j == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) ||
        j == 4) || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3)
        || j == 2) || j == 2) || j == 3) || j == 2) || j == 1) || (0 == j && j ==
        0)) || j == 1) || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) ||
        j == 1) || (0 == j && j == 0)) || j == 2) || j == 1) || (0 == j && j == 0))
        || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) || j == 1) || (0
        == j && j == 0)) || (0 == j && j == 0)) || ((0 == j && j == 0) && ptr == 0))))
        || ((((3 == i && min == i) && i == 3) && count == 3) && (((((((((((((((((((((((((((((((((((((((((j
        == 6 || j == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) ||
        j == 4) || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3)
        || j == 2) || j == 2) || j == 3) || j == 2) || j == 1) || (0 == j && j ==
        0)) || j == 1) || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) ||
        j == 1) || (0 == j && j == 0)) || j == 2) || j == 1) || (0 == j && j == 0))
        || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) || j == 2) || j ==
        1) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) || (0 == j &&
        j == 0)) || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) || ((0 ==
        j && j == 0) && ptr == 0)))) || ((((3 == i && min == i) && i == 3) && count
        == 3) && (((((((((((((((((((((((((((((((((((((((((((((((((((j == 6 || j ==
        7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) || j == 4) || j
        == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3) || j == 2) ||
        j == 2) || j == 3) || j == 2) || j == 1) || (0 == j && j == 0)) || j == 1)
        || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) || j == 1) || (0
        == j && j == 0)) || j == 3) || j == 2) || j == 1) || (0 == j && j == 0)) ||
        j == 2) || j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0))
        || (0 == j && j == 0)) || j == 2) || j == 1) || (0 == j && j == 0)) || j ==
        1) || (0 == j && j == 0)) || (0 == j && j == 0)) || j == 2) || j == 1) ||
        (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) || j == 1) || (0 ==
        j && j == 0)) || (0 == j && j == 0)) || (0 == j && j == 0)) || ((0 == j &&
        j == 0) && ptr == 0)))) || ((((3 == i && min == i) && i == 3) && count ==
        3) && ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((j
        == 6 || j == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) ||
        j == 4) || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3)
        || j == 2) || j == 2) || j == 3) || j == 2) || j == 1) || (0 == j && j ==
        0)) || j == 1) || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) ||
        j == 1) || (0 == j && j == 0)) || j == 4) || j == 3) || j == 2) || j == 3)
        || j == 2) || j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j ==
        0)) || j == 3) || j == 2) || j == 1) || (0 == j && j == 0)) || j == 2) ||
        j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) || (0 ==
        j && j == 0)) || j == 2) || j == 1) || (0 == j && j == 0)) || j == 1) || (0
        == j && j == 0)) || (0 == j && j == 0)) || j == 2) || j == 2) || j == 1) ||
        (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) || j == 1) || (0 ==
        j && j == 0)) || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) ||
        (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0))
        || ((0 == j && j == 0) && ptr == 0)))) || ((((3 == i && min == i) && i ==
        3) && head == ptr) && ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((j
        == 6 || j == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) ||
        j == 4) || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3)
        || j == 2) || j == 2) || j == 3) || j == 2) || j == 1) || (0 == j && j ==
        0)) || j == 1) || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) ||
        j == 1) || (0 == j && j == 0)) || j == 5) || j == 4) || j == 4) || j == 3)
        || j == 3) || j == 2) || j == 2) || j == 3) || j == 2) || j == 1) || j ==
        1) || (0 == j && j == 0)) || (0 == j && j == 0)) || j == 1) || (0 == j &&
        j == 0)) || j == 4) || j == 3) || j == 2) || j == 3) || j == 2) || j == 3)
        || j == 2) || j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j ==
        0)) || j == 1) || (0 == j && j == 0)) || j == 2) || j == 1) || (0 == j &&
        j == 0)) || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) || j ==
        2) || j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) ||
        (0 == j && j == 0)) || j == 2) || j == 2) || j == 2) || j == 1) || (0 == j
        && j == 0)) || j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j ==
        0)) || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) || (0 == j &&
        j == 0)) || j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0))
        || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) || (0 == j && j ==
        0)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 642
        column: 3
        function: main
      value: 3 == min
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 642
        column: 3
        function: main
      value: 5 == max
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 642
        column: 3
        function: main
      value: (int )min == 3
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 642
        column: 3
        function: main
      value: (int )max == 5
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 642
        column: 3
        function: main
      value: (((((i == 6 && ptr == 0) && count == 5) && (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((j
        == 6 || j == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) ||
        j == 4) || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3)
        || j == 2) || j == 2) || j == 3) || j == 2) || j == 1) || j == 1) || j ==
        1) || j == 1) || j == 5) || j == 4) || j == 4) || j == 3) || j == 3) || j
        == 2) || j == 2) || j == 3) || j == 2) || j == 1) || j == 1) || j == 1) ||
        j == 4) || j == 3) || j == 2) || j == 3) || j == 2) || j == 3) || j == 2)
        || j == 1) || j == 1) || j == 1) || j == 2) || j == 1) || j == 1) || j ==
        2) || j == 1) || j == 1) || j == 2) || j == 2) || j == 2) || j == 1) || j
        == 1) || j == 1) || j == 1) || j == 1) || j == 1) || j == 1)) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((4
        <= count && 5 <= i) && i <= 6) && count <= 6) && ((((((((((((((((((j == 6
        || j == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) || j ==
        4) || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3) || j
        == 2) || j == 2) || j == 3) || j == 2) || j == 1)) || ((((0 == j && i == 5)
        && j == 0) && ptr == 0) && count == 4)) || ((((4 <= count && 5 <= i) && i
        <= 6) && count <= 6) && j == 1)) || ((((4 <= count && 5 <= i) && i <= 6) &&
        count <= 6) && j == 1)) || ((((0 == j && i == 5) && j == 0) && ptr == 0) &&
        count == 4)) || ((((0 == j && i == 5) && j == 0) && ptr == 0) && count ==
        4)) || ((((4 <= count && 5 <= i) && i <= 6) && count <= 6) && j == 1)) ||
        ((((0 == j && i == 5) && j == 0) && ptr == 0) && count == 4)) || ((((4 <=
        count && 5 <= i) && i <= 6) && count <= 6) && j == 5)) || ((i == 5 && j ==
        4) && (count == 4 || count == 5))) || ((((4 <= count && 5 <= i) && i <= 6)
        && count <= 6) && j == 4)) || ((i == 5 && j == 3) && (count == 4 || count
        == 5))) || ((i == 5 && j == 3) && (count == 4 || count == 5))) || ((i == 5
        && j == 2) && (count == 4 || count == 5))) || ((i == 5 && j == 2) && (count
        == 4 || count == 5))) || ((((4 <= count && 5 <= i) && i <= 6) && count <=
        6) && j == 3)) || ((i == 5 && j == 2) && (count == 4 || count == 5))) || ((i
        == 5 && j == 1) && (count == 4 || count == 5))) || ((i == 5 && j == 1) &&
        (count == 4 || count == 5))) || ((((0 == j && i == 5) && j == 0) && ptr ==
        0) && count == 4)) || ((((0 == j && i == 5) && j == 0) && ptr == 0) && count
        == 4)) || ((i == 5 && j == 1) && (count == 4 || count == 5))) || ((((0 ==
        j && i == 5) && j == 0) && ptr == 0) && count == 4)) || ((((4 <= count &&
        5 <= i) && i <= 6) && count <= 6) && j == 4)) || ((i == 5 && j == 3) && (count
        == 4 || count == 5))) || ((i == 5 && j == 2) && (count == 4 || count == 5)))
        || ((((4 <= count && 5 <= i) && i <= 6) && count <= 6) && j == 3)) || ((i
        == 5 && j == 2) && (count == 4 || count == 5))) || ((((4 <= count && 5 <=
        i) && i <= 6) && count <= 6) && j == 3)) || ((i == 5 && j == 2) && (count
        == 4 || count == 5))) || ((i == 5 && j == 1) && (count == 4 || count == 5)))
        || ((((0 == j && i == 5) && j == 0) && ptr == 0) && count == 4)) || ((i ==
        5 && j == 1) && (count == 4 || count == 5))) || ((((0 == j && i == 5) && j
        == 0) && ptr == 0) && count == 4)) || ((i == 5 && j == 1) && (count == 4 ||
        count == 5))) || ((((0 == j && i == 5) && j == 0) && ptr == 0) && count ==
        4)) || ((((4 <= count && 5 <= i) && i <= 6) && count <= 6) && j == 2)) ||
        ((((4 <= count && 5 <= i) && i <= 6) && count <= 6) && j == 1)) || ((((0 ==
        j && i == 5) && j == 0) && ptr == 0) && count == 4)) || ((((4 <= count &&
        5 <= i) && i <= 6) && count <= 6) && j == 1)) || ((((0 == j && i == 5) &&
        j == 0) && ptr == 0) && count == 4)) || ((((4 <= count && 5 <= i) && i <=
        6) && count <= 6) && j == 2)) || ((i == 5 && j == 1) && (count == 4 || count
        == 5))) || ((((0 == j && i == 5) && j == 0) && ptr == 0) && count == 4)) ||
        ((((4 <= count && 5 <= i) && i <= 6) && count <= 6) && j == 1)) || ((((0 ==
        j && i == 5) && j == 0) && ptr == 0) && count == 4)) || ((((4 <= count &&
        5 <= i) && i <= 6) && count <= 6) && j == 2)) || ((((4 <= count && 5 <= i)
        && i <= 6) && count <= 6) && j == 2)) || ((((4 <= count && 5 <= i) && i <=
        6) && count <= 6) && j == 2)) || ((i == 5 && j == 1) && (count == 4 || count
        == 5))) || ((((0 == j && i == 5) && j == 0) && ptr == 0) && count == 4)) ||
        ((i == 5 && j == 1) && (count == 4 || count == 5))) || ((((0 == j && i ==
        5) && j == 0) && ptr == 0) && count == 4)) || ((((4 <= count && 5 <= i) &&
        i <= 6) && count <= 6) && j == 1)) || ((((0 == j && i == 5) && j == 0) &&
        ptr == 0) && count == 4)) || ((((4 <= count && 5 <= i) && i <= 6) && count
        <= 6) && j == 1)) || ((((0 == j && i == 5) && j == 0) && ptr == 0) && count
        == 4)) || ((i == 5 && j == 1) && (count == 4 || count == 5))) || ((((0 ==
        j && i == 5) && j == 0) && ptr == 0) && count == 4)) || ((((4 <= count &&
        5 <= i) && i <= 6) && count <= 6) && j == 1)) || ((((0 == j && i == 5) &&
        j == 0) && ptr == 0) && count == 4)) || ((((4 <= count && 5 <= i) && i <=
        6) && count <= 6) && j == 1)) || ((((0 == j && i == 5) && j == 0) && ptr ==
        0) && count == 4))) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((4
        <= i && i <= 5) && ((count == 3 || count == 4) || count == 5)) && ((((((((((((((((((j
        == 6 || j == 7) || j == 8) || j == 9) || j == 10) || j == 5) || j == 5) ||
        j == 4) || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3)
        || j == 2) || j == 2) || j == 3) || j == 2) || j == 1)) || (((0 == j && i
        == 4) && j == 0) && (count == 3 || count == 4))) || (((4 <= i && i <= 5) &&
        j == 1) && ((count == 3 || count == 4) || count == 5))) || (((4 <= i && i
        <= 5) && j == 1) && ((count == 3 || count == 4) || count == 5))) || (((0 ==
        j && i == 4) && j == 0) && (count == 3 || count == 4))) || (((0 == j && i
        == 4) && j == 0) && (count == 3 || count == 4))) || (((4 <= i && i <= 5) &&
        j == 1) && ((count == 3 || count == 4) || count == 5))) || (((0 == j && i
        == 4) && j == 0) && (count == 3 || count == 4))) || ((((4 <= i && i <= 5)
        && j == 5) && head == ptr) && (count == 4 || count == 5))) || (((i == 4 &&
        j == 4) && head == ptr) && count == 4)) || (((4 <= i && i <= 5) && j == 4)
        && (count == 4 || count == 5))) || (((i == 4 && j == 3) && head == ptr) &&
        count == 4)) || ((i == 4 && j == 3) && count == 4)) || (((i == 4 && j == 2)
        && head == ptr) && count == 4)) || ((i == 4 && j == 2) && count == 4)) ||
        (((4 <= i && i <= 5) && j == 3) && (count == 4 || count == 5))) || ((i ==
        4 && j == 2) && count == 4)) || (((i == 4 && j == 1) && head == ptr) && count
        == 4)) || ((i == 4 && j == 1) && count == 4)) || ((((0 == j && i == 4) &&
        j == 0) && head == ptr) && count == 4)) || (((0 == j && i == 4) && j == 0)
        && count == 4)) || ((i == 4 && j == 1) && count == 4)) || (((0 == j && i ==
        4) && j == 0) && count == 4)) || ((((4 <= i && i <= 5) && j == 4) && head
        == ptr) && (count == 4 || count == 5))) || (((i == 4 && j == 3) && head ==
        ptr) && count == 4)) || (((i == 4 && j == 2) && head == ptr) && count == 4))
        || (((4 <= i && i <= 5) && j == 3) && (count == 4 || count == 5))) || ((i
        == 4 && j == 2) && count == 4)) || ((((4 <= i && i <= 5) && j == 3) && head
        == ptr) && (count == 4 || count == 5))) || (((i == 4 && j == 2) && head ==
        ptr) && count == 4)) || (((i == 4 && j == 1) && head == ptr) && count == 4))
        || ((((0 == j && i == 4) && j == 0) && head == ptr) && count == 4)) || ((i
        == 4 && j == 1) && count == 4)) || (((0 == j && i == 4) && j == 0) && count
        == 4)) || (((i == 4 && j == 1) && head == ptr) && count == 4)) || ((((0 ==
        j && i == 4) && j == 0) && head == ptr) && count == 4)) || (((4 <= i && i
        <= 5) && j == 2) && ((count == 3 || count == 4) || count == 5))) || (((4 <=
        i && i <= 5) && j == 1) && ((count == 3 || count == 4) || count == 5))) ||
        (((0 == j && i == 4) && j == 0) && (count == 3 || count == 4))) || (((4 <=
        i && i <= 5) && j == 1) && ((count == 3 || count == 4) || count == 5))) ||
        (((0 == j && i == 4) && j == 0) && (count == 3 || count == 4))) || ((((0 ==
        j && i == 4) && j == 0) && ptr == 0) && count == 3)) || (((4 <= i && i <=
        5) && j == 2) && (count == 4 || count == 5))) || ((i == 4 && j == 1) && count
        == 4)) || (((0 == j && i == 4) && j == 0) && count == 4)) || (((4 <= i &&
        i <= 5) && j == 1) && (count == 4 || count == 5))) || (((0 == j && i == 4)
        && j == 0) && count == 4)) || ((((0 == j && i == 4) && j == 0) && ptr == 0)
        && count == 3)) || (((4 <= i && i <= 5) && j == 2) && (count == 4 || count
        == 5))) || (((4 <= i && i <= 5) && j == 2) && (count == 4 || count == 5)))
        || ((((4 <= i && i <= 5) && j == 2) && head == ptr) && (count == 4 || count
        == 5))) || ((i == 4 && j == 1) && count == 4)) || (((0 == j && i == 4) &&
        j == 0) && count == 4)) || ((i == 4 && j == 1) && count == 4)) || (((0 ==
        j && i == 4) && j == 0) && count == 4)) || (((4 <= i && i <= 5) && j == 1)
        && (count == 4 || count == 5))) || (((0 == j && i == 4) && j == 0) && count
        == 4)) || (((4 <= i && i <= 5) && j == 1) && (count == 4 || count == 5)))
        || (((0 == j && i == 4) && j == 0) && count == 4)) || ((((0 == j && i == 4)
        && j == 0) && ptr == 0) && count == 3)) || ((((0 == j && i == 4) && j == 0)
        && ptr == 0) && count == 3)) || (((i == 4 && j == 1) && head == ptr) && count
        == 4)) || ((((0 == j && i == 4) && j == 0) && head == ptr) && count == 4))
        || (((4 <= i && i <= 5) && j == 1) && (count == 4 || count == 5))) || (((0
        == j && i == 4) && j == 0) && count == 4)) || ((((0 == j && i == 4) && j ==
        0) && ptr == 0) && count == 3)) || ((((4 <= i && i <= 5) && j == 1) && head
        == ptr) && (count == 4 || count == 5))) || ((((0 == j && i == 4) && j == 0)
        && head == ptr) && count == 4)) || ((((0 == j && i == 4) && j == 0) && ptr
        == 0) && count == 3))) || ((((3 == i && min == i) && i == 3) && head == ptr)
        && ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        == j && 0 == head) && 0 == ptr) && j == 0) && j == head) && j == ptr) && head
        == 0) && ptr == 0) || ((((j == 6 || j == 7) || j == 8) || j == 9) || j ==
        10)) || j == 5) || j == 5) || j == 4) || j == 3) || j == 2) || j == 4) ||
        j == 4) || j == 3) || j == 3) || j == 2) || j == 2) || j == 3) || j == 2)
        || j == 1) || (0 == j && j == 0)) || j == 1) || j == 1) || (0 == j && j ==
        0)) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) || j == 5) ||
        j == 4) || j == 4) || j == 3) || j == 3) || j == 2) || j == 2) || j == 3)
        || j == 2) || j == 1) || j == 1) || (0 == j && j == 0)) || (0 == j && j ==
        0)) || j == 1) || (0 == j && j == 0)) || j == 4) || j == 3) || j == 2) ||
        j == 3) || j == 2) || j == 3) || j == 2) || j == 1) || (0 == j && j == 0))
        || j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) || j ==
        2) || j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) ||
        (0 == j && j == 0)) || j == 2) || j == 1) || (0 == j && j == 0)) || j == 1)
        || (0 == j && j == 0)) || (0 == j && j == 0)) || j == 2) || j == 2) || j ==
        2) || j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) ||
        j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) || (0 ==
        j && j == 0)) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) ||
        j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) || j == 1) || (0 ==
        j && j == 0)) || (0 == j && j == 0)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 577
        column: 3
        function: sll_create
      value: (head == new_head && (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((len
        == 0 || len == 1) || len == 0) || (len == 0 || len == 1)) || (len == 0 ||
        len == 1)) || (len == 0 || len == 1)) || (len == 0 || len == 1)) || len ==
        0) || (len == 0 || len == 1)) || (len == 0 || len == 1)) || (len == 0 || len
        == 1)) || (len == 0 || len == 1)) || len == 0) || (len == 0 || len == 1))
        || (len == 0 || len == 1)) || (len == 0 || len == 1)) || (len == 0 || len
        == 1)) || (len == 0 || len == 1)) || (len == 0 || len == 1)) || (len == 0
        || len == 1)) || (len == 0 || len == 1)) || (len == 0 || len == 1)) || len
        == 0) || (len == 0 || len == 1)) || len == 0) || (len == 0 || len == 1)) ||
        (len == 0 || len == 1)) || (len == 0 || len == 1)) || (len == 0 || len ==
        1)) || len == 0) || (len == 0 || len == 1)) || (len == 0 || len == 1)) ||
        (len == 0 || len == 1)) || (len == 0 || len == 1)) || (len == 0 || len ==
        1)) || (len == 0 || len == 1)) || (len == 0 || len == 1)) || len == 0) ||
        (len == 0 || len == 1)) || (len == 0 || len == 1)) || len == 0) || (len ==
        0 || len == 1)) || len == 0) || (len == 0 || len == 1)) || (len == 0 || len
        == 1)) || (len == 0 || len == 1)) || (len == 0 || len == 1)) || (len == 0
        || len == 1)) || (len == 0 || len == 1)) || (len == 0 || len == 1)) || len
        == 0) || (len == 0 || len == 1)) || (len == 0 || len == 1)) || len == 0) ||
        (len == 0 || len == 1)) || len == 0) || (len == 0 || len == 1)) || (len ==
        0 || len == 1)) || len == 0) || (len == 0 || len == 1)) || len == 0) || len
        == 0) || len == 0) || (len == 0 || len == 1)) || (len == 0 || len == 1)) ||
        (len == 0 || len == 1)) || (len == 0 || len == 1)) || len == 0) || (len ==
        0 || len == 1)) || len == 0) || (len == 0 || len == 1)) || (len == 0 || len
        == 1)) || (len == 0 || len == 1)) || len == 0) || (len == 0 || len == 1))
        || len == 0) || (len == 0 || len == 1)) || ((((((((((((((((((((((((((((((((((((((((((((((((len
        == 2 || (len == 1 || len == 2)) || len == 2) || len == 2) || (len == 1 ||
        len == 2)) || (len == 1 || len == 2)) || len == 2) || (len == 1 || len ==
        2)) || len == 2) || len == 2) || len == 2) || len == 2) || len == 2) || len
        == 2) || (len == 1 || len == 2)) || len == 2) || (len == 1 || len == 2)) ||
        len == 2) || len == 2) || len == 2) || (len == 1 || len == 2)) || len == 2)
        || len == 2) || (len == 1 || len == 2)) || len == 2) || (len == 1 || len ==
        2)) || ((len == 0 || len == 1) || len == 2)) || len == 2) || len == 2) ||
        (len == 1 || len == 2)) || len == 2) || (len == 1 || len == 2)) || ((len ==
        0 || len == 1) || len == 2)) || len == 2) || len == 2) || len == 2) || (len
        == 1 || len == 2)) || len == 2) || (len == 1 || len == 2)) || len == 2) ||
        (len == 1 || len == 2)) || len == 2) || (len == 1 || len == 2)) || ((len ==
        0 || len == 1) || len == 2)) || ((len == 0 || len == 1) || len == 2)) || len
        == 2) || (len == 1 || len == 2)) || ((len == 0 || len == 1) || len == 2))
        || ((len == 0 || len == 1) || len == 2))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((len
        == 3 || (len == 2 || len == 3)) || len == 3) || len == 3) || len == 3) ||
        len == 3) || (len == 2 || len == 3)) || (len == 2 || len == 3)) || (len ==
        2 || len == 3)) || (len == 2 || len == 3)) || len == 3) || len == 3) || (len
        == 2 || len == 3)) || (len == 2 || len == 3)) || len == 3) || len == 3) ||
        len == 3) || len == 3) || len == 3) || len == 3) || (len == 2 || len == 3))
        || len == 3) || (len == 2 || len == 3)) || len == 3) || len == 3) || len ==
        3) || (len == 2 || len == 3)) || len == 3) || len == 3) || len == 3) || len
        == 3) || (len == 2 || len == 3)) || (len == 2 || len == 3)) || len == 3) ||
        len == 3) || (len == 2 || len == 3)) || (len == 2 || len == 3)) || ((len ==
        1 || len == 2) || len == 3)) || ((len == 1 || len == 2) || len == 3)) || len
        == 3) || len == 3) || (len == 2 || len == 3)) || len == 3) || (len == 2 ||
        len == 3)) || ((len == 1 || len == 2) || len == 3)) || len == 3) || len ==
        3) || len == 3) || (len == 2 || len == 3)) || len == 3) || (len == 2 || len
        == 3)) || len == 3) || (len == 2 || len == 3)) || len == 3) || (len == 2 ||
        len == 3)) || ((len == 1 || len == 2) || len == 3)) || ((len == 1 || len ==
        2) || len == 3)) || len == 3) || (len == 2 || len == 3)) || ((len == 1 ||
        len == 2) || len == 3)) || ((len == 1 || len == 2) || len == 3))) || ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((len
        == 4 || (len == 3 || len == 4)) || len == 4) || len == 4) || (len == 3 ||
        len == 4)) || (len == 3 || len == 4)) || len == 4) || (len == 3 || len ==
        4)) || len == 4) || len == 4) || len == 4) || len == 4) || len == 4) || len
        == 4) || len == 4) || len == 4) || len == 4) || len == 4) || (len == 3 ||
        len == 4)) || (len == 3 || len == 4)) || len == 4) || (len == 3 || len ==
        4)) || len == 4) || len == 4) || len == 4) || len == 4) || len == 4) || len
        == 4) || (len == 3 || len == 4)) || len == 4) || (len == 3 || len == 4)) ||
        len == 4) || len == 4) || len == 4) || (len == 3 || len == 4)) || len == 4)
        || len == 4) || (len == 3 || len == 4)) || len == 4) || (len == 3 || len ==
        4)) || ((len == 2 || len == 3) || len == 4)) || len == 4) || len == 4) ||
        (len == 3 || len == 4)) || len == 4) || (len == 3 || len == 4)) || ((len ==
        2 || len == 3) || len == 4)) || len == 4) || len == 4) || (len == 3 || len
        == 4)) || len == 4) || (len == 3 || len == 4)) || ((len == 2 || len == 3)
        || len == 4)) || len == 4) || len == 4) || len == 4) || (len == 3 || len ==
        4)) || len == 4) || (len == 3 || len == 4)) || len == 4) || (len == 3 || len
        == 4)) || len == 4) || (len == 3 || len == 4)) || ((len == 2 || len == 3)
        || len == 4)) || ((len == 2 || len == 3) || len == 4)) || len == 4) || (len
        == 3 || len == 4)) || ((len == 2 || len == 3) || len == 4)) || ((len == 2
        || len == 3) || len == 4)))) || ((0 == head && head == 0) && ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((len
        == 5 || (len == 4 || len == 5)) || len == 5) || len == 5) || (len == 4 ||
        len == 5)) || (len == 4 || len == 5)) || len == 5) || (len == 4 || len ==
        5)) || len == 5) || len == 5) || len == 5) || len == 5) || len == 5) || len
        == 5) || len == 5) || len == 5) || len == 5) || len == 5) || (len == 4 ||
        len == 5)) || (len == 4 || len == 5)) || len == 5) || (len == 4 || len ==
        5)) || len == 5) || len == 5) || len == 5) || len == 5) || len == 5) || len
        == 5) || len == 5) || len == 5) || (len == 4 || len == 5)) || len == 5) ||
        (len == 4 || len == 5)) || len == 5) || (len == 4 || len == 5)) || len ==
        5) || len == 5) || (len == 4 || len == 5)) || len == 5) || (len == 4 || len
        == 5)) || ((len == 3 || len == 4) || len == 5)) || len == 5) || len == 5)
        || (len == 4 || len == 5)) || len == 5) || (len == 4 || len == 5)) || ((len
        == 3 || len == 4) || len == 5)) || len == 5) || len == 5) || len == 5) ||
        len == 5) || (len == 4 || len == 5)) || len == 5) || (len == 4 || len == 5))
        || len == 5) || (len == 4 || len == 5)) || len == 5) || (len == 4 || len ==
        5)) || ((len == 3 || len == 4) || len == 5)) || ((len == 3 || len == 4) ||
        len == 5)) || len == 5) || (len == 4 || len == 5)) || len == 5) || (len ==
        4 || len == 5)) || ((len == 3 || len == 4) || len == 5)) || len == 5) || (len
        == 4 || len == 5)) || ((len == 3 || len == 4) || len == 5)) || ((len == 3
        || len == 4) || len == 5)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 610
        column: 5
        function: sll_append
      value: ((((((((((((((((sublist_length == 5 || sublist_length == 4) || sublist_length
        == 5) || sublist_length == 5) || sublist_length == 4) || sublist_length ==
        4) || sublist_length == 5) || sublist_length == 4) || sublist_length == 5)
        || sublist_length == 5) || sublist_length == 4) || sublist_length == 5) ||
        sublist_length == 4) || (3 == sublist_length && sublist_length == 3)) || ((((((((((((((((((((((((((((((((((sublist_length
        == 5 || sublist_length == 4) || sublist_length == 5) || sublist_length ==
        5) || sublist_length == 4) || sublist_length == 4) || sublist_length == 5)
        || sublist_length == 4) || sublist_length == 5) || sublist_length == 5) ||
        sublist_length == 5) || sublist_length == 5) || sublist_length == 5) || sublist_length
        == 5) || sublist_length == 5) || sublist_length == 5) || sublist_length ==
        5) || sublist_length == 5) || sublist_length == 5) || sublist_length == 4)
        || sublist_length == 4) || sublist_length == 5) || sublist_length == 4) ||
        sublist_length == 5) || sublist_length == 5) || sublist_length == 4) || sublist_length
        == 5) || sublist_length == 4) || (3 == sublist_length && sublist_length ==
        3)) || sublist_length == 5) || sublist_length == 5) || sublist_length == 4)
        || sublist_length == 5) || sublist_length == 4) || (3 == sublist_length &&
        sublist_length == 3))) || (((((((((((((((((((((((((((((((((((((((((((((((((sublist_length
        == 5 || sublist_length == 4) || sublist_length == 5) || sublist_length ==
        5) || sublist_length == 4) || sublist_length == 4) || sublist_length == 5)
        || sublist_length == 4) || sublist_length == 5) || sublist_length == 5) ||
        sublist_length == 5) || sublist_length == 5) || sublist_length == 5) || sublist_length
        == 5) || sublist_length == 5) || sublist_length == 5) || sublist_length ==
        5) || sublist_length == 5) || sublist_length == 5) || sublist_length == 4)
        || sublist_length == 4) || sublist_length == 5) || sublist_length == 4) ||
        sublist_length == 5) || sublist_length == 5) || sublist_length == 5) || sublist_length
        == 5) || sublist_length == 5) || sublist_length == 5) || sublist_length ==
        4) || sublist_length == 5) || sublist_length == 4) || sublist_length == 5)
        || sublist_length == 5) || sublist_length == 4) || sublist_length == 5) ||
        sublist_length == 4) || (3 == sublist_length && sublist_length == 3)) || sublist_length
        == 5) || sublist_length == 5) || sublist_length == 4) || sublist_length ==
        5) || sublist_length == 4) || (3 == sublist_length && sublist_length == 3))
        || sublist_length == 5) || sublist_length == 5) || sublist_length == 4) ||
        sublist_length == 5) || sublist_length == 4) || (3 == sublist_length && sublist_length
        == 3))) || (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((sublist_length
        == 5 || sublist_length == 4) || sublist_length == 5) || sublist_length ==
        5) || sublist_length == 4) || sublist_length == 4) || sublist_length == 5)
        || sublist_length == 4) || sublist_length == 5) || sublist_length == 5) ||
        sublist_length == 5) || sublist_length == 5) || sublist_length == 5) || sublist_length
        == 5) || sublist_length == 5) || sublist_length == 5) || sublist_length ==
        5) || sublist_length == 5) || sublist_length == 5) || sublist_length == 4)
        || sublist_length == 4) || sublist_length == 5) || sublist_length == 4) ||
        sublist_length == 5) || sublist_length == 5) || sublist_length == 5) || sublist_length
        == 5) || sublist_length == 5) || sublist_length == 5) || sublist_length ==
        5) || sublist_length == 5) || sublist_length == 4) || sublist_length == 5)
        || sublist_length == 4) || sublist_length == 5) || sublist_length == 4) ||
        sublist_length == 5) || sublist_length == 5) || sublist_length == 4) || sublist_length
        == 5) || sublist_length == 4) || (3 == sublist_length && sublist_length ==
        3)) || sublist_length == 5) || sublist_length == 5) || sublist_length == 4)
        || sublist_length == 5) || sublist_length == 4) || (3 == sublist_length &&
        sublist_length == 3)) || sublist_length == 5) || sublist_length == 5) || sublist_length
        == 5) || sublist_length == 4) || sublist_length == 5) || sublist_length ==
        4) || sublist_length == 5) || sublist_length == 4) || sublist_length == 5)
        || sublist_length == 4) || (3 == sublist_length && sublist_length == 3)) ||
        (3 == sublist_length && sublist_length == 3))) || (temp == *head && (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((sublist_length
        == 5 || sublist_length == 4) || sublist_length == 5) || sublist_length ==
        5) || sublist_length == 4) || sublist_length == 4) || sublist_length == 5)
        || sublist_length == 4) || sublist_length == 5) || sublist_length == 5) ||
        sublist_length == 5) || sublist_length == 5) || sublist_length == 5) || sublist_length
        == 5) || sublist_length == 5) || sublist_length == 5) || sublist_length ==
        5) || sublist_length == 5) || sublist_length == 5) || sublist_length == 4)
        || sublist_length == 4) || sublist_length == 5) || sublist_length == 4) ||
        sublist_length == 5) || sublist_length == 5) || sublist_length == 5) || sublist_length
        == 5) || sublist_length == 5) || sublist_length == 5) || sublist_length ==
        5) || sublist_length == 5) || sublist_length == 4) || sublist_length == 5)
        || sublist_length == 4) || sublist_length == 5) || sublist_length == 4) ||
        sublist_length == 5) || sublist_length == 5) || sublist_length == 4) || sublist_length
        == 5) || sublist_length == 4) || (3 == sublist_length && sublist_length ==
        3)) || sublist_length == 5) || sublist_length == 5) || sublist_length == 4)
        || sublist_length == 5) || sublist_length == 4) || (3 == sublist_length &&
        sublist_length == 3)) || sublist_length == 5) || sublist_length == 5) || sublist_length
        == 5) || sublist_length == 5) || sublist_length == 4) || sublist_length ==
        5) || sublist_length == 4) || sublist_length == 5) || sublist_length == 4)
        || sublist_length == 5) || sublist_length == 4) || (3 == sublist_length &&
        sublist_length == 3)) || (3 == sublist_length && sublist_length == 3)) ||
        sublist_length == 5) || sublist_length == 4) || sublist_length == 5) || sublist_length
        == 4) || (3 == sublist_length && sublist_length == 3)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 636
        column: 3
        function: main
      value: 3 == min
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 636
        column: 3
        function: main
      value: 5 == max
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 636
        column: 3
        function: main
      value: (int )min == 3
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 636
        column: 3
        function: main
      value: (int )max == 5
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-ext3-properties/sll_of_sll_nondet_append-1.i
        line: 636
        column: 3
        function: main
      value: ((((((0 == head && 3 == i) && min == i) && i == 3) && head == 0) || (i
        == 6 && (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        == j && 0 == head) && j == 0) && j == head) && head == 0) || ((((j == 6 ||
        j == 7) || j == 8) || j == 9) || j == 10)) || j == 5) || j == 5) || j == 4)
        || j == 3) || j == 2) || j == 4) || j == 4) || j == 3) || j == 3) || j ==
        2) || j == 2) || j == 3) || j == 2) || j == 1) || (0 == j && j == 0)) || j
        == 1) || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) || j == 1)
        || (0 == j && j == 0)) || j == 5) || j == 4) || j == 4) || j == 3) || j ==
        3) || j == 2) || j == 2) || j == 3) || j == 2) || j == 1) || j == 1) || (0
        == j && j == 0)) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0))
        || j == 4) || j == 3) || j == 2) || j == 3) || j == 2) || j == 3) || j ==
        2) || j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) ||
        j == 1) || (0 == j && j == 0)) || j == 2) || j == 1) || (0 == j && j == 0))
        || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) || j == 2) || j ==
        1) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) || (0 == j &&
        j == 0)) || j == 2) || j == 2) || j == 2) || j == 1) || (0 == j && j == 0))
        || j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) || j ==
        1) || (0 == j && j == 0)) || (0 == j && j == 0)) || (0 == j && j == 0)) ||
        j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)) || (0 ==
        j && j == 0)) || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)))) ||
        (i == 5 && (((((((((((((((((((((((((((((((0 == j && 0 == head) && j == 0)
        && j == head) && head == 0) || ((((j == 6 || j == 7) || j == 8) || j == 9)
        || j == 10)) || j == 5) || j == 4) || j == 3) || j == 5) || j == 4) || j ==
        3) || j == 4) || j == 3) || j == 3) || j == 2) || j == 1) || (0 == j && j
        == 0)) || j == 2) || j == 1) || (0 == j && j == 0)) || j == 2) || j == 2)
        || j == 1) || j == 1) || (0 == j && j == 0)) || (0 == j && j == 0)) || j ==
        2) || j == 1) || (0 == j && j == 0)) || j == 1) || (0 == j && j == 0)))) ||
        (i == 4 && ((((((((((0 == j && 0 == head) && j == 0) && j == head) && head
        == 0) || ((((j == 6 || j == 7) || j == 8) || j == 9) || j == 10)) || j ==
        5) || j == 4) || j == 3) || j == 2) || j == 1))
      format: c_expression
