- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 54258743-762c-45c0-959e-93a3b4c87f7b
    creation_time: 2025-03-22T04:57:40Z
    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'' ''64bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i: 8e036d03abaa2464843bef35227938cb8e4d04c5a12ab6a4a0003d6a8df9a501
      data_model: LP64
      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/busybox-1.22.0/chgrp-incomplete-1.i
        line: 2363
        column: 3
        function: full_write
      value: 2 == fd
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i
        line: 2363
        column: 3
        function: full_write
      value: fd == 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i
        line: 2363
        column: 3
        function: full_write
      value: (0L <= cc && 0L <= total) || (0L == total && total == 0L)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i
        line: 2503
        column: 3
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i
        line: 2503
        column: 3
        function: main
      value: (((((j == 10 && i == 1) && ((((((((((10 <= argc && 10 <= i) || (argc
        == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 7 && i == 7)) || (argc
        == 6 && i == 6)) || (argc == 5 && i == 5)) || (argc == 3 && i == 3)) || (argc
        == 4 && i == 4)) || (argc == 2 && i == 2)) || (argc == 1 && i == 1))) || ((0
        == i && i == 0) && ((j == 10 && ((((((((((10 <= argc && 10 <= i) || (argc
        == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 7 && i == 7)) || (argc
        == 6 && i == 6)) || (argc == 5 && i == 5)) || (argc == 3 && i == 3)) || (argc
        == 4 && i == 4)) || (argc == 2 && i == 2)) || (argc == 1 && i == 1))) || (((argc
        <= 0 && 0 == i) && i == 0) && i == i)))) || (j == 10 && ((4 <= i && ((((((10
        <= argc && 10 <= i) || ((i <= 9 && argc == 9) && i == 9)) || ((i <= 8 && argc
        == 8) && i == 8)) || ((i <= 7 && argc == 7) && i == 7)) || ((i <= 6 && argc
        == 6) && i == 6)) || ((i <= 5 && argc == 5) && i == 5))) || ((argc == 4 &&
        i == 4) && i == 4)))) || ((j == 10 && i == 3) && ((((((((10 <= argc && 10
        <= i) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) || (argc == 7 &&
        i == 7)) || (argc == 6 && i == 6)) || (argc == 5 && i == 5)) || (argc == 3
        && i == 3)) || (argc == 4 && i == 4)))) || ((j == 10 && i == 2) && (((((((((10
        <= argc && 10 <= i) || (argc == 9 && i == 9)) || (argc == 8 && i == 8)) ||
        (argc == 7 && i == 7)) || (argc == 6 && i == 6)) || (argc == 5 && i == 5))
        || (argc == 3 && i == 3)) || (argc == 4 && i == 4)) || (argc == 2 && i ==
        2)))
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i
        line: 2499
        column: 5
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i
        line: 2499
        column: 5
        function: main
      value: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((3 <= argc &&
        0 == j) && i == 2) && j == 0) || ((2 <= argc && i == 1) && j == 10)) || (j
        == 10 && (((((((9 <= i && 10 <= argc) && i <= 2147483646) || (9 <= argc &&
        i == 8)) || (8 <= argc && i == 7)) || (7 <= argc && i == 6)) || (6 <= argc
        && i == 5)) || (5 <= argc && i == 4)))) || ((2 <= argc && i == 1) && j ==
        9)) || ((2 <= argc && i == 1) && j == 8)) || (j == 9 && (((((((9 <= i && 10
        <= argc) && i <= 2147483646) || (9 <= argc && i == 8)) || (8 <= argc && i
        == 7)) || (7 <= argc && i == 6)) || (6 <= argc && i == 5)) || (5 <= argc &&
        i == 4)))) || ((2 <= argc && i == 1) && j == 7)) || (j == 8 && (((((((9 <=
        i && 10 <= argc) && i <= 2147483646) || (9 <= argc && i == 8)) || (8 <= argc
        && i == 7)) || (7 <= argc && i == 6)) || (6 <= argc && i == 5)) || (5 <= argc
        && i == 4)))) || ((2 <= argc && i == 1) && j == 6)) || (j == 7 && (((((((9
        <= i && 10 <= argc) && i <= 2147483646) || (9 <= argc && i == 8)) || (8 <=
        argc && i == 7)) || (7 <= argc && i == 6)) || (6 <= argc && i == 5)) || (5
        <= argc && i == 4)))) || ((2 <= argc && i == 1) && j == 5)) || (j == 6 &&
        (((((((9 <= i && 10 <= argc) && i <= 2147483646) || (9 <= argc && i == 8))
        || (8 <= argc && i == 7)) || (7 <= argc && i == 6)) || (6 <= argc && i ==
        5)) || (5 <= argc && i == 4)))) || ((2 <= argc && i == 1) && j == 4)) || (j
        == 5 && (((((((9 <= i && 10 <= argc) && i <= 2147483646) || (9 <= argc &&
        i == 8)) || (8 <= argc && i == 7)) || (7 <= argc && i == 6)) || (6 <= argc
        && i == 5)) || (5 <= argc && i == 4)))) || ((2 <= argc && i == 1) && j ==
        3)) || (j == 4 && (((((((9 <= i && 10 <= argc) && i <= 2147483646) || (9 <=
        argc && i == 8)) || (8 <= argc && i == 7)) || (7 <= argc && i == 6)) || (6
        <= argc && i == 5)) || (5 <= argc && i == 4)))) || ((2 <= argc && i == 1)
        && j == 2)) || (j == 3 && (((((((9 <= i && 10 <= argc) && i <= 2147483646)
        || (9 <= argc && i == 8)) || (8 <= argc && i == 7)) || (7 <= argc && i ==
        6)) || (6 <= argc && i == 5)) || (5 <= argc && i == 4)))) || ((2 <= argc &&
        i == 1) && j == 1)) || (j == 2 && (((((((9 <= i && 10 <= argc) && i <= 2147483646)
        || (9 <= argc && i == 8)) || (8 <= argc && i == 7)) || (7 <= argc && i ==
        6)) || (6 <= argc && i == 5)) || (5 <= argc && i == 4)))) || (((2 <= argc
        && 0 == j) && i == 1) && j == 0)) || (j == 1 && (((((((9 <= i && 10 <= argc)
        && i <= 2147483646) || (9 <= argc && i == 8)) || (8 <= argc && i == 7)) ||
        (7 <= argc && i == 6)) || (6 <= argc && i == 5)) || (5 <= argc && i == 4))))
        || ((0 == j && j == 0) && (((((((9 <= i && 10 <= argc) && i <= 2147483646)
        || (9 <= argc && i == 8)) || (8 <= argc && i == 7)) || (7 <= argc && i ==
        6)) || (6 <= argc && i == 5)) || (5 <= argc && i == 4)))) || ((1 <= argc &&
        i == 0) && j == 10)) || ((1 <= argc && i == 0) && j == 9)) || ((4 <= argc
        && i == 3) && j == 10)) || ((1 <= argc && i == 0) && j == 8)) || ((4 <= argc
        && i == 3) && j == 9)) || ((1 <= argc && i == 0) && j == 7)) || ((4 <= argc
        && i == 3) && j == 8)) || ((1 <= argc && i == 0) && j == 6)) || ((4 <= argc
        && i == 3) && j == 7)) || ((1 <= argc && i == 0) && j == 5)) || ((4 <= argc
        && i == 3) && j == 6)) || ((1 <= argc && i == 0) && j == 4)) || ((4 <= argc
        && i == 3) && j == 5)) || ((1 <= argc && i == 0) && j == 3)) || ((4 <= argc
        && i == 3) && j == 4)) || ((1 <= argc && i == 0) && j == 2)) || ((4 <= argc
        && i == 3) && j == 3)) || ((1 <= argc && i == 0) && j == 1)) || ((4 <= argc
        && i == 3) && j == 2)) || (((1 <= argc && 0 == j) && i == 0) && j == 0)) ||
        ((4 <= argc && i == 3) && j == 1)) || (((4 <= argc && 0 == j) && i == 3) &&
        j == 0)) || ((3 <= argc && i == 2) && j == 10)) || ((3 <= argc && i == 2)
        && j == 9)) || ((3 <= argc && i == 2) && j == 8)) || ((3 <= argc && i == 2)
        && j == 7)) || ((3 <= argc && i == 2) && j == 6)) || ((3 <= argc && i == 2)
        && j == 5)) || ((3 <= argc && i == 2) && j == 4)) || ((3 <= argc && i == 2)
        && j == 3)) || ((3 <= argc && i == 2) && j == 2)) || ((3 <= argc && i == 2)
        && j == 1)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i
        line: 2484
        column: 3
        function: main
      value: (((((((((i == 1 || (0 == i && i == 0)) || i == 10) || i == 9) || i ==
        8) || i == 7) || i == 6) || i == 5) || i == 4) || i == 3) || i == 2
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i
        line: 2337
        column: 3
        function: __main
      value: (((((((((10 <= argc || argc == 9) || argc == 8) || argc == 7) || argc
        == 6) || argc == 5) || argc == 3) || argc == 4) || argc == 2) || argc == 1)
        || argc <= 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i
        line: 2494
        column: 3
        function: main
      value: i == 10
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i
        line: 2494
        column: 3
        function: main
      value: ((j == 10 && (((2 <= argc && i == 2) || (1 <= argc && i == 1)) || (((((((10
        <= argc && 10 <= i) || (9 <= argc && i == 9)) || (8 <= argc && i == 8)) ||
        (7 <= argc && i == 7)) || (6 <= argc && i == 6)) || (5 <= argc && i == 5))
        || (4 <= argc && i == 4)))) || (0 == i && i == 0)) || ((3 <= argc && i ==
        3) && j == 10)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i
        line: 2381
        column: 3
        function: safe_write
      value: 1UL <= count
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i
        line: 2381
        column: 3
        function: safe_write
      value: 2 == fd
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete-1.i
        line: 2381
        column: 3
        function: safe_write
      value: fd == 2
      format: c_expression
