./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i


--------------------------------------------------------------------------------


Deagle version 2.1 64-bit x86_64 linux
which contains:
CBMC version 5.67.0 (SVCOMP2023_221122-2-g2121ef1a2) 64-bit x86_64 linux
Parsing /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i
Converting
Type-checking lamport-b
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_create> line 20: warning: pointer parameter types differ between declaration and definition "pthread_create"
old definition in module lamport-b file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 404
signed int (pthread_t *, const pthread_attr_t *, void * (*)(void *), void *)
new definition in module <built-in-library> file <builtin-library-pthread_create> line 20
signed int (pthread_t *thread, const pthread_attr_t *attr, void * (*start_routine)(void *), void *arg)
Removal of function pointers and virtual functions
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 2 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
[Warning][Deadcode] Function "__bswap_32" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:67:1)
[Warning][Deadcode] Function "__bswap_64" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:72:1)
[Warning][Deadcode] Function "__uint16_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:77:1)
[Warning][Deadcode] Function "__uint32_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:82:1)
[Warning][Deadcode] Function "__uint64_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:87:1)
[Warning][Race] Memory location y@lamport-b.i:684:8 (race with conf. 110):
  read with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:691:5)
  read with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:693:7)
  read with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:700:7)
  read with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:701:2)
  read with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:717:5)
  read with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:719:7)
  read with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:726:7)
  read with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:727:2)
  write with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:696:5)
  write with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:709:3)
  write with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:722:5)
  write with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:735:3)
[Warning][Race] Memory location b1@lamport-b.i:685:5 (race with conf. 110):
  read with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:725:7)
  write with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:689:5)
  write with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:692:7)
  write with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:698:7)
  write with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:710:3)
[Warning][Race] Memory location b2@lamport-b.i:685:9 (race with conf. 110):
  read with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:699:7)
  write with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:715:5)
  write with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:718:7)
  write with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:724:7)
  write with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:736:3)
[Warning][Race] Memory location x@lamport-b.i:684:5 (race with conf. 110):
  read with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:697:5)
  read with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:723:5)
  write with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:690:5)
  write with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:716:5)
