- entry_type: invariant_set
  metadata:
    format_version: "2.0"
    uuid: dc3826ea-49c7-4187-bbc9-b60a3686fe69
    creation_time: 2025-03-21T01:25:00Z
    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'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i: 5d4ac8f9993fdd9a611524b9b9f0ae991f3672b4fa16738dbd64025282f00ca6
      data_model: ILP32
      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/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: current_execution_context == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: jiffies == 0UL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: fixed_cdev_used == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: number_cdev_registered == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: number_genhd_registered == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: number_fixed_genhd_used == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: registered_pci_driver.dev_initialized == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: registered_pci_driver.no_pci_device_id == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_dev.bus == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_dev.dev.release == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_dev.devfn == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_dev.device == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_dev.dma_mask == 0ULL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_dev.irq == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_dev.vendor == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_driver == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: number_tasklet_registered == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: number_timer_registered == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: number_request_queue_used == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: proc_root_driver == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.allocated == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.break_ctl == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.cdev.count == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.cdev.dev == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.cdev.ops == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.cdev.owner == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.chars_in_buffer == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.close == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.driver_name == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.flags == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.flush_buffer == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.flush_chars == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.hangup == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.init_termios.c_cflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.init_termios.c_iflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.init_termios.c_lflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.init_termios.c_line == (unsigned char)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.init_termios.c_oflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.ioctl == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.magic == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.major == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.minor_num == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.minor_start == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.name == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.name_base == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.num == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.open == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.owner == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.proc_entry == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.put_char == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.read_proc == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.refcount == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.send_xchar == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.set_ldisc == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.set_termios == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.start == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.stop == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.subtype == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.throttle == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.tiocmget == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.tiocmset == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.type == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.unthrottle == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.wait_until_sent == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.write == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.write_proc == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.write_room == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: global_tty_driver.registered == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: ddv_ioport_request_start == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: ddv_ioport_request_len == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: (unsigned int )registered_pci_driver.pci_dev.dev.driver_data == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2668
        column: 5
        function: init_kernel
      value: (((((((((i == 10 || i == 9) || i == 8) || i == 7) || i == 6) || i ==
        5) || i == 4) || 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/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: current_execution_context == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: jiffies == 0UL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: fixed_cdev_used == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: number_cdev_registered == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: number_genhd_registered == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: number_fixed_genhd_used == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: registered_pci_driver.dev_initialized == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: registered_pci_driver.no_pci_device_id == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_dev.bus == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_dev.dev.release == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_dev.devfn == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_dev.device == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_dev.dma_mask == 0ULL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_dev.irq == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_dev.vendor == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: registered_pci_driver.pci_driver == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: number_tasklet_registered == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: number_timer_registered == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: number_request_queue_used == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: proc_root_driver == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.allocated == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.break_ctl == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.cdev.count == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.cdev.dev == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.cdev.ops == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.cdev.owner == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.chars_in_buffer == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.close == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.driver_name == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.flags == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.flush_buffer == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.flush_chars == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.hangup == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.init_termios.c_cflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.init_termios.c_iflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.init_termios.c_lflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.init_termios.c_line == (unsigned char)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.init_termios.c_oflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.ioctl == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.magic == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.major == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.minor_num == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.minor_start == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.name == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.name_base == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.num == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.open == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.owner == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.proc_entry == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.put_char == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.read_proc == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.refcount == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.send_xchar == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.set_ldisc == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.set_termios == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.start == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.stop == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.subtype == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.throttle == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.tiocmget == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.tiocmset == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.type == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.unthrottle == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.wait_until_sent == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.write == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.write_proc == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.driver.write_room == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: global_tty_driver.registered == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: ddv_ioport_request_start == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: ddv_ioport_request_len == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: (unsigned int )registered_pci_driver.pci_dev.dev.driver_data == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2672
        column: 5
        function: init_kernel
      value: i == 1 || (0 == i && i == 0)
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: jiffies == 0UL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: fixed_cdev_used == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: number_genhd_registered == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: number_fixed_genhd_used == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: registered_pci_driver.dev_initialized == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: registered_pci_driver.no_pci_device_id == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: registered_pci_driver.pci_dev.bus == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: registered_pci_driver.pci_dev.dev.release == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: registered_pci_driver.pci_dev.devfn == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: registered_pci_driver.pci_dev.device == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: registered_pci_driver.pci_dev.dma_mask == 0ULL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: registered_pci_driver.pci_dev.irq == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: registered_pci_driver.pci_dev.vendor == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: registered_pci_driver.pci_driver == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: number_tasklet_registered == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: number_request_queue_used == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: proc_root_driver == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.allocated == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.break_ctl == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.cdev.count == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.cdev.dev == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.cdev.ops == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.cdev.owner == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.chars_in_buffer == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.close == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.driver_name == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.flags == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.flush_buffer == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.flush_chars == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.hangup == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.init_termios.c_cflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.init_termios.c_iflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.init_termios.c_lflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.init_termios.c_line == (unsigned char)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.init_termios.c_oflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.ioctl == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.magic == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.major == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.minor_num == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.minor_start == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.name == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.name_base == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.num == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.open == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.owner == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.proc_entry == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.put_char == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.read_proc == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.refcount == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.send_xchar == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.set_ldisc == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.set_termios == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.start == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.stop == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.subtype == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.throttle == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.tiocmget == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.tiocmset == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.type == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.unthrottle == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.wait_until_sent == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.write == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.write_proc == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.driver.write_room == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: global_tty_driver.registered == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: (unsigned int )registered_pci_driver.pci_dev.dev.driver_data == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: number_cdev_registered == (short)0 || number_cdev_registered == (short)1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: number_timer_registered == (short)0 || number_timer_registered == (short)1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: ddv_ioport_request_start == 0 || ddv_ioport_request_start == 536
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: ddv_ioport_request_len == 0 || ddv_ioport_request_len == 3
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 2682
        column: 5
        function: ddv
      value: ((unsigned short)1 <= random && (current_execution_context == 1 || current_execution_context
        == 2)) || current_execution_context == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: current_execution_context == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: jiffies == 0UL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: fixed_cdev_used == 1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: number_cdev_registered == (short)1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: number_genhd_registered == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: number_fixed_genhd_used == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: registered_pci_driver.dev_initialized == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: registered_pci_driver.no_pci_device_id == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: registered_pci_driver.pci_dev.bus == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: registered_pci_driver.pci_dev.dev.release == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: registered_pci_driver.pci_dev.devfn == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: registered_pci_driver.pci_dev.device == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: registered_pci_driver.pci_dev.dma_mask == 0ULL
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: registered_pci_driver.pci_dev.irq == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: registered_pci_driver.pci_dev.vendor == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: registered_pci_driver.pci_driver == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: number_tasklet_registered == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: number_request_queue_used == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: proc_root_driver == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.allocated == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.break_ctl == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.cdev.count == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.cdev.dev == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.cdev.ops == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.cdev.owner == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.chars_in_buffer == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.close == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.driver_name == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.flags == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.flush_buffer == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.flush_chars == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.hangup == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.init_termios.c_cflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.init_termios.c_iflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.init_termios.c_lflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.init_termios.c_line == (unsigned char)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.init_termios.c_oflag == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.ioctl == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.magic == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.major == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.minor_num == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.minor_start == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.name == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.name_base == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.num == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.open == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.owner == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.proc_entry == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.put_char == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.read_proc == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.refcount == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.send_xchar == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.set_ldisc == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.set_termios == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.start == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.stop == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.subtype == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.throttle == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.tiocmget == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.tiocmset == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.type == (short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.unthrottle == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.wait_until_sent == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.write == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.write_proc == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.driver.write_room == 0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: global_tty_driver.registered == (unsigned short)0
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: (unsigned int )registered_pci_driver.pci_dev.dev.driver_data == 0U
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: number_timer_registered == (short)0 || number_timer_registered == (short)1
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: ddv_ioport_request_start == 0 || ddv_ioport_request_start == 536
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: ddv_ioport_request_len == 0 || ddv_ioport_request_len == 3
      format: c_expression
  - invariant:
      type: loop_invariant
      location:
        file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ddv-machzwd/ddv_machzwd_outb_p.i
        line: 1642
        column: 4
        function: zf_write
      value: (((4U <= count || (3U <= count && ofs == 3U)) || (2U <= count && ofs
        == 2U)) || (1U <= count && ofs == 1U)) || ((1U <= count && 0 == ofs) && ofs
        == 0U)
      format: c_expression
