- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 61f7d906-8131-4a93-aa92-99486519e65a
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3505
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  location_invariant:
    string: 1U <= max_n_32bit
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d0bdb1e3-a7a9-4b1f-ba49-ded0e7d55af6
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3505
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  location_invariant:
    string: max_n_32bit <= 1073741823U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0e1ef3b1-a643-424d-bdcc-4c6e3e8f50c2
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3505
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  location_invariant:
    string: i <= 4U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 85cf68d2-8c2f-48f3-8767-3a52b82980ee
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3505
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  location_invariant:
    string: count <= 1073741822U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81a4012e-45a8-4d5a-ae8d-4de4283405f4
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3505
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  location_invariant:
    string: max_n_32bit != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4b6f3b51-13c1-4058-976e-bd96fd0aaab8
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3514
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  location_invariant:
    string: max_n_32bit <= 1073741823U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5dd04e40-905d-415f-8473-9a1e8afc5969
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3514
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  location_invariant:
    string: count <= 1073741823U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1454b091-2974-4f80-a181-9c9b55b77ed9
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3537
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  location_invariant:
    string: 1U <= max_n_32bit
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a16ed820-5231-463b-ac88-e9e30a14cada
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3537
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  location_invariant:
    string: count <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48be8252-c1c2-4bec-b36c-b7769a04767d
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3537
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  location_invariant:
    string: max_n_32bit != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5a32ea7d-c87a-4980-8023-af6305a09557
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3596
    column: 8
    function: tegra_slink_read_rx_fifo_to_client_rxbuf
  location_invariant:
    string: 1U <= rx_full_count
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 82eb6b5e-f06c-4ad7-9ba5-5aa9d3d67e58
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3596
    column: 8
    function: tegra_slink_read_rx_fifo_to_client_rxbuf
  location_invariant:
    string: i <= 4U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8776615b-78f8-4242-8cd9-3b285b706380
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3596
    column: 8
    function: tegra_slink_read_rx_fifo_to_client_rxbuf
  location_invariant:
    string: count <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6a87b9bc-faf3-47e4-9cf5-c0e1bf2bf817
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3596
    column: 8
    function: tegra_slink_read_rx_fifo_to_client_rxbuf
  location_invariant:
    string: rx_full_count != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0da93167-fb07-4210-bdba-6b7d401373f9
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3624
    column: 8
    function: tegra_slink_read_rx_fifo_to_client_rxbuf
  location_invariant:
    string: 1U <= rx_full_count
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 627ff268-032b-449f-8a4e-10eb95eb8b8e
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3624
    column: 8
    function: tegra_slink_read_rx_fifo_to_client_rxbuf
  location_invariant:
    string: count <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c9ec61a3-45ab-4cd0-9136-380421ba13be
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3624
    column: 8
    function: tegra_slink_read_rx_fifo_to_client_rxbuf
  location_invariant:
    string: rx_full_count != 0U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e3273bca-7bc9-4bbb-9f63-07ea2f57f33c
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3676
    column: 8
    function: tegra_slink_copy_client_txbuf_to_spi_txbuf
  location_invariant:
    string: count <= 4294967294U
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 8cac8f25-a0d5-4feb-84f9-94c72ef3a434
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3732
    column: 8
    function: tegra_slink_copy_spi_rxbuf_to_client_rxbuf
  location_invariant:
    string: count <= 4294967294U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 10ef7ca5-d9ea-4ce9-9482-dddb00d5a99a
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3505
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  loop_invariant:
    string: 1U <= max_n_32bit
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3bd6b36c-6af4-445c-b568-bf8c5470eabd
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3505
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  loop_invariant:
    string: max_n_32bit <= 1073741823U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ba2bedc3-476d-42e8-b426-da1d54b07ced
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3505
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  loop_invariant:
    string: i <= 4U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a7a021c-ddce-417d-88eb-057c0a0f8279
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3505
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  loop_invariant:
    string: count <= 1073741822U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a234b12d-a033-430e-b855-05eebe7759b0
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3505
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  loop_invariant:
    string: max_n_32bit != 0U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 6cc4563b-a783-4e0f-8c96-96ccb9c0bb46
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3514
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  loop_invariant:
    string: max_n_32bit <= 1073741823U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: a5dd6a76-ea84-45b3-9a93-5664c3f051fa
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3514
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  loop_invariant:
    string: count <= 1073741823U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 271a0fad-d9de-4306-bfb9-045bfeaa1de3
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3537
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  loop_invariant:
    string: 1U <= max_n_32bit
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c4aa9b6f-7198-429b-837e-a5fe47942112
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3537
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  loop_invariant:
    string: count <= 4294967294U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 771513f9-f5cb-4ad0-a040-d66e1b5d6747
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3537
    column: 8
    function: tegra_slink_fill_tx_fifo_from_client_txbuf
  loop_invariant:
    string: max_n_32bit != 0U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 192629d4-d486-4f16-979a-c8d183f8a8f3
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3596
    column: 8
    function: tegra_slink_read_rx_fifo_to_client_rxbuf
  loop_invariant:
    string: 1U <= rx_full_count
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 629f7817-9e41-451e-b32a-61e8966b7654
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3596
    column: 8
    function: tegra_slink_read_rx_fifo_to_client_rxbuf
  loop_invariant:
    string: i <= 4U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: e71cd81b-485f-4abc-ab52-4437e8c64c81
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3596
    column: 8
    function: tegra_slink_read_rx_fifo_to_client_rxbuf
  loop_invariant:
    string: count <= 4294967294U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 0926c501-627c-419f-9800-b9250db5c0eb
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3596
    column: 8
    function: tegra_slink_read_rx_fifo_to_client_rxbuf
  loop_invariant:
    string: rx_full_count != 0U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a5d09e0-876a-4de8-ba5c-9e0d89b48ec1
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3624
    column: 8
    function: tegra_slink_read_rx_fifo_to_client_rxbuf
  loop_invariant:
    string: 1U <= rx_full_count
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: de46b19b-b546-460b-b24b-d1b5ff4dcccb
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3624
    column: 8
    function: tegra_slink_read_rx_fifo_to_client_rxbuf
  loop_invariant:
    string: count <= 4294967294U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: c70b034d-cdac-4add-bc6a-1de453897bca
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3624
    column: 8
    function: tegra_slink_read_rx_fifo_to_client_rxbuf
  loop_invariant:
    string: rx_full_count != 0U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: 57d11bce-89fd-48d5-8f31-9892ed513e91
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3676
    column: 8
    function: tegra_slink_copy_client_txbuf_to_spi_txbuf
  loop_invariant:
    string: count <= 4294967294U
    type: assertion
    format: C
