- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 8f64f5e4-a768-4c6d-8b0b-103379ad8137
    creation_time: 2025-03-21T19:16:39Z
    producer:
      name: Goblint
      version: heads/master-0-g66dff5a90-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp.json'' ''--disable'' ''witness.graphml.enabled''
        ''--sets'' ''ana.specification'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/valid-memsafety.prp''
        ''--sets'' ''exp.architecture'' ''64bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i: f3090fd14639372da088dcbc149768c93516e312be941c28b3a0b4b80aaee842
      data_model: LP64
      language: C
      specification: 'CHECK( init(main()), LTL(G valid-free) )

        CHECK( init(main()), LTL(G valid-deref) )

        CHECK( init(main()), LTL(G valid-memtrack) )'
  content:
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4179
        column: 3
        function: iowarrior_read
      value: LDV_IN_INTERRUPT == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4179
        column: 3
        function: iowarrior_read
      value: ((((((((((((((((((((((((((((((((((0 <= ldv_urb_state && 0 <= ldv_coherent_state)
        || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0
        && ldv_coherent_state == 0)) || (ldv_coherent_state == 0 && (ldv_urb_state
        == 0 || ldv_urb_state == 1))) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_coherent_state
        == 0 && (ldv_urb_state == 0 || ldv_urb_state == 1))) || (ldv_urb_state ==
        0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state
        == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || 0 <= ldv_coherent_state) || 0 <= ldv_coherent_state)
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || 0 <= ldv_coherent_state)
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (ldv_urb_state == 0
        && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && (ldv_coherent_state == 0 || ldv_coherent_state
        == 1))) || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state
        == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4209
        column: 15
        function: iowarrior_read
      value: 0 == __ret
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4209
        column: 15
        function: iowarrior_read
      value: 0U == __wait.flags
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4209
        column: 15
        function: iowarrior_read
      value: read_idx == -1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4209
        column: 15
        function: iowarrior_read
      value: __ret == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4209
        column: 15
        function: iowarrior_read
      value: __wait.flags == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4209
        column: 15
        function: iowarrior_read
      value: __wait.func == & autoremove_wake_function
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4209
        column: 15
        function: iowarrior_read
      value: __wait.task_list.next == __wait.task_list.prev
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4209
        column: 15
        function: iowarrior_read
      value: __wait.task_list.next == & __wait.task_list
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4209
        column: 15
        function: iowarrior_read
      value: __wait.task_list.prev == & __wait.task_list
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4209
        column: 15
        function: iowarrior_read
      value: LDV_IN_INTERRUPT == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4209
        column: 15
        function: iowarrior_read
      value: ((((((((((((((((((((((((((((((((((0 <= ldv_urb_state && 0 <= ldv_coherent_state)
        || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0
        && ldv_coherent_state == 0)) || (ldv_coherent_state == 0 && (ldv_urb_state
        == 0 || ldv_urb_state == 1))) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_coherent_state
        == 0 && (ldv_urb_state == 0 || ldv_urb_state == 1))) || (ldv_urb_state ==
        0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state
        == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || 0 <= ldv_coherent_state) || 0 <= ldv_coherent_state)
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || 0 <= ldv_coherent_state)
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (ldv_urb_state == 0
        && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && (ldv_coherent_state == 0 || ldv_coherent_state
        == 1))) || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state
        == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: 1UL <= count
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: 0 == retval
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: 0 == buf
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: 0 == int_out_urb
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: 0 == __ret
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: 0U == __wait.flags
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: retval == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: retval == buf
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: retval == int_out_urb
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: retval == __ret
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: buf == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: buf == int_out_urb
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: buf == __ret
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: int_out_urb == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: int_out_urb == __ret
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: __ret == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: __wait.flags == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: __wait.func == & autoremove_wake_function
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: __wait.task_list.next == __wait.task_list.prev
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: __wait.task_list.next == & __wait.task_list
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: __wait.task_list.prev == & __wait.task_list
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: LDV_IN_INTERRUPT == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 4438
        column: 17
        function: iowarrior_write
      value: ((((((((((((((((((((((((((((((((((0 <= ldv_urb_state && 0 <= ldv_coherent_state)
        || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0
        && ldv_coherent_state == 0)) || (ldv_coherent_state == 0 && (ldv_urb_state
        == 0 || ldv_urb_state == 1))) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_coherent_state
        == 0 && (ldv_urb_state == 0 || ldv_urb_state == 1))) || (ldv_urb_state ==
        0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state
        == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || 0 <= ldv_coherent_state) || 0 <= ldv_coherent_state)
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || 0 <= ldv_coherent_state)
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (ldv_urb_state == 0
        && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && (ldv_coherent_state == 0 || ldv_coherent_state
        == 1))) || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state
        == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 5377
        column: 3
        function: main
      value: LDV_IN_INTERRUPT == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 5377
        column: 3
        function: main
      value: (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((0
        == ldv_s_iowarrior_fops_file_operations && 0 == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_fops_file_operations == 0) && ldv_s_iowarrior_fops_file_operations
        == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_driver_usb_driver
        == 0) && ldv_urb_state == 0) && ldv_coherent_state == 0) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((ldv_s_iowarrior_driver_usb_driver
        == 0 && ldv_urb_state == 0) && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((ldv_s_iowarrior_driver_usb_driver
        == 0 && ldv_urb_state == 0) && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((ldv_coherent_state
        == 0 && (ldv_s_iowarrior_driver_usb_driver == 0 || ldv_s_iowarrior_driver_usb_driver
        == 1)) && (ldv_urb_state == 0 || ldv_urb_state == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || ((((0 == ldv_s_iowarrior_fops_file_operations
        && ldv_s_iowarrior_fops_file_operations == 0) && ldv_coherent_state == 0)
        && (ldv_s_iowarrior_driver_usb_driver == 0 || ldv_s_iowarrior_driver_usb_driver
        == 1)) && (ldv_urb_state == 0 || ldv_urb_state == 1))) || (((ldv_s_iowarrior_driver_usb_driver
        == 0 && ldv_urb_state == 0) && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((ldv_s_iowarrior_driver_usb_driver
        == 0 && ldv_urb_state == 0) && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((ldv_coherent_state
        == 0 && (ldv_s_iowarrior_driver_usb_driver == 0 || ldv_s_iowarrior_driver_usb_driver
        == 1)) && (ldv_urb_state == 0 || ldv_urb_state == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((ldv_s_iowarrior_driver_usb_driver
        == 0 && ldv_urb_state == 0) && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || ((((((0 == ldv_s_iowarrior_fops_file_operations
        && 0 == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_fops_file_operations == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0) && ldv_coherent_state
        == 0)) || (((ldv_s_iowarrior_driver_usb_driver == 0 && ldv_urb_state == 0)
        && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations ==
        0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((ldv_s_iowarrior_driver_usb_driver
        == 0 && ldv_urb_state == 0) && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || ((((((0 == ldv_s_iowarrior_fops_file_operations
        && 0 == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_fops_file_operations == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0) && ldv_coherent_state
        == 0)) || (((ldv_s_iowarrior_driver_usb_driver == 0 && ldv_urb_state == 0)
        && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations ==
        0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((ldv_s_iowarrior_driver_usb_driver
        == 0 && ldv_urb_state == 0) && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || ((((((0 == ldv_s_iowarrior_fops_file_operations
        && 0 == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_fops_file_operations == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0) && ldv_coherent_state
        == 0)) || (((0 <= ldv_urb_state && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver
        == 0 || ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || ((0 <= ldv_coherent_state
        && (ldv_s_iowarrior_driver_usb_driver == 0 || ldv_s_iowarrior_driver_usb_driver
        == 1)) && (((ldv_s_iowarrior_fops_file_operations == 0 || ldv_s_iowarrior_fops_file_operations
        == 1) || ldv_s_iowarrior_fops_file_operations == 2) || ldv_s_iowarrior_fops_file_operations
        == 3))) || ((0 <= ldv_coherent_state && (ldv_s_iowarrior_driver_usb_driver
        == 0 || ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || ((0 <= ldv_coherent_state
        && (ldv_s_iowarrior_driver_usb_driver == 0 || ldv_s_iowarrior_driver_usb_driver
        == 1)) && (((ldv_s_iowarrior_fops_file_operations == 0 || ldv_s_iowarrior_fops_file_operations
        == 1) || ldv_s_iowarrior_fops_file_operations == 2) || ldv_s_iowarrior_fops_file_operations
        == 3))) || (((0 <= ldv_urb_state && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver
        == 0 || ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((0 <= ldv_urb_state
        && 0 <= ldv_coherent_state) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1)) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || ((((((0 == ldv_s_iowarrior_fops_file_operations
        && 0 == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_fops_file_operations == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0) && ldv_coherent_state
        == 0)) || (((ldv_s_iowarrior_driver_usb_driver == 0 && ldv_urb_state == 0)
        && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations ==
        0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((ldv_s_iowarrior_driver_usb_driver
        == 0 && ldv_urb_state == 0) && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || (((ldv_s_iowarrior_driver_usb_driver
        == 0 && ldv_urb_state == 0) && (ldv_coherent_state == 0 || ldv_coherent_state
        == 1)) && (((ldv_s_iowarrior_fops_file_operations == 0 || ldv_s_iowarrior_fops_file_operations
        == 1) || ldv_s_iowarrior_fops_file_operations == 2) || ldv_s_iowarrior_fops_file_operations
        == 3))) || (((ldv_s_iowarrior_driver_usb_driver == 0 && ldv_urb_state == 0)
        && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations ==
        0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || ((((((0 == ldv_s_iowarrior_fops_file_operations
        && 0 == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_fops_file_operations == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0) && ldv_coherent_state
        == 0)) || (((ldv_s_iowarrior_driver_usb_driver == 0 && ldv_urb_state == 0)
        && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations ==
        0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || ((((((0 == ldv_s_iowarrior_fops_file_operations
        && 0 == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_fops_file_operations == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0) && ldv_coherent_state
        == 0)) || ((((((0 == ldv_s_iowarrior_fops_file_operations && 0 == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_fops_file_operations == 0) && ldv_s_iowarrior_fops_file_operations
        == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_driver_usb_driver
        == 0) && ldv_urb_state == 0) && ldv_coherent_state == 0)) || ((((((0 == ldv_s_iowarrior_fops_file_operations
        && 0 == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_fops_file_operations == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0) && ldv_coherent_state
        == 0)) || (((ldv_s_iowarrior_driver_usb_driver == 0 && ldv_urb_state == 0)
        && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations ==
        0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || ((((((0 == ldv_s_iowarrior_fops_file_operations
        && 0 == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_fops_file_operations == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0) && ldv_coherent_state
        == 0)) || ((((((0 == ldv_s_iowarrior_fops_file_operations && 0 == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_fops_file_operations == 0) && ldv_s_iowarrior_fops_file_operations
        == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_driver_usb_driver
        == 0) && ldv_urb_state == 0) && ldv_coherent_state == 0)) || (((ldv_s_iowarrior_driver_usb_driver
        == 0 && ldv_urb_state == 0) && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || ((((((0 == ldv_s_iowarrior_fops_file_operations
        && 0 == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_fops_file_operations == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0) && ldv_coherent_state
        == 0)) || ((((((ldv_coherent_state == 0 && ((((((((((((((((0 == ldv_s_iowarrior_fops_file_operations
        && ldv_s_iowarrior_fops_file_operations == 0) && ((((0 == ldv_s_iowarrior_driver_usb_driver
        && ldv_s_iowarrior_fops_file_operations == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0) || (ldv_s_iowarrior_driver_usb_driver
        == 1 && ldv_urb_state == 1))) || (((ldv_s_iowarrior_fops_file_operations ==
        0 || ldv_s_iowarrior_fops_file_operations == 1) && (ldv_s_iowarrior_driver_usb_driver
        == 0 || ldv_s_iowarrior_driver_usb_driver == 1)) && (ldv_urb_state == 0 ||
        ldv_urb_state == 1))) || (((0 <= ldv_urb_state && ldv_urb_state <= 2) && (ldv_s_iowarrior_driver_usb_driver
        == 0 || ldv_s_iowarrior_driver_usb_driver == 1)) && ((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2))) || (((0 == ldv_s_iowarrior_fops_file_operations && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_driver_usb_driver == 1) && ldv_urb_state == 1)) ||
        (((0 <= ldv_urb_state && ldv_urb_state <= 2) && (ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1)) && (ldv_s_iowarrior_driver_usb_driver
        == 0 || ldv_s_iowarrior_driver_usb_driver == 1))) || (((0 == ldv_s_iowarrior_driver_usb_driver
        && ldv_s_iowarrior_fops_file_operations == 1) && ldv_s_iowarrior_driver_usb_driver
        == 0) && ldv_urb_state == 0)) || (((0 == ldv_s_iowarrior_fops_file_operations
        && ldv_s_iowarrior_fops_file_operations == 0) && (ldv_s_iowarrior_driver_usb_driver
        == 0 || ldv_s_iowarrior_driver_usb_driver == 1)) && (ldv_urb_state == 0 ||
        ldv_urb_state == 1))) || (((0 == ldv_s_iowarrior_fops_file_operations && ldv_s_iowarrior_fops_file_operations
        == 0) && (ldv_s_iowarrior_driver_usb_driver == 0 || ldv_s_iowarrior_driver_usb_driver
        == 1)) && (ldv_urb_state == 0 || ldv_urb_state == 1))) || (((0 == ldv_s_iowarrior_driver_usb_driver
        && ldv_s_iowarrior_fops_file_operations == 1) && ldv_s_iowarrior_driver_usb_driver
        == 0) && ldv_urb_state == 0)) || (((ldv_s_iowarrior_fops_file_operations ==
        0 || ldv_s_iowarrior_fops_file_operations == 1) && (ldv_s_iowarrior_driver_usb_driver
        == 0 || ldv_s_iowarrior_driver_usb_driver == 1)) && (ldv_urb_state == 0 ||
        ldv_urb_state == 1))) || (((0 == ldv_s_iowarrior_driver_usb_driver && ldv_s_iowarrior_fops_file_operations
        == 1) && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0)) ||
        ((ldv_s_iowarrior_driver_usb_driver == 0 && ldv_urb_state == 0) && ((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2))) || ((ldv_s_iowarrior_driver_usb_driver == 0 && ldv_urb_state == 0)
        && (ldv_s_iowarrior_fops_file_operations == 1 || ldv_s_iowarrior_fops_file_operations
        == 2))) || (((((0 == ldv_s_iowarrior_fops_file_operations && 0 == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_fops_file_operations == 0) && ldv_s_iowarrior_fops_file_operations
        == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_driver_usb_driver
        == 0) && ldv_urb_state == 0)) || ((ldv_s_iowarrior_driver_usb_driver == 1
        && ldv_urb_state == 1) && ((ldv_s_iowarrior_fops_file_operations == 0 || ldv_s_iowarrior_fops_file_operations
        == 1) || ldv_s_iowarrior_fops_file_operations == 2)))) || (((ldv_s_iowarrior_driver_usb_driver
        == 0 && ldv_urb_state == 0) && (ldv_s_iowarrior_fops_file_operations == 1
        || ldv_s_iowarrior_fops_file_operations == 3)) && (ldv_coherent_state == 0
        || ldv_coherent_state == 1))) || (((ldv_s_iowarrior_driver_usb_driver == 0
        && ldv_urb_state == 0) && ldv_coherent_state == 0) && ((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2))) || ((((((0 == ldv_s_iowarrior_fops_file_operations && 0 == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_fops_file_operations == 0) && ldv_s_iowarrior_fops_file_operations
        == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_driver_usb_driver
        == 0) && ldv_urb_state == 0) && ldv_coherent_state == 0)) || (((ldv_s_iowarrior_driver_usb_driver
        == 0 && ldv_urb_state == 0) && ldv_coherent_state == 0) && (((ldv_s_iowarrior_fops_file_operations
        == 0 || ldv_s_iowarrior_fops_file_operations == 1) || ldv_s_iowarrior_fops_file_operations
        == 2) || ldv_s_iowarrior_fops_file_operations == 3))) || ((((((0 == ldv_s_iowarrior_fops_file_operations
        && 0 == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_fops_file_operations == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0) && ldv_coherent_state
        == 0))) || (ldv_coherent_state == 0 && ((((((((((((((0 == ldv_s_iowarrior_fops_file_operations
        && 0 == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_fops_file_operations == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0) || ((ldv_s_iowarrior_fops_file_operations
        == 1 && ldv_s_iowarrior_driver_usb_driver == 1) && ldv_urb_state == 1)) ||
        (((0 == ldv_s_iowarrior_fops_file_operations && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_driver_usb_driver == 1) && ldv_urb_state == 1)) ||
        (((0 == ldv_s_iowarrior_fops_file_operations && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_urb_state == 1) && (ldv_s_iowarrior_driver_usb_driver == 0 ||
        ldv_s_iowarrior_driver_usb_driver == 1))) || (((0 == ldv_s_iowarrior_fops_file_operations
        && ldv_s_iowarrior_fops_file_operations == 0) && (ldv_s_iowarrior_driver_usb_driver
        == 0 || ldv_s_iowarrior_driver_usb_driver == 1)) && (ldv_urb_state == 0 ||
        ldv_urb_state == 1))) || (((0 == ldv_s_iowarrior_driver_usb_driver && ldv_s_iowarrior_fops_file_operations
        == 1) && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0)) ||
        (((0 == ldv_s_iowarrior_driver_usb_driver && ldv_s_iowarrior_fops_file_operations
        == 1) && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0)) ||
        (((((0 == ldv_s_iowarrior_fops_file_operations && 0 == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_fops_file_operations == 0) && ldv_s_iowarrior_fops_file_operations
        == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_driver_usb_driver
        == 0) && ldv_urb_state == 0)) || ((ldv_s_iowarrior_driver_usb_driver == 0
        && ldv_urb_state == 0) && ((ldv_s_iowarrior_fops_file_operations == 0 || ldv_s_iowarrior_fops_file_operations
        == 1) || ldv_s_iowarrior_fops_file_operations == 2))) || (((((0 == ldv_s_iowarrior_fops_file_operations
        && 0 == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_fops_file_operations == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0)))) || (ldv_coherent_state
        == 0 && ((((0 == ldv_s_iowarrior_fops_file_operations && ldv_s_iowarrior_fops_file_operations
        == 0) && ((((0 == ldv_s_iowarrior_driver_usb_driver && ldv_s_iowarrior_fops_file_operations
        == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_driver_usb_driver
        == 0) && ldv_urb_state == 0) || (ldv_s_iowarrior_driver_usb_driver == 1 &&
        ldv_urb_state == 1))) || (((0 == ldv_s_iowarrior_driver_usb_driver && ldv_s_iowarrior_fops_file_operations
        == 1) && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0)) ||
        (((((0 == ldv_s_iowarrior_fops_file_operations && 0 == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_fops_file_operations == 0) && ldv_s_iowarrior_fops_file_operations
        == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_driver_usb_driver
        == 0) && ldv_urb_state == 0)))) || ((((((0 == ldv_s_iowarrior_fops_file_operations
        && 0 == ldv_s_iowarrior_driver_usb_driver) && ldv_s_iowarrior_fops_file_operations
        == 0) && ldv_s_iowarrior_fops_file_operations == ldv_s_iowarrior_driver_usb_driver)
        && ldv_s_iowarrior_driver_usb_driver == 0) && ldv_urb_state == 0) && ldv_coherent_state
        == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 5124
        column: 3
        function: iowarrior_probe
      value: -12 == retval
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 5124
        column: 3
        function: iowarrior_probe
      value: retval == -12
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 5124
        column: 3
        function: iowarrior_probe
      value: LDV_IN_INTERRUPT == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 5124
        column: 3
        function: iowarrior_probe
      value: ((((4 <= i && i <= 255) || i == 3) || i == 2) || i == 1) || (0 == i &&
        i == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-usb-misc-iowarrior.ko.cil.out.i
        line: 5124
        column: 3
        function: iowarrior_probe
      value: (((((((((((((((((((((((((((((((((((((((((((((((((((((ldv_urb_state ==
        0 && ldv_coherent_state == 0) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0
        && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state
        == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state
        == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state
        == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || 0 <= ldv_coherent_state) || 0 <= ldv_coherent_state)
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || 0 <= ldv_coherent_state)
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state
        && 0 <= ldv_coherent_state)) || (0 <= ldv_urb_state && 0 <= ldv_coherent_state))
        || (0 <= ldv_urb_state && 0 <= ldv_coherent_state)) || (ldv_urb_state == 0
        && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state
        == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)) || (ldv_urb_state
        == 0 && ldv_coherent_state == 0)) || (ldv_urb_state == 0 && ldv_coherent_state
        == 0)) || (ldv_urb_state == 0 && ldv_coherent_state == 0)
      format: c_expression
