- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 670cebe7-b0c5-4821-9c5a-d9a819146370
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2b278416-d96c-44fd-8aa9-8780dac6dc37
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 086e29fe-89d3-4b24-b5e4-b916566d2ab4
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d99d4e51-d4d7-41e4-8224-16144c610450
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77989f35-c23b-4c9f-8e26-ba50f0a30f05
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 2) && ((x == 0 || x == 1) || x ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e2a24ff-32ba-460b-828b-371e8d6be04e
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 2) && ((x == 0 || x == 1) || x ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ffb0e3a1-bbbe-4be3-b647-1e77f920e632
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 2) && ((x == 0 || x == 1) || x ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: cd51f8c9-adbb-4f85-b3b4-6c65a27eacbd
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x && x <= 2) && ((x == 0 || x == 1) || x ==
      2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a094aee0-f15a-4acf-b40d-99e07d22bbc1
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p3_EAX) && 0 <= a) && 0 <=
      x) && 0 <= x$mem_tmp) && 0 <= x$w_buff0) && 0 <= x$w_buff1) && 0 <= y) && 0
      <= z) && __unbuffered_p1_EAX <= 1) && __unbuffered_p3_EAX <= 1) && a <= 1) &&
      x <= 2) && x$mem_tmp <= 2) && x$w_buff0 <= 2) && x$w_buff0 <= 127) && x$w_buff1
      <= 2) && x$w_buff1 <= 127) && y <= 1) && z <= 2) && x$flush_delayed == (_Bool)0)
      && x$r_buff0_thd0 == (_Bool)0) && x$r_buff0_thd1 == (_Bool)0) && x$r_buff0_thd3
      == (_Bool)0) && x$r_buff0_thd4 == (_Bool)0) && x$r_buff1_thd0 == (_Bool)0) &&
      x$r_buff1_thd1 == (_Bool)0) && x$r_buff1_thd3 == (_Bool)0) && x$r_buff1_thd4
      == (_Bool)0) && x$read_delayed == (_Bool)0) && x$read_delayed_var == 0) && x$w_buff0
      % 2 == 0) && x$w_buff1 % 2 == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX
      == 1)) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1)) && (a == 0
      || a == 1)) && (x$w_buff0 == 0 || x$w_buff0 == 2)) && (x$w_buff1 == 0 || x$w_buff1
      == 2)) && (y == 0 || y == 1)) && ((x == 0 || x == 1) || x == 2)) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2)) && ((z == 0 || z == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 81b8d176-63f2-445e-9cc8-40e6d7874222
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p3_EAX) && 0 <= a) && 0 <=
      x) && 0 <= x$mem_tmp) && 0 <= x$w_buff0) && 0 <= x$w_buff1) && 0 <= y) && 0
      <= z) && __unbuffered_p1_EAX <= 1) && __unbuffered_p3_EAX <= 1) && a <= 1) &&
      x <= 2) && x$mem_tmp <= 2) && x$w_buff0 <= 2) && x$w_buff0 <= 127) && x$w_buff1
      <= 2) && x$w_buff1 <= 127) && y <= 1) && z <= 2) && x$flush_delayed == (_Bool)0)
      && x$r_buff0_thd0 == (_Bool)0) && x$r_buff0_thd1 == (_Bool)0) && x$r_buff0_thd3
      == (_Bool)0) && x$r_buff0_thd4 == (_Bool)0) && x$r_buff1_thd0 == (_Bool)0) &&
      x$r_buff1_thd1 == (_Bool)0) && x$r_buff1_thd3 == (_Bool)0) && x$r_buff1_thd4
      == (_Bool)0) && x$read_delayed == (_Bool)0) && x$read_delayed_var == 0) && x$w_buff0
      % 2 == 0) && x$w_buff1 % 2 == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX
      == 1)) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1)) && (a == 0
      || a == 1)) && (x$w_buff0 == 0 || x$w_buff0 == 2)) && (x$w_buff1 == 0 || x$w_buff1
      == 2)) && (y == 0 || y == 1)) && ((x == 0 || x == 1) || x == 2)) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2)) && ((z == 0 || z == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 676e6450-a32d-4e19-b15c-95a2835e806f
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p3_EAX) && 0 <= a) && 0 <=
      x) && 0 <= x$mem_tmp) && 0 <= x$w_buff0) && 0 <= x$w_buff1) && 0 <= y) && 0
      <= z) && __unbuffered_p1_EAX <= 1) && __unbuffered_p3_EAX <= 1) && a <= 1) &&
      x <= 2) && x$mem_tmp <= 2) && x$w_buff0 <= 2) && x$w_buff0 <= 127) && x$w_buff1
      <= 2) && x$w_buff1 <= 127) && y <= 1) && z <= 2) && x$flush_delayed == (_Bool)0)
      && x$r_buff0_thd0 == (_Bool)0) && x$r_buff0_thd1 == (_Bool)0) && x$r_buff0_thd3
      == (_Bool)0) && x$r_buff0_thd4 == (_Bool)0) && x$r_buff1_thd0 == (_Bool)0) &&
      x$r_buff1_thd1 == (_Bool)0) && x$r_buff1_thd3 == (_Bool)0) && x$r_buff1_thd4
      == (_Bool)0) && x$read_delayed == (_Bool)0) && x$read_delayed_var == 0) && x$w_buff0
      % 2 == 0) && x$w_buff1 % 2 == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX
      == 1)) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1)) && (a == 0
      || a == 1)) && (x$w_buff0 == 0 || x$w_buff0 == 2)) && (x$w_buff1 == 0 || x$w_buff1
      == 2)) && (y == 0 || y == 1)) && ((x == 0 || x == 1) || x == 2)) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2)) && ((z == 0 || z == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 77115451-dbe9-4f2e-b38d-93bea44b81fd
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((((((((((((((((((((((((((((((((((((((((0 <= __unbuffered_cnt
      && 0 <= __unbuffered_p1_EAX) && 0 <= __unbuffered_p3_EAX) && 0 <= a) && 0 <=
      x) && 0 <= x$mem_tmp) && 0 <= x$w_buff0) && 0 <= x$w_buff1) && 0 <= y) && 0
      <= z) && __unbuffered_p1_EAX <= 1) && __unbuffered_p3_EAX <= 1) && a <= 1) &&
      x <= 2) && x$mem_tmp <= 2) && x$w_buff0 <= 2) && x$w_buff0 <= 127) && x$w_buff1
      <= 2) && x$w_buff1 <= 127) && y <= 1) && z <= 2) && x$flush_delayed == (_Bool)0)
      && x$r_buff0_thd0 == (_Bool)0) && x$r_buff0_thd1 == (_Bool)0) && x$r_buff0_thd3
      == (_Bool)0) && x$r_buff0_thd4 == (_Bool)0) && x$r_buff1_thd0 == (_Bool)0) &&
      x$r_buff1_thd1 == (_Bool)0) && x$r_buff1_thd3 == (_Bool)0) && x$r_buff1_thd4
      == (_Bool)0) && x$read_delayed == (_Bool)0) && x$read_delayed_var == 0) && x$w_buff0
      % 2 == 0) && x$w_buff1 % 2 == 0) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX
      == 1)) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1)) && (a == 0
      || a == 1)) && (x$w_buff0 == 0 || x$w_buff0 == 2)) && (x$w_buff1 == 0 || x$w_buff1
      == 2)) && (y == 0 || y == 1)) && ((x == 0 || x == 1) || x == 2)) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2)) && ((z == 0 || z == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 06764d13-8a50-4d99-b665-467c22e54731
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 03a19ec8-dbcb-4d07-8592-75a40ada9b56
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 755bb4e1-6886-4ac5-9c16-71e959faf9cd
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 325a9ea4-7a0d-490e-938a-acb4b8e405dd
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 9f4cbc5b-a11e-475a-b02e-652be9009ed2
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= x$w_buff1 && x$w_buff1 <= 2) && x$w_buff1
      <= 127) && x$w_buff1 % 2 == 0) && (x$w_buff1 == 0 || x$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6320d32b-cd12-4c49-a623-08aa86b4a3d7
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= x$w_buff1 && x$w_buff1 <= 2) && x$w_buff1
      <= 127) && x$w_buff1 % 2 == 0) && (x$w_buff1 == 0 || x$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 464f20d4-2309-43af-b03e-bd1808c536e0
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= x$w_buff1 && x$w_buff1 <= 2) && x$w_buff1
      <= 127) && x$w_buff1 % 2 == 0) && (x$w_buff1 == 0 || x$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ebc586f0-92f9-4b9d-92e9-6401109854cc
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= x$w_buff1 && x$w_buff1 <= 2) && x$w_buff1
      <= 127) && x$w_buff1 % 2 == 0) && (x$w_buff1 == 0 || x$w_buff1 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3a0f3de9-bea6-4131-8631-c7b0eef83e7c
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 783c6c79-fdcb-47a5-9ad6-a2c00d0b4428
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7cee44e5-27a6-4692-ba2e-b2fcd2b0b7e6
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ad487570-aa23-48ad-a232-59b145edfab7
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p3_EAX && __unbuffered_p3_EAX
      <= 1) && (__unbuffered_p3_EAX == 0 || __unbuffered_p3_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: be785f0c-2bec-49d9-a8b5-7e554997a45e
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a93bffdf-2e0d-43bb-a8a9-6a7e435fefdd
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 922677ea-894a-44f0-a548-53d1e9abc8cb
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c2c84ed0-dd8a-46bb-b82b-31d3bfa352e0
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= __unbuffered_p1_EAX && __unbuffered_p1_EAX
      <= 1) && (__unbuffered_p1_EAX == 0 || __unbuffered_p1_EAX == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b248a7b9-bb57-483f-8c4b-ae41b566b8aa
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 07364972-6c7e-4f27-88e9-e0ba3a1eed25
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: f17d13b3-0b59-4da0-9c14-51f6c516af15
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: d36d6d8a-faa5-4311-a960-d4669863bcbf
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= a && a <= 1) && (a == 0 || a == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 661a0c0c-2443-4f92-ae60-edca565e1212
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2aba2eb8-f0f4-4d5f-a10c-3da3fee178a6
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 0d29a82e-f3ca-4d75-8aee-b0f5909b286d
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e23d10f-6135-4a3f-b722-fd7532786299
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed_var == 0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a66137bf-ac20-4662-a5b5-c30f58b0f1a3
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 383ce7b3-f7b7-486c-9843-f9d749803764
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 95884029-f896-4eb3-b74f-745320911e37
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: b25a27d7-7586-48f1-aa3b-a3a2c1a34fa9
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 87dc1582-9526-4951-86dc-ab3129cff4b6
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 10eb060b-2f2a-48bd-b675-8626e8131a48
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3307bc39-5cdd-49c4-bf0c-f5d84d27bc17
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 53bec24b-602a-4b38-8758-a5329a57e65b
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= y && y <= 1) && (y == 0 || y == 1))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 691e7c4b-7935-4978-8f04-d4664e56cfc6
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$mem_tmp && x$mem_tmp <= 2) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 2f6039e2-4df2-4d47-a364-37e9cc3ed92e
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$mem_tmp && x$mem_tmp <= 2) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a2cc2489-3d4b-43a6-81b7-23bb0e24a2c2
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$mem_tmp && x$mem_tmp <= 2) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99180bc4-9727-497b-bde4-edcdcd361a8c
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((0 <= x$mem_tmp && x$mem_tmp <= 2) && ((x$mem_tmp
      == 0 || x$mem_tmp == 1) || x$mem_tmp == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5784cff2-fe73-4399-929f-d69f567515b2
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 54a0e291-b659-41f3-82af-9e9278363fd1
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 88b62744-9402-4d2f-a3b5-d829c677b0f7
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5aa373b5-f55f-4934-a42a-9e818d06d483
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || (((0 <= z && z <= 2) && z <= 127) && ((z == 0 || z
      == 1) || z == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e2199ea9-fb4e-4e2f-a9b3-d1d19f37ce56
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c8c9d9be-74e8-4f9f-89a4-1c5632157ae5
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 744a8da5-e4f9-4a2d-8b57-19c4392e8bb2
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 80d0f0ab-1918-4810-91bb-2d5dfef4533f
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 7e312274-041a-429a-80f8-39198217f3f4
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 61c4ceea-e0be-485b-aaad-83ec38c23e50
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 6e9c1da2-b1c5-420e-bce0-3c058108d92b
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 26dbdbbb-c84d-4c4e-9214-bf32fb916ee4
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd1 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: c585bb05-01e7-4897-ad94-98cccf4ff70a
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1d699dca-64f3-4be9-9bce-f04281a5fff5
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 93e2071f-2782-429a-b62e-b8368640f005
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e10ead17-c01d-4925-9294-90374dbbaf8f
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd3 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 1a1afe0f-1106-4c3d-ab56-e26212527b66
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 48768fd6-bfd5-44e3-b71f-67144eedcfad
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: fdb47a7c-9fd3-401d-8abc-14e7928d140f
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 593c399a-6db7-4364-bc5d-2df550083f76
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff0_thd4 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63ba6d91-c3c6-456d-8dd4-0593677a58d6
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 58a24794-c072-4927-85a0-5a3a15991079
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: e96aaac7-e24b-4e56-9e25-c5605174c3f6
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 44ec9c61-7776-4057-9254-6ec2efb60c59
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$read_delayed == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: dc16a5d4-196e-4960-ac6e-c45e3dbae688
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 99f1eb67-63bb-491b-aa9c-6f8fe36ddd56
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 39856176-7a8b-44bd-a857-57a221c140f7
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 62f06261-b34d-48bc-8516-5589b2aca17b
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || x$r_buff1_thd0 == (_Bool)0'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 63ef4cad-2a80-43bf-8502-b37573b227ff
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: a6ab56b8-8b70-4379-ba33-8b3ae7fbdcfe
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 5e953d5f-845c-454e-b577-9b56bfcc8bb3
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 4c439a34-b5b2-40d2-8637-c19e03ead1b9
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || 0 <= __unbuffered_cnt'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 23f979d1-45d4-449b-991a-e6e06cf0b49a
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 849
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= x$w_buff0 && x$w_buff0 <= 2) && x$w_buff0
      <= 127) && x$w_buff0 % 2 == 0) && (x$w_buff0 == 0 || x$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: 3662f322-d3ae-44ba-a7d8-122368c955a9
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 851
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= x$w_buff0 && x$w_buff0 <= 2) && x$w_buff0
      <= 127) && x$w_buff0 % 2 == 0) && (x$w_buff0 == 0 || x$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: ee6717dc-66c3-4d0b-b57f-ee8bf2698ccc
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 853
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= x$w_buff0 && x$w_buff0 <= 2) && x$w_buff0
      <= 127) && x$w_buff0 % 2 == 0) && (x$w_buff0 == 0 || x$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: location_invariant
  metadata:
    format_version: "0.1"
    uuid: eb15216e-c5c4-452e-90fa-34cf70451d70
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      data_model: ILP32
      language: C
      specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
  location:
    file_name: /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 854
    column: 3
    function: main
  location_invariant:
    string: '! multithreaded || ((((0 <= x$w_buff0 && x$w_buff0 <= 2) && x$w_buff0
      <= 127) && x$w_buff0 % 2 == 0) && (x$w_buff0 == 0 || x$w_buff0 == 2))'
    type: assertion
    format: C
- entry_type: ghost_variable
  metadata:
    format_version: "0.1"
    uuid: 78f086d9-f8f8-466d-8f20-cce25a091c16
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      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: "0.1"
    uuid: bf38d0c8-bd25-4add-890c-0a7d5982f1fa
    creation_time: 2024-06-18T14:55:50Z
    producer:
      name: Goblint
      version: heads/yaml-witness-ghost-0-g7fcb10cd0-dirty
      command_line: '''./goblint'' ''--conf'' ''conf/svcomp-ghost.json'' ''--set''
        ''ana.base.privatization'' ''mutex-meet'' ''--set'' ''ana.autotune.activated[-]''
        ''octagon'' ''--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-wmm/mix055_tso.oepc.i'''
    task:
      input_files:
      - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i
      input_file_hashes:
        /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/mix055_tso.oepc.i: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
      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-wmm/mix055_tso.oepc.i
    file_hash: 9ec75f624fee0326f6dc01ebf4c0afe8f65e83cfa5c5726cd79e55765f7366f9
    line: 847
    column: 3
    function: main