- entry_type: loop_invariant
  metadata:
    format_version: "0.1"
    uuid: ae6eeca3-f6b6-4634-8901-641051ef55cb
    creation_time: 2023-02-02T14:22:48Z
    producer:
      name: Goblint
      version: heads/yaml-witness-unassume-bench-0-g98c2a85b0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/bench-yaml.json'' ''--enable''
        ''dbg.timing.enabled'' ''--enable'' ''witness.invariant.loop-head'' ''--enable''
        ''witness.invariant.after-lock'' ''--disable'' ''witness.invariant.other''
        ''--disable'' ''witness.invariant.accessed'' ''--ana.base.privatization''
        ''protection-read'' ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i'''
    task:
      input_files:
      - /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
      input_file_hashes:
        /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
      data_model: ILP32
      language: C
  location:
    file_name: /mnt/thread-witnesses/replication/bench/svcomp/linux-3.14--drivers--spi--spi-tegra20-slink.ko.cil.i
    file_hash: 8933630f4cde50cf36eb2db51c9e240fc5e0c6bd245d32e47623c1906a97a301
    line: 3732
    column: 8
    function: tegra_slink_copy_spi_rxbuf_to_client_rxbuf
  loop_invariant:
    string: count <= 4294967294U
    type: assertion
    format: C
