- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ed089e4e-6668-47ff-a110-d72146254bf6
    creation_time: 2024-04-26T10:45:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 7630
    column: 3
    function: ldv_dispatch_insmod_register_10_3
  location_invariant:
    string: '! multithreaded || (smutex_lock_of_w83977af_ir_locked || ((((((((x86_dma_fallback_dev.offline
      == (_Bool)0 || x86_dma_fallback_dev.offline == (_Bool)1) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ef724151-c7b5-4a62-b56c-7c979d3b8b75
    creation_time: 2024-04-26T10:45:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 7662
    column: 3
    function: ldv_dispatch_irq_register_8_3
  location_invariant:
    string: '! multithreaded || (smutex_lock_of_w83977af_ir_locked || ((((((((x86_dma_fallback_dev.offline
      == (_Bool)0 || x86_dma_fallback_dev.offline == (_Bool)1) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: daee205c-48c3-4198-b8e7-ef6852d62c21
    creation_time: 2024-04-26T10:45:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 7679
    column: 3
    function: ldv_dispatch_register_7_4
  location_invariant:
    string: '! multithreaded || (smutex_lock_of_w83977af_ir_locked || ((((((((x86_dma_fallback_dev.offline
      == (_Bool)0 || x86_dma_fallback_dev.offline == (_Bool)1) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1)))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be8de2b8-987f-4a84-a513-6f5b4c949fce
    creation_time: 2024-04-26T10:45:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 7630
    column: 3
    function: ldv_dispatch_insmod_register_10_3
  location_invariant:
    string: '! multithreaded || ((((((((x86_dma_fallback_dev.offline == (_Bool)0 ||
      x86_dma_fallback_dev.offline == (_Bool)1) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 932bbada-b1b5-4acb-8d17-81288da4d260
    creation_time: 2024-04-26T10:45:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 7662
    column: 3
    function: ldv_dispatch_irq_register_8_3
  location_invariant:
    string: '! multithreaded || ((((((((x86_dma_fallback_dev.offline == (_Bool)0 ||
      x86_dma_fallback_dev.offline == (_Bool)1) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a9756ca5-9b70-4ee7-a53b-bb57ba4e67e0
    creation_time: 2024-04-26T10:45:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 7679
    column: 3
    function: ldv_dispatch_register_7_4
  location_invariant:
    string: '! multithreaded || ((((((((x86_dma_fallback_dev.offline == (_Bool)0 ||
      x86_dma_fallback_dev.offline == (_Bool)1) && (x86_dma_fallback_dev.offline_disabled
      == (_Bool)0 || x86_dma_fallback_dev.offline_disabled == (_Bool)1)) && (x86_dma_fallback_dev.power.early_init
      == (_Bool)0 || x86_dma_fallback_dev.power.early_init == (_Bool)1)) && (x86_dma_fallback_dev.power.ignore_children
      == (_Bool)0 || x86_dma_fallback_dev.power.ignore_children == (_Bool)1)) && (x86_dma_fallback_dev.power.is_prepared
      == (_Bool)0 || x86_dma_fallback_dev.power.is_prepared == (_Bool)1)) && (x86_dma_fallback_dev.power.is_suspended
      == (_Bool)0 || x86_dma_fallback_dev.power.is_suspended == (_Bool)1)) && (x86_dma_fallback_dev.power.syscore
      == (_Bool)0 || x86_dma_fallback_dev.power.syscore == (_Bool)1)) && (x86_dma_fallback_dev.power.wakeup_path
      == (_Bool)0 || x86_dma_fallback_dev.power.wakeup_path == (_Bool)1))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 6a2e7c9b-d5bf-4e74-842a-13d93e7966c5
    creation_time: 2024-04-26T10:45:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: ed2038ae-e02d-4447-9577-889830b1dada
    creation_time: 2024-04-26T10:45:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 7628
    column: 3
    function: ldv_dispatch_insmod_register_10_3
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: e214070a-2bed-4d7a-9e44-c55f4f0d1754
    creation_time: 2024-04-26T10:45:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: smutex_lock_of_w83977af_ir_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: 9d176e79-61a8-49e9-aee6-ffe9c9fb7d2b
    creation_time: 2024-04-26T10:45:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: smutex_lock_of_w83977af_ir_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 9420
    column: 3
    function: ldv_spin_unlock_lock_of_w83977af_ir
- entry_type: ghost_update
  metadata:
    format_version: "0.1"
    uuid: c669ba06-dcd4-4a94-b0ac-471782e0a9b0
    creation_time: 2024-04-26T10:45:46Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g10dfba143-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: smutex_lock_of_w83977af_ir_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.14-races/linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i
    file_hash: dcbacb5c6320cc7d732f3f08957667bdf1dc73f77660278f36230fbc0ccef69c
    line: 9411
    column: 3
    function: ldv_spin_lock_lock_of_w83977af_ir
