- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 8bef6f70-cf58-4df5-9c37-4828296d09e5
    creation_time: 2025-03-21T01:24:55Z
    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-properties/splice-2.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-properties/splice-2.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-properties/splice-2.i: 098fc4cb5d15cb305e8d98bf2e1c69b111d102681b51dec68ae720515d6f30bc
      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-properties/splice-2.i
        line: 574
        column: 3
        function: main
      value: ((((flag == 0 || flag == 1) || (((flag == 0 || flag == 1) || (((1 ==
        flag && flag == 1) && t == l2) && p == 0)) || (((0 == flag && flag == 0) &&
        t == l1) && p == 0))) || (((((flag == 0 || flag == 1) || ((1 == flag && flag
        == 1) && t == l2)) || ((0 == flag && flag == 0) && t == l1)) || ((((1 == flag
        && flag == 1) && a == l1) && t == l2) && p == 0)) || ((((((((0 == flag &&
        0 == l2) && flag == 0) && flag == l2) && a == t) && a == l1) && t == l1) &&
        l2 == 0) && p == 0))) || (l1 == p && (((((flag == 0 || flag == 1) || ((1 ==
        flag && flag == 1) && t == l2)) || (((0 == flag && flag == 0) && t == l1)
        && t == p)) || ((((1 == flag && flag == 1) && a == l1) && a == p) && t ==
        l2)) || (((((((((0 == flag && 0 == l2) && flag == 0) && flag == l2) && a ==
        t) && a == l1) && a == p) && t == l1) && t == p) && l2 == 0)))) || (flag ==
        0 || flag == 1)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-properties/splice-2.i
        line: 541
        column: 3
        function: main
      value: ((((((((((flag == 0 || flag == 1) || (0 == flag && flag == 0)) || (0
        == flag && flag == 0)) || (1 == flag && flag == 1)) || (1 == flag && flag
        == 1)) || (0 == flag && flag == 0)) || (1 == flag && flag == 1)) || (0 ==
        flag && flag == 0)) || (1 == flag && flag == 1)) || (0 == flag && flag ==
        0)) || ((1 == flag && flag == 1) && a == p)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-properties/splice-2.i
        line: 560
        column: 3
        function: main
      value: (((((flag == 0 || flag == 1) || ((1 == flag && flag == 1) && t == l2))
        || ((0 == flag && flag == 0) && t == l1)) || (((1 == flag && flag == 1) &&
        a == l1) && t == l2)) || (((((((0 == flag && 0 == l2) && flag == 0) && flag
        == l2) && a == t) && a == l1) && t == l1) && l2 == 0)) || (((((((0 == l1 &&
        0 == l2) && 1 == flag) && flag == 1) && a == p) && l1 == 0) && l1 == l2) &&
        l2 == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/list-properties/splice-2.i
        line: 579
        column: 3
        function: main
      value: (((flag == 0 || flag == 1) || ((flag == 0 || flag == 1) || (((1 == flag
        && flag == 1) && t == l2) && p == 0))) || ((((flag == 0 || flag == 1) || ((1
        == flag && flag == 1) && t == l2)) || (((0 == flag && flag == 0) && t == l1)
        && p == 0)) || ((((1 == flag && flag == 1) && a == l1) && t == l2) && p ==
        0))) || (l2 == p && (((((flag == 0 || flag == 1) || (((1 == flag && flag ==
        1) && t == l2) && t == p)) || ((0 == flag && flag == 0) && t == l1)) || ((((1
        == flag && flag == 1) && a == l1) && t == l2) && t == p)) || ((((((((((0 ==
        flag && 0 == l2) && 0 == p) && flag == 0) && flag == l2) && flag == p) &&
        a == t) && a == l1) && t == l1) && l2 == 0) && p == 0)))
      format: c_expression
