- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: 8facb0cd-2993-4640-858e-77841686d18d
    creation_time: 2025-03-22T04:37:09Z
    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-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
      input_file_hashes:
        ? /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        : 4426d364359557dc10cf7e8f346d379b7d379eaf4a1a095af818bcdb9a3f651d
      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-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 0U == b0[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 0U == b2[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 0U == b3[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 0U == b4[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 0U == get_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 0U == get_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 0U == get_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 0U == get_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 0U == get_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 0U == get_dsp_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 0U == get_dsp_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 0U == get_dsp_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 0U == get_dsp_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 0U == get_dsp_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 1U == b0[3]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 1U == b1[3]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 1U == b1[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 1U == b2[3]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 1U == b3[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 1U == b4[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 2U == b3[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 2U == b4[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 4U == b4[3]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 5U == b3[3]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 5U == get_version[3]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 16U == b3[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 16U == b4[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 21U == b0[2]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 21U == b1[2]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 23U == get_version[2]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 28U == get_dsp_version[3]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 30U == b3[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 30U == b4[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 38U == get_dsp_version[2]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 49U == b3[2]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 49U == b4[2]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 50U == b2[2]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 85U == b4[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 170U == b0[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 170U == b1[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 170U == b2[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 170U == b3[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 170U == get_version[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: 170U == get_dsp_version[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[0] == b1[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[0] == b2[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[0] == b3[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[0] == get_version[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[0] == get_dsp_version[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[2] == b1[2]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[3] == b1[3]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[3] == b1[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[3] == b2[3]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[3] == b3[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[3] == b4[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[4] == b2[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[4] == b3[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[4] == b4[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[4] == get_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[4] == get_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[4] == get_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[4] == get_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[4] == get_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[4] == get_dsp_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[4] == get_dsp_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[4] == get_dsp_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[4] == get_dsp_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b0[4] == get_dsp_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b1[0] == b2[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b1[0] == b3[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b1[0] == get_version[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b1[0] == get_dsp_version[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b1[3] == b1[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b1[3] == b2[3]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b1[3] == b3[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b1[3] == b4[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b1[4] == b2[3]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b1[4] == b3[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b1[4] == b4[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[0] == b3[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[0] == get_version[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[0] == get_dsp_version[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[3] == b3[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[3] == b4[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[4] == b3[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[4] == b4[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[4] == get_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[4] == get_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[4] == get_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[4] == get_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[4] == get_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[4] == get_dsp_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[4] == get_dsp_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[4] == get_dsp_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[4] == get_dsp_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b2[4] == get_dsp_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[0] == get_version[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[0] == get_dsp_version[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[2] == b4[2]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[3] == get_version[3]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[4] == b4[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[5] == b4[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[6] == b4[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[7] == b4[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[7] == get_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[7] == get_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[7] == get_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[7] == get_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[7] == get_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[7] == get_dsp_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[7] == get_dsp_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[7] == get_dsp_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[7] == get_dsp_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[7] == get_dsp_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b3[8] == b4[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b4[7] == get_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b4[7] == get_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b4[7] == get_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b4[7] == get_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b4[7] == get_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b4[7] == get_dsp_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b4[7] == get_dsp_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b4[7] == get_dsp_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b4[7] == get_dsp_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: b4[7] == get_dsp_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[0] == get_dsp_version[0]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[4] == get_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[4] == get_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[4] == get_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[4] == get_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[4] == get_dsp_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[4] == get_dsp_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[4] == get_dsp_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[4] == get_dsp_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[4] == get_dsp_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[5] == get_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[5] == get_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[5] == get_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[5] == get_dsp_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[5] == get_dsp_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[5] == get_dsp_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[5] == get_dsp_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[5] == get_dsp_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[6] == get_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[6] == get_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[6] == get_dsp_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[6] == get_dsp_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[6] == get_dsp_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[6] == get_dsp_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[6] == get_dsp_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[7] == get_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[7] == get_dsp_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[7] == get_dsp_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[7] == get_dsp_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[7] == get_dsp_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[7] == get_dsp_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[8] == get_dsp_version[4]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[8] == get_dsp_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[8] == get_dsp_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[8] == get_dsp_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_version[8] == get_dsp_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_dsp_version[4] == get_dsp_version[5]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_dsp_version[4] == get_dsp_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_dsp_version[4] == get_dsp_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_dsp_version[4] == get_dsp_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_dsp_version[5] == get_dsp_version[6]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_dsp_version[5] == get_dsp_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_dsp_version[5] == get_dsp_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_dsp_version[6] == get_dsp_version[7]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_dsp_version[6] == get_dsp_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: get_dsp_version[7] == get_dsp_version[8]
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_thread_0.function == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_thread_0.identifier == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_thread_1.function == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_thread_1.identifier == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_thread_2.function == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_thread_2.identifier == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_thread_3.function == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_thread_3.identifier == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_thread_4.function == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_thread_4.identifier == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_thread_9.function == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_thread_9.identifier == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_alloc_usb_lock_lock == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_arch_io_iomem == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_block_request_blk_rq == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_drivers_base_class_usb_gadget_class == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_fs_char_dev_usb_gadget_chrdev == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_fs_sysfs_sysfs == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_kernel_locking_rwlock_rlock == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_kernel_locking_rwlock_wlock == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_kernel_module_module_refcounter == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_kernel_rcu_srcu_srcu_nested == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_kernel_rcu_update_lock_bh_rcu_nested_bh == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_kernel_rcu_update_lock_sched_rcu_nested_sched == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_kernel_rcu_update_lock_rcu_nested == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_mmc_sdio_func_sdio_element == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_net_register_probe_state == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: rtnllocknumber == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: locksocknumber == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_usb_coherent_coherent_state == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: LDV_LINUX_USB_DEV_USB_DEV_REF_COUNTS == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_usb_gadget_usb_gadget == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ldv_linux_usb_register_probe_state == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: LDV_LINUX_KERNEL_LOCKING_MUTEX_MUTEXES_i_mutex_of_inode == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: LDV_LINUX_KERNEL_LOCKING_MUTEX_MUTEXES_lock == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: LDV_LINUX_KERNEL_LOCKING_MUTEX_MUTEXES_mutex_of_device == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: LDV_LINUX_KERNEL_LOCKING_MUTEX_MUTEXES_semi2c_of_ttusb == (_Bool)1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: LDV_LINUX_KERNEL_LOCKING_MUTEX_MUTEXES_semusb_of_ttusb == (_Bool)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko.cil.i
        line: 8204
        column: 3
        function: ttusb_init_controller
      value: ((ldv_linux_usb_urb_urb_state == 4 || ldv_linux_usb_urb_urb_state <=
        3) || ldv_linux_usb_urb_urb_state <= 2) || (ldv_linux_usb_urb_urb_state ==
        0 || ldv_linux_usb_urb_urb_state == 1)
      format: c_expression