[Warning][Race] Memory location X@lamport-b.i:686:5 (race with conf. 110):
  read with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:708:3)
  read with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:734:3)
  write with {thread:([thr1@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:742:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:707:3)
  write with {thread:([thr2@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:743:3, main], {})} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i:733:3)

Summary for all memory locations:
	safe:            0
	vulnerable:      0
	unsafe:          5
	-------------------
	total:           5
Use SV-COMP unwinding strategy: 2
Deagle's solver is set!!!!!!
replacing self-loop at file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 693 function thr1 by assume(!TRUE)
replacing self-loop at file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 699 function thr1 by assume(!TRUE)
replacing self-loop at file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 701 function thr1 by assume(!TRUE)
Unwinding loop thr1.3 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 688 function thr1 thread 1
replacing self-loop at file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 693 function thr1 by assume(!TRUE)
replacing self-loop at file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 699 function thr1 by assume(!TRUE)
replacing self-loop at file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 701 function thr1 by assume(!TRUE)
Not unwinding loop thr1.3 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 688 function thr1 thread 1
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 1
replacing self-loop at file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 719 function thr2 by assume(!TRUE)
replacing self-loop at file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 725 function thr2 by assume(!TRUE)
replacing self-loop at file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 727 function thr2 by assume(!TRUE)
Unwinding loop thr2.3 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 714 function thr2 thread 2
replacing self-loop at file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 719 function thr2 by assume(!TRUE)
replacing self-loop at file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 725 function thr2 by assume(!TRUE)
replacing self-loop at file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 727 function thr2 by assume(!TRUE)
Not unwinding loop thr2.3 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i line 714 function thr2 thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
Handling datarace, passing the problem to goblint first
getcwd: /mnt/goblint-svcomp/benchexec/tools-pldi/deagle
/mnt/goblint-svcomp/benchexec/tools-pldi/deagle/goblint/goblint /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 689 690 691 692 693 694 696 697 698 699 700 701 702 707 708 709 710 711 715 716 717 718 719 720 722 723 724 725 726 727 728 733 734 735 736 737 
The number of races before goblint filter: 152
The number of races after goblint filter: 100
Race categories: 34
	707(1) - 733(1) X:
		X#2 X#4
	707(1) - 734(1) X:
		X#2 X#5
	708(1) - 733(1) X:
		X#3 X#4
	689(1) - 725(1) b1:
		b1#2 b1#9
		b1#2 b1#10
		b1#5 b1#9
		b1#5 b1#10
	692(1) - 725(1) b1:
		b1#3 b1#9
		b1#3 b1#10
		b1#6 b1#9
		b1#6 b1#10
	698(1) - 725(1) b1:
		b1#4 b1#9
		b1#4 b1#10
		b1#7 b1#9
		b1#7 b1#10
	710(1) - 725(1) b1:
		b1#8 b1#9
		b1#8 b1#10
	699(1) - 715(1) b2:
		b2#2 b2#4
		b2#2 b2#7
		b2#3 b2#4
		b2#3 b2#7
	699(1) - 718(1) b2:
		b2#2 b2#5
		b2#2 b2#8
		b2#3 b2#5
		b2#3 b2#8
	699(1) - 724(1) b2:
		b2#2 b2#6
		b2#2 b2#9
		b2#3 b2#6
		b2#3 b2#9
	699(1) - 736(1) b2:
		b2#2 b2#10
		b2#3 b2#10
	690(1) - 716(1) x:
		x#2 x#6
		x#2 x#8
		x#4 x#6
		x#4 x#8
	690(1) - 723(1) x:
		x#2 x#7
		x#2 x#9
		x#4 x#7
		x#4 x#9
	697(1) - 716(1) x:
		x#3 x#6
		x#3 x#8
		x#5 x#6
		x#5 x#8
	691(1) - 722(1) y:
		y#2 y#15
		y#2 y#20
		y#7 y#15
		y#7 y#20
	691(1) - 735(1) y:
		y#2 y#23
		y#7 y#23
	693(1) - 722(1) y:
		y#3 y#15
		y#3 y#20
		y#8 y#15
		y#8 y#20
	693(1) - 735(1) y:
		y#3 y#23
		y#8 y#23
	696(1) - 717(1) y:
		y#4 y#13
		y#4 y#18
		y#9 y#13
		y#9 y#18
	696(1) - 719(1) y:
		y#4 y#14
		y#4 y#19
		y#9 y#14
		y#9 y#19
	696(1) - 722(1) y:
		y#4 y#15
		y#4 y#20
		y#9 y#15
		y#9 y#20
	696(1) - 726(1) y:
		y#4 y#16
		y#4 y#21
		y#9 y#16
		y#9 y#21
	696(1) - 727(1) y:
		y#4 y#17
		y#4 y#22
		y#9 y#17
		y#9 y#22
	696(1) - 735(1) y:
		y#4 y#23
		y#9 y#23
	700(1) - 722(1) y:
		y#5 y#15
		y#5 y#20
		y#10 y#15
		y#10 y#20
	700(1) - 735(1) y:
		y#5 y#23
		y#10 y#23
	701(1) - 722(1) y:
		y#6 y#15
		y#6 y#20
		y#11 y#15
		y#11 y#20
	701(1) - 735(1) y:
		y#6 y#23
		y#11 y#23
	709(1) - 717(1) y:
		y#12 y#13
		y#12 y#18
	709(1) - 719(1) y:
		y#12 y#14
		y#12 y#19
	709(1) - 722(1) y:
		y#12 y#15
		y#12 y#20
	709(1) - 726(1) y:
		y#12 y#16
		y#12 y#21
	709(1) - 727(1) y:
		y#12 y#17
		y#12 y#22
	709(1) - 735(1) y:
		y#12 y#23
Runtime Symex: 0.483224s
Adding SC constraints
Shared __CPROVER_threads_exited: 4R/3W
Shared __CPROVER_next_thread_id: 3R/3W
Shared x: 4R/5W
Shared y: 16R/7W
Shared b1: 2R/8W
Shared b2: 2R/8W
Shared X: 2R/3W
Shared main::1::t1!0@1: 2R/2W
Shared main::1::t2!0@1: 2R/2W
size of program expression: 682 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.00482635s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00361398s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.000834186s
Solving with Deagle's Closure solver
3810 variables, 12185 clauses
ClosureSolver finishes with 21 conflicts, 1602 decisions, and 5744 propagations. 24 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00172194s
Runtime decision procedure: 0.0160148s
Running propositional reduction
Solving with Deagle's Closure solver
3810 variables, 10227 clauses
ClosureSolver finishes with 21 conflicts, 2854 decisions, and 8713 propagations. 24 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000384787s
Runtime decision procedure: 0.000408457s
Running propositional reduction
Solving with Deagle's Closure solver
3810 variables, 10228 clauses
ClosureSolver finishes with 21 conflicts, 4096 decisions, and 11682 propagations. 24 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000382167s
Runtime decision procedure: 0.000403797s
Running propositional reduction
Solving with Deagle's Closure solver
3810 variables, 10229 clauses
ClosureSolver finishes with 21 conflicts, 5308 decisions, and 14651 propagations. 24 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000396527s
Runtime decision procedure: 0.000417817s
Running propositional reduction
Solving with Deagle's Closure solver
3810 variables, 10230 clauses
ClosureSolver finishes with 21 conflicts, 6499 decisions, and 17620 propagations. 24 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000375506s
Runtime decision procedure: 0.000396637s
Running propositional reduction
Solving with Deagle's Closure solver
3810 variables, 10231 clauses
ClosureSolver finishes with 21 conflicts, 7685 decisions, and 20589 propagations. 24 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000391127s
Runtime decision procedure: 0.000411667s
Running propositional reduction
Solving with Deagle's Closure solver
3810 variables, 10232 clauses
ClosureSolver finishes with 22 conflicts, 8893 decisions, and 23902 propagations. 24 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000380657s
Runtime decision procedure: 0.000400717s
Running propositional reduction
Solving with Deagle's Closure solver
3810 variables, 10233 clauses
ClosureSolver finishes with 22 conflicts, 10120 decisions, and 26871 propagations. 26 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000391127s
Runtime decision procedure: 0.000417418s
Running propositional reduction
Solving with Deagle's Closure solver
3810 variables, 10234 clauses
ClosureSolver finishes with 28 conflicts, 11513 decisions, and 30888 propagations. 32 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0005601s
Runtime decision procedure: 0.000581951s
Running propositional reduction
Solving with Deagle's Closure solver
3810 variables, 10235 clauses
ClosureSolver finishes with 28 conflicts, 12633 decisions, and 33857 propagations. 35 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000377116s
Runtime decision procedure: 0.000397127s
Running propositional reduction
Solving with Deagle's Closure solver
3810 variables, 10236 clauses
ClosureSolver finishes with 33 conflicts, 14190 decisions, and 38755 propagations. 35 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000631211s
Runtime decision procedure: 0.000652092s
Running propositional reduction
Solving with Deagle's Closure solver
3810 variables, 10237 clauses
ClosureSolver finishes with 35 conflicts, 15341 decisions, and 41814 propagations. 37 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000404747s
Runtime decision procedure: 0.000424637s
Running propositional reduction
Solving with Deagle's Closure solver
3810 variables, 10237 clauses
ClosureSolver finishes with 38 conflicts, 16560 decisions, and 44925 propagations. 37 theory propagations and 0 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000490859s
Runtime decision procedure: 0.00051016s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-atomic/lamport-b.i function main
[nodatarace.assertion.0] line 743 No data races on variable X between line 707 and line 733: FAILURE
[nodatarace.assertion.1] line 743 No data races on variable X between line 707 and line 734: FAILURE
[nodatarace.assertion.2] line 743 No data races on variable X between line 708 and line 733: FAILURE
[nodatarace.assertion.3] line 743 No data races on variable b1 between line 689 and line 725: FAILURE
[nodatarace.assertion.4] line 743 No data races on variable b1 between line 692 and line 725: FAILURE
[nodatarace.assertion.5] line 743 No data races on variable b1 between line 698 and line 725: FAILURE
[nodatarace.assertion.6] line 743 No data races on variable b1 between line 710 and line 725: FAILURE
[nodatarace.assertion.7] line 743 No data races on variable b2 between line 699 and line 715: FAILURE
[nodatarace.assertion.8] line 743 No data races on variable b2 between line 699 and line 718: FAILURE
[nodatarace.assertion.9] line 743 No data races on variable b2 between line 699 and line 724: FAILURE
[nodatarace.assertion.10] line 743 No data races on variable b2 between line 699 and line 736: FAILURE
[nodatarace.assertion.11] line 743 No data races on variable x between line 690 and line 716: FAILURE
[nodatarace.assertion.12] line 743 No data races on variable x between line 690 and line 723: FAILURE
[nodatarace.assertion.13] line 743 No data races on variable x between line 697 and line 716: FAILURE
[nodatarace.assertion.14] line 743 No data races on variable y between line 691 and line 722: FAILURE
[nodatarace.assertion.15] line 743 No data races on variable y between line 691 and line 735: FAILURE
[nodatarace.assertion.16] line 743 No data races on variable y between line 693 and line 722: FAILURE
[nodatarace.assertion.17] line 743 No data races on variable y between line 693 and line 735: FAILURE
[nodatarace.assertion.18] line 743 No data races on variable y between line 696 and line 717: FAILURE
[nodatarace.assertion.19] line 743 No data races on variable y between line 696 and line 719: FAILURE
[nodatarace.assertion.20] line 743 No data races on variable y between line 696 and line 722: FAILURE
[nodatarace.assertion.21] line 743 No data races on variable y between line 696 and line 726: FAILURE
[nodatarace.assertion.22] line 743 No data races on variable y between line 696 and line 727: FAILURE
[nodatarace.assertion.23] line 743 No data races on variable y between line 696 and line 735: FAILURE
[nodatarace.assertion.24] line 743 No data races on variable y between line 700 and line 722: FAILURE
[nodatarace.assertion.25] line 743 No data races on variable y between line 700 and line 735: FAILURE
[nodatarace.assertion.26] line 743 No data races on variable y between line 701 and line 722: FAILURE
[nodatarace.assertion.27] line 743 No data races on variable y between line 701 and line 735: FAILURE
[nodatarace.assertion.28] line 743 No data races on variable y between line 709 and line 717: FAILURE
[nodatarace.assertion.29] line 743 No data races on variable y between line 709 and line 719: FAILURE
[nodatarace.assertion.30] line 743 No data races on variable y between line 709 and line 722: FAILURE
[nodatarace.assertion.31] line 743 No data races on variable y between line 709 and line 726: FAILURE
[nodatarace.assertion.32] line 743 No data races on variable y between line 709 and line 727: FAILURE
[nodatarace.assertion.33] line 743 No data races on variable y between line 709 and line 735: FAILURE

** 34 of 34 failed (14 iterations)
VERIFICATION FAILED
