- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: b6a80511-7d16-46dd-83b4-64742b0632ca
    creation_time: 2024-04-23T11:02:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || ((0 <= flag && flag <= 1) && (flag == 0 || flag ==
      1))'
    type: assertion
    format: C
- entry_type: flow_insensitive_invariant
  metadata:
    format_version: "2.0"
    uuid: 7f4ed952-ddcc-4caf-b0d1-68e25e1562bb
    creation_time: 2024-04-23T11:02:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  flow_insensitive_invariant:
    string: '! multithreaded || (0 <= num && num <= 1)'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "2.0"
    uuid: 15db7a10-a883-471e-b065-de6df0375734
    creation_time: 2024-04-23T11:02:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 5fa87dab-7e56-44bc-ae69-bba9ba862aad
    creation_time: 2024-04-23T11:02:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
    file_hash: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
    line: 881
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: e9de80a4-5457-4d4b-aff9-5a8b2ce83045
    creation_time: 2024-04-23T11:02:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
    file_hash: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
    line: 881
    column: 7
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: c1393d85-8fdd-4a0a-b970-49cd4e96af46
    creation_time: 2024-04-23T11:02:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
    file_hash: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
    line: 898
    column: 5
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: a833972f-e4a5-4cf7-bd2d-fe0727fe9dec
    creation_time: 2024-04-23T11:02:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
    file_hash: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
    line: 895
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: d355b11f-0fcc-4f83-a89e-a8b11e4dc20d
    creation_time: 2024-04-23T11:02:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
    file_hash: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
    line: 895
    column: 7
    function: thread2
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: a891f896-c157-42a7-8a7b-905d7a9073d3
    creation_time: 2024-04-23T11:02:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "0"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
    file_hash: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
    line: 883
    column: 5
    function: thread1
- entry_type: ghost_variable
  metadata:
    format_version: "2.0"
    uuid: 39f6f0d7-4dc5-4a48-afb1-10e1c418eb3f
    creation_time: 2024-04-23T11:02:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  scope: global
  type: int
  initial: "0"
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 7e58ad21-bb8e-412b-8050-67a78aa6b2b9
    creation_time: 2024-04-23T11:02:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: multithreaded
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
    file_hash: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
    line: 913
    column: 3
    function: main
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: 40ea58d4-0cdc-460d-8905-6e7609512484
    creation_time: 2024-04-23T11:02:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
    file_hash: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
    line: 879
    column: 5
    function: thread1
- entry_type: ghost_update
  metadata:
    format_version: "2.0"
    uuid: de5d1126-0c4f-43bc-94b3-7606c234c6df
    creation_time: 2024-04-23T11:02:21Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-gd6abc0b4f-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--disable''
        ''witness.graphml.enabled'' ''--set'' ''ana.activated[+]'' ''mutexGhosts''
        ''--set'' ''ana.activated[+]'' ''pthreadMutexType'' ''--set'' ''witness.yaml.entry-types[-]''
        ''location_invariant'' ''--set'' ''witness.yaml.entry-types[-]'' ''loop_invariant''
        ''--set'' ''witness.yaml.entry-types[+]'' ''flow_insensitive_invariant'' ''--set''
        ''witness.yaml.entry-types[-]'' ''invariant_set'' ''--enable'' ''witness.invariant.after-lock''
        ''--enable'' ''witness.invariant.other'' ''--enable'' ''witness.invariant.accessed''
        ''--disable'' ''witness.invariant.all-locals'' ''--sets'' ''ana.specification''
        ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp''
        ''--sets'' ''exp.architecture'' ''32bit'' ''/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  variable: m_locked
  expression: "1"
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-deagle/arithmetic_prog_ok.i
    file_hash: 29016034e4102bf62d4fcba069301a54da1d77dfd5739e4cf52e395ddaa22e38
    line: 893
    column: 5
    function: thread2
