- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: e85663f8-b252-4e45-a294-f712b1aa5de6
    creation_time: 2025-03-21T20:09:04Z
    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/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i: 4fa8f711706c6827dfd46bfbbe473b8c8a578e07b4d272918901355226a20b94
      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/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: 0 == v4op[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: 1 == v4op[1]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: 2 == v4op[2]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: 6 == v4op[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: 7 == v4op[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: 8 == v4op[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: 9 == v4op[3]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: 10 == v4op[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: 11 == v4op[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: 15 == v4op[9]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: 16 == v4op[10]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: 17 == v4op[11]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: LDV_IN_INTERRUPT == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (ioport_resource.end & 0ULL) == 0ULL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (ioport_resource.flags & 0UL) == 0UL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (ioport_resource.start & 0ULL) == 0ULL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.core_num_syms & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.core_ro_size & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.core_size & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.core_text_size & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.init_ro_size & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.init_size & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.init_text_size & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.mkobj.kobj.state_add_uevent_sent & (unsigned char)0) ==
        (unsigned char)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.mkobj.kobj.state_in_sysfs & (unsigned char)0) == (unsigned
        char)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.mkobj.kobj.state_initialized & (unsigned char)0) == (unsigned
        char)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.mkobj.kobj.state_remove_uevent_sent & (unsigned char)0)
        == (unsigned char)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.mkobj.kobj.uevent_suppress & (unsigned char)0) == (unsigned
        char)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.num_bugs & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.num_ctors & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.num_exentries & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.num_gpl_future_syms & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.num_gpl_syms & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.num_kp & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.num_syms & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.num_symtab & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.num_trace_bprintk_fmt & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.num_trace_events & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.num_tracepoints & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.num_unused_gpl_syms & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.num_unused_syms & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.percpu_size & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (__this_module.taints & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ ioport_resource.end & 0ULL) == 0ULL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ ioport_resource.flags & 0UL) == 0UL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ ioport_resource.start & 0ULL) == 0ULL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.core_num_syms & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.core_ro_size & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.core_size & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.core_text_size & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.init_ro_size & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.init_size & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.init_text_size & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.mkobj.kobj.state_add_uevent_sent & (unsigned char)0)
        == (unsigned char)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.mkobj.kobj.state_in_sysfs & (unsigned char)0) == (unsigned
        char)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.mkobj.kobj.state_initialized & (unsigned char)0) ==
        (unsigned char)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.mkobj.kobj.state_remove_uevent_sent & (unsigned char)0)
        == (unsigned char)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.mkobj.kobj.uevent_suppress & (unsigned char)0) == (unsigned
        char)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.num_bugs & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.num_ctors & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.num_exentries & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.num_gpl_future_syms & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.num_gpl_syms & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.num_kp & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.num_syms & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.num_symtab & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.num_trace_bprintk_fmt & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.num_trace_events & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.num_tracepoints & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.num_unused_gpl_syms & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.num_unused_syms & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.percpu_size & 0U) == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.i
        line: 2645
        column: 3
        function: enter_4op_mode
      value: (~ __this_module.taints & 0U) == 0U
      format: c_expression
