- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f4a4bd89-c302-4065-a396-7dd9f6b6d52d
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: d26189af-e53d-47d0-b10a-705ec91744a1
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 76e36119-a18a-4d5f-9356-a377e3d1cfb3
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: ad2b901c-c99e-4e26-aaef-5437026350da
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 68a379d7-ea58-43c2-8cd6-b46b5cdd1b62
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: ec243bf0-90f6-4a88-8980-c621396b4000
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 38e3a52b-20cb-41ea-9deb-933b76715176
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 6816f400-d7e7-4b6c-a7a3-0bb0eacdf74a
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 297f7aeb-9711-4647-8dba-8dd8dd0de3b2
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 78ad6082-958f-4188-aaba-1e41e9b41c06
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 3cbe29b3-309e-438c-be8f-93e2148bc3e6
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 04070975-e83d-4764-8e27-7463777de766
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 016269e4-c8e3-47f3-b32a-3b49b5ab8717
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: be597577-b77e-4256-8f2d-8bd986dd7a9e
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: b4764244-4819-4d1e-a087-666abcf032b8
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 5356da56-98b9-4246-ae6c-44f816fc434b
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 1b2bf421-4f20-433f-9db1-64c9c8fe3315
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: f3c9032f-27d4-4e59-84d4-d18f9de5a5ed
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 617d941e-3951-4763-be6c-efaf15092d00
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: b5969eae-f186-43b8-a071-0c300b99c439
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: f94be846-0cd2-48e1-8702-3870701b89c2
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 5276f20d-8778-46e9-a127-4d2c81cfb8fd
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 55520981-1332-4684-b176-94a328e2b12f
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 3777d4e2-92e7-4f19-a252-0fb2897d2eb5
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 554706df-3413-476f-9666-dc3af3cc17b4
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: e476a0ff-deb7-4cbc-b378-ed282efd6ec3
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 16901840-e4a1-4697-9778-16c91934bfbb
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 95ed9d82-c512-453e-b338-ddbbf04b5196
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: b7c75d8d-79dd-44dc-9be7-031c147a6216
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 14ad3354-b025-405e-aeff-d6c26718e089
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: d84ba8fc-388d-4587-b7a6-1fa971750d2d
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: f7ff7836-8372-47e1-a3e1-ef2fe908bff0
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: c839541c-1791-4739-b70c-efcef9e57517
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 150e251f-01d0-421e-a63c-a7f460bf7520
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 7c0d0fac-5a45-4095-96cb-ec7c71815ac9
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: be5d79e8-e146-42b8-9716-0295f2a3d11b
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: c3007cc9-2a60-4ca1-99b1-7aa9d41c2235
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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: 1bbd2342-e41a-4bd2-8efb-88befb23dea4
    creation_time: 2023-02-02T14:24:01Z
    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''
        ''mine'' ''--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
