Counterexample: State 1 thread 0 ---------------------------------------------------- c::latch1$w_buff0_used=FALSE (0) State 2 thread 0 ---------------------------------------------------- c::latch1$w_buff1_used=FALSE (0) State 3 thread 0 ---------------------------------------------------- c::latch1$flush_delayed=FALSE (0) State 4 thread 0 ---------------------------------------------------- c::latch1$read_delayed=FALSE (0) State 5 thread 0 ---------------------------------------------------- c::latch1$read_delayed_var=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 6 thread 0 ---------------------------------------------------- c::latch1$r_buff0_thd0=FALSE (0) State 7 thread 0 ---------------------------------------------------- c::latch1$r_buff0_thd1=FALSE (0) State 8 thread 0 ---------------------------------------------------- c::latch1$r_buff0_thd2=FALSE (0) State 9 thread 0 ---------------------------------------------------- c::latch1$r_buff1_thd0=FALSE (0) State 10 thread 0 ---------------------------------------------------- c::latch1$r_buff1_thd1=FALSE (0) State 11 thread 0 ---------------------------------------------------- c::latch1$r_buff1_thd2=FALSE (0) State 12 thread 0 ---------------------------------------------------- c::flag1$w_buff0_used=FALSE (0) State 13 thread 0 ---------------------------------------------------- c::flag1$w_buff1_used=FALSE (0) State 14 thread 0 ---------------------------------------------------- c::flag1$flush_delayed=FALSE (0) State 15 thread 0 ---------------------------------------------------- c::flag1$read_delayed=FALSE (0) State 16 thread 0 ---------------------------------------------------- c::flag1$read_delayed_var=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 17 thread 0 ---------------------------------------------------- c::flag1$r_buff0_thd0=FALSE (0) State 18 thread 0 ---------------------------------------------------- c::flag1$r_buff0_thd1=FALSE (0) State 19 thread 0 ---------------------------------------------------- c::flag1$r_buff0_thd2=FALSE (0) State 20 thread 0 ---------------------------------------------------- c::flag1$r_buff1_thd0=FALSE (0) State 21 thread 0 ---------------------------------------------------- c::flag1$r_buff1_thd1=FALSE (0) State 22 thread 0 ---------------------------------------------------- c::flag1$r_buff1_thd2=FALSE (0) State 23 thread 0 ---------------------------------------------------- c::latch2$w_buff0_used=FALSE (0) State 24 thread 0 ---------------------------------------------------- c::latch2$w_buff1_used=FALSE (0) State 25 thread 0 ---------------------------------------------------- c::latch2$flush_delayed=FALSE (0) State 26 thread 0 ---------------------------------------------------- c::latch2$read_delayed=FALSE (0) State 27 thread 0 ---------------------------------------------------- c::latch2$read_delayed_var=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 28 thread 0 ---------------------------------------------------- c::latch2$r_buff0_thd0=FALSE (0) State 29 thread 0 ---------------------------------------------------- c::latch2$r_buff0_thd1=FALSE (0) State 30 thread 0 ---------------------------------------------------- c::latch2$r_buff0_thd2=FALSE (0) State 31 thread 0 ---------------------------------------------------- c::latch2$r_buff1_thd0=FALSE (0) State 32 thread 0 ---------------------------------------------------- c::latch2$r_buff1_thd1=FALSE (0) State 33 thread 0 ---------------------------------------------------- c::latch2$r_buff1_thd2=FALSE (0) State 34 thread 0 ---------------------------------------------------- c::flag2$w_buff0_used=FALSE (0) State 35 thread 0 ---------------------------------------------------- c::flag2$w_buff1_used=FALSE (0) State 36 thread 0 ---------------------------------------------------- c::flag2$flush_delayed=FALSE (0) State 37 thread 0 ---------------------------------------------------- c::flag2$read_delayed=FALSE (0) State 38 thread 0 ---------------------------------------------------- c::flag2$read_delayed_var=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 39 thread 0 ---------------------------------------------------- c::flag2$r_buff0_thd0=FALSE (0) State 40 thread 0 ---------------------------------------------------- c::flag2$r_buff0_thd1=FALSE (0) State 41 thread 0 ---------------------------------------------------- c::flag2$r_buff0_thd2=FALSE (0) State 42 thread 0 ---------------------------------------------------- c::flag2$r_buff1_thd0=FALSE (0) State 43 thread 0 ---------------------------------------------------- c::flag2$r_buff1_thd1=FALSE (0) State 44 thread 0 ---------------------------------------------------- c::flag2$r_buff1_thd2=FALSE (0) State 45 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$w_buff0_used=FALSE (0) State 46 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$w_buff1_used=FALSE (0) State 47 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$flush_delayed=FALSE (0) State 48 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$read_delayed=FALSE (0) State 49 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$read_delayed_var=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 50 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$r_buff0_thd0=FALSE (0) State 51 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$r_buff0_thd1=FALSE (0) State 52 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$r_buff0_thd2=FALSE (0) State 53 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$r_buff1_thd0=FALSE (0) State 54 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$r_buff1_thd1=FALSE (0) State 55 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$r_buff1_thd2=FALSE (0) State 56 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$w_buff0_used=FALSE (0) State 57 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$w_buff1_used=FALSE (0) State 58 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$flush_delayed=FALSE (0) State 59 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$read_delayed=FALSE (0) State 60 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$read_delayed_var=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 61 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$r_buff0_thd0=FALSE (0) State 62 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$r_buff0_thd1=FALSE (0) State 63 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$r_buff0_thd2=FALSE (0) State 64 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$r_buff1_thd0=FALSE (0) State 65 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$r_buff1_thd1=FALSE (0) State 66 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$r_buff1_thd2=FALSE (0) State 67 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$w_buff0_used=FALSE (0) State 68 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$w_buff1_used=FALSE (0) State 69 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$flush_delayed=FALSE (0) State 70 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$read_delayed=FALSE (0) State 71 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$read_delayed_var=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 72 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$r_buff0_thd0=FALSE (0) State 73 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$r_buff0_thd1=FALSE (0) State 74 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$r_buff0_thd2=FALSE (0) State 75 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$r_buff1_thd0=FALSE (0) State 76 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$r_buff1_thd1=FALSE (0) State 77 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$r_buff1_thd2=FALSE (0) State 78 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard3$w_buff0_used=FALSE (0) State 79 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard3$w_buff1_used=FALSE (0) State 80 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard3$flush_delayed=FALSE (0) State 81 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard3$read_delayed=FALSE (0) State 82 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard3$read_delayed_var=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 83 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard3$r_buff0_thd0=FALSE (0) State 84 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard3$r_buff0_thd1=FALSE (0) State 85 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard3$r_buff0_thd2=FALSE (0) State 86 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard3$r_buff1_thd0=FALSE (0) State 87 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard3$r_buff1_thd1=FALSE (0) State 88 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard3$r_buff1_thd2=FALSE (0) State 89 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard0$w_buff0_used=FALSE (0) State 90 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard0$w_buff1_used=FALSE (0) State 91 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard0$flush_delayed=FALSE (0) State 92 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard0$read_delayed=FALSE (0) State 93 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard0$read_delayed_var=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 94 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard0$r_buff0_thd0=FALSE (0) State 95 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard0$r_buff0_thd1=FALSE (0) State 96 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard0$r_buff0_thd2=FALSE (0) State 97 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard0$r_buff1_thd0=FALSE (0) State 98 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard0$r_buff1_thd1=FALSE (0) State 99 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard0$r_buff1_thd2=FALSE (0) State 100 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard1$w_buff0_used=FALSE (0) State 101 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard1$w_buff1_used=FALSE (0) State 102 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard1$flush_delayed=FALSE (0) State 103 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard1$read_delayed=FALSE (0) State 104 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard1$read_delayed_var=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 105 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard1$r_buff0_thd0=FALSE (0) State 106 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard1$r_buff0_thd1=FALSE (0) State 107 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard1$r_buff0_thd2=FALSE (0) State 108 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard1$r_buff1_thd0=FALSE (0) State 109 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard1$r_buff1_thd1=FALSE (0) State 110 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard1$r_buff1_thd2=FALSE (0) State 111 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard2$w_buff0_used=FALSE (0) State 112 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard2$w_buff1_used=FALSE (0) State 113 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard2$flush_delayed=FALSE (0) State 114 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard2$read_delayed=FALSE (0) State 115 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard2$read_delayed_var=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 116 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard2$r_buff0_thd0=FALSE (0) State 117 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard2$r_buff0_thd1=FALSE (0) State 118 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard2$r_buff0_thd2=FALSE (0) State 119 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard2$r_buff1_thd0=FALSE (0) State 120 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard2$r_buff1_thd1=FALSE (0) State 121 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard2$r_buff1_thd2=FALSE (0) State 122 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard3$w_buff0_used=FALSE (0) State 123 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard3$w_buff1_used=FALSE (0) State 124 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard3$flush_delayed=FALSE (0) State 125 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard3$read_delayed=FALSE (0) State 126 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard3$read_delayed_var=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 127 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard3$r_buff0_thd0=FALSE (0) State 128 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard3$r_buff0_thd1=FALSE (0) State 129 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard3$r_buff0_thd2=FALSE (0) State 130 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard3$r_buff1_thd0=FALSE (0) State 131 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard3$r_buff1_thd1=FALSE (0) State 132 thread 0 ---------------------------------------------------- c::worker_2$tmp_guard3$r_buff1_thd2=FALSE (0) State 134 file line 26 thread 0 ---------------------------------------------------- __CPROVER_deallocated=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 135 file line 27 thread 0 ---------------------------------------------------- __CPROVER_malloc_object=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 136 file line 28 thread 0 ---------------------------------------------------- __CPROVER_malloc_size=0 (0000000000000000000000000000000000000000000000000000000000000000) State 137 file line 29 thread 0 ---------------------------------------------------- __CPROVER_malloc_is_new_array=FALSE (0) State 138 file line 38 thread 0 ---------------------------------------------------- __CPROVER_rounding_mode=0 (00000000000000000000000000000000) State 139 file pgsql_two.c line 6 thread 0 ---------------------------------------------------- latch1=TRUE (1) State 140 file pgsql_two.c line 7 thread 0 ---------------------------------------------------- flag1=TRUE (1) State 141 file pgsql_two.c line 8 thread 0 ---------------------------------------------------- latch2=FALSE (0) State 142 file pgsql_two.c line 8 thread 0 ---------------------------------------------------- flag2=FALSE (0) State 151 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- arg=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 152 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- arg=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 154 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- weak::choice0=FALSE (0) State 155 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- weak::choice2=FALSE (0) State 156 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::latch1$flush_delayed=FALSE (0) State 157 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::latch1$mem_tmp=TRUE (1) State 158 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- latch1=TRUE (1) State 159 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::latch1$w_buff0=FALSE (0) State 160 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::latch1$w_buff1=FALSE (0) State 161 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::latch1$w_buff0_used=FALSE (0) State 162 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::latch1$w_buff1_used=FALSE (0) State 163 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::latch1$r_buff0_thd1=FALSE (0) State 164 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::latch1$r_buff1_thd1=FALSE (0) State 165 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- $tmp_guard=TRUE (1) State 166 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$w_buff0_used=FALSE (0) State 167 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$w_buff1_used=FALSE (0) State 168 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$r_buff0_thd0=FALSE (0) State 169 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$r_buff1_thd0=FALSE (0) State 170 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$r_buff0_thd1=FALSE (0) State 171 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$r_buff1_thd1=FALSE (0) State 172 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$r_buff0_thd2=FALSE (0) State 173 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard0$r_buff1_thd2=FALSE (0) State 174 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- latch1=TRUE (1) State 175 file pgsql_two.c line 42 function worker_1 thread 0 ---------------------------------------------------- c::latch1$flush_delayed=FALSE (0) State 179 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- weak::choice0=FALSE (0) State 180 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- weak::choice2=FALSE (0) State 181 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::flag1$flush_delayed=FALSE (0) State 182 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::flag1$mem_tmp=TRUE (1) State 183 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- flag1=TRUE (1) State 184 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::flag1$w_buff0=FALSE (0) State 185 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::flag1$w_buff1=FALSE (0) State 186 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::flag1$w_buff0_used=FALSE (0) State 187 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::flag1$w_buff1_used=FALSE (0) State 188 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::flag1$r_buff0_thd1=FALSE (0) State 189 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::flag1$r_buff1_thd1=FALSE (0) State 190 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- weak::choice0=FALSE (0) State 191 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- weak::choice2=FALSE (0) State 192 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::latch1$flush_delayed=FALSE (0) State 193 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::latch1$mem_tmp=TRUE (1) State 194 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- latch1=TRUE (1) State 195 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::latch1$w_buff0=FALSE (0) State 196 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::latch1$w_buff1=FALSE (0) State 197 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::latch1$w_buff0_used=FALSE (0) State 198 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::latch1$w_buff1_used=FALSE (0) State 199 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::latch1$r_buff0_thd1=FALSE (0) State 200 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::latch1$r_buff1_thd1=FALSE (0) State 201 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- $tmp_guard=TRUE (1) State 202 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$w_buff0_used=FALSE (0) State 203 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$w_buff1_used=FALSE (0) State 204 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$r_buff0_thd0=FALSE (0) State 205 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$r_buff1_thd0=FALSE (0) State 206 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$r_buff0_thd1=FALSE (0) State 207 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$r_buff1_thd1=FALSE (0) State 208 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$r_buff0_thd2=FALSE (0) State 209 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard1$r_buff1_thd2=FALSE (0) State 210 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- flag1=TRUE (1) State 211 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::flag1$flush_delayed=FALSE (0) State 212 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- latch1=TRUE (1) State 213 file pgsql_two.c line 45 function worker_1 thread 0 ---------------------------------------------------- c::latch1$flush_delayed=FALSE (0) State 217 file pgsql_two.c line 46 function worker_1 thread 0 ---------------------------------------------------- latch1=FALSE (0) State 218 file pgsql_two.c line 46 function worker_1 thread 0 ---------------------------------------------------- c::latch1$w_buff0_used=FALSE (0) State 219 file pgsql_two.c line 46 function worker_1 thread 0 ---------------------------------------------------- c::latch1$w_buff1_used=FALSE (0) State 220 file pgsql_two.c line 46 function worker_1 thread 0 ---------------------------------------------------- c::latch1$r_buff0_thd0=FALSE (0) State 221 file pgsql_two.c line 46 function worker_1 thread 0 ---------------------------------------------------- c::latch1$r_buff1_thd0=FALSE (0) State 222 file pgsql_two.c line 46 function worker_1 thread 0 ---------------------------------------------------- c::latch1$r_buff0_thd1=FALSE (0) State 223 file pgsql_two.c line 46 function worker_1 thread 0 ---------------------------------------------------- c::latch1$r_buff1_thd1=FALSE (0) State 224 file pgsql_two.c line 46 function worker_1 thread 0 ---------------------------------------------------- c::latch1$r_buff0_thd2=FALSE (0) State 225 file pgsql_two.c line 46 function worker_1 thread 0 ---------------------------------------------------- c::latch1$r_buff1_thd2=FALSE (0) State 228 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- weak::choice0=FALSE (0) State 229 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- weak::choice2=FALSE (0) State 230 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::flag1$flush_delayed=FALSE (0) State 231 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::flag1$mem_tmp=TRUE (1) State 232 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- weak::choice1=FALSE (0) State 233 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- flag1=TRUE (1) State 234 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::flag1$w_buff0=FALSE (0) State 235 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::flag1$w_buff1=FALSE (0) State 236 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::flag1$w_buff0_used=FALSE (0) State 237 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::flag1$w_buff1_used=FALSE (0) State 238 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::flag1$r_buff0_thd1=FALSE (0) State 239 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::flag1$r_buff1_thd1=FALSE (0) State 240 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$read_delayed=TRUE (1) State 241 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$read_delayed_var=&flag1 (0000001000000000000000000000000000000000000000000000000000000000) State 242 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- $tmp_guard=FALSE (0) State 243 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$w_buff0_used=FALSE (0) State 244 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$w_buff1_used=FALSE (0) State 245 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$r_buff0_thd0=FALSE (0) State 246 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$r_buff1_thd0=FALSE (0) State 247 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$r_buff0_thd1=FALSE (0) State 248 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$r_buff1_thd1=FALSE (0) State 249 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$r_buff0_thd2=FALSE (0) State 250 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::worker_1$tmp_guard2$r_buff1_thd2=FALSE (0) State 251 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- flag1=TRUE (1) State 252 file pgsql_two.c line 47 function worker_1 thread 0 ---------------------------------------------------- c::flag1$flush_delayed=FALSE (0) State 256 file pgsql_two.c line 49 function worker_1 thread 0 ---------------------------------------------------- c::flag1$w_buff1=FALSE (0) State 257 file pgsql_two.c line 49 function worker_1 thread 0 ---------------------------------------------------- c::flag1$w_buff0=FALSE (0) State 258 file pgsql_two.c line 49 function worker_1 thread 0 ---------------------------------------------------- c::flag1$w_buff1_used=FALSE (0) State 259 file pgsql_two.c line 49 function worker_1 thread 0 ---------------------------------------------------- c::flag1$w_buff0_used=TRUE (1) State 261 file pgsql_two.c line 49 function worker_1 thread 0 ---------------------------------------------------- c::flag1$r_buff1_thd0=FALSE (0) State 262 file pgsql_two.c line 49 function worker_1 thread 0 ---------------------------------------------------- c::flag1$r_buff1_thd1=FALSE (0) State 263 file pgsql_two.c line 49 function worker_1 thread 0 ---------------------------------------------------- c::flag1$r_buff1_thd2=FALSE (0) State 264 file pgsql_two.c line 49 function worker_1 thread 0 ---------------------------------------------------- c::flag1$r_buff0_thd1=TRUE (1) State 267 file pgsql_two.c line 50 function worker_1 thread 0 ---------------------------------------------------- c::flag2$w_buff1=FALSE (0) State 268 file pgsql_two.c line 50 function worker_1 thread 0 ---------------------------------------------------- c::flag2$w_buff0=TRUE (1) State 269 file pgsql_two.c line 50 function worker_1 thread 0 ---------------------------------------------------- c::flag2$w_buff1_used=FALSE (0) State 270 file pgsql_two.c line 50 function worker_1 thread 0 ---------------------------------------------------- c::flag2$w_buff0_used=TRUE (1) State 272 file pgsql_two.c line 50 function worker_1 thread 0 ---------------------------------------------------- c::flag2$r_buff1_thd0=FALSE (0) State 273 file pgsql_two.c line 50 function worker_1 thread 0 ---------------------------------------------------- c::flag2$r_buff1_thd1=FALSE (0) State 274 file pgsql_two.c line 50 function worker_1 thread 0 ---------------------------------------------------- c::flag2$r_buff1_thd2=FALSE (0) State 275 file pgsql_two.c line 50 function worker_1 thread 0 ---------------------------------------------------- c::flag2$r_buff0_thd1=TRUE (1) State 278 file pgsql_two.c line 51 function worker_1 thread 0 ---------------------------------------------------- latch2=TRUE (1) State 279 file pgsql_two.c line 51 function worker_1 thread 0 ---------------------------------------------------- c::latch2$w_buff0_used=FALSE (0) State 280 file pgsql_two.c line 51 function worker_1 thread 0 ---------------------------------------------------- c::latch2$w_buff1_used=FALSE (0) State 281 file pgsql_two.c line 51 function worker_1 thread 0 ---------------------------------------------------- c::latch2$r_buff0_thd0=FALSE (0) State 282 file pgsql_two.c line 51 function worker_1 thread 0 ---------------------------------------------------- c::latch2$r_buff1_thd0=FALSE (0) State 283 file pgsql_two.c line 51 function worker_1 thread 0 ---------------------------------------------------- c::latch2$r_buff0_thd1=FALSE (0) State 284 file pgsql_two.c line 51 function worker_1 thread 0 ---------------------------------------------------- c::latch2$r_buff1_thd1=FALSE (0) State 285 file pgsql_two.c line 51 function worker_1 thread 0 ---------------------------------------------------- c::latch2$r_buff0_thd2=FALSE (0) State 286 file pgsql_two.c line 51 function worker_1 thread 0 ---------------------------------------------------- c::latch2$r_buff1_thd2=FALSE (0) State 289 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- weak::choice0=FALSE (0) State 290 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- weak::choice2=FALSE (0) State 291 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::latch2$flush_delayed=FALSE (0) State 292 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::latch2$mem_tmp=TRUE (1) State 293 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- latch2=TRUE (1) State 294 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::latch2$w_buff0=FALSE (0) State 295 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::latch2$w_buff1=FALSE (0) State 296 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::latch2$w_buff0_used=FALSE (0) State 297 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::latch2$w_buff1_used=FALSE (0) State 298 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::latch2$r_buff0_thd2=FALSE (0) State 299 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::latch2$r_buff1_thd2=FALSE (0) State 300 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- $tmp_guard=TRUE (1) State 301 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard0$w_buff0_used=FALSE (0) State 302 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard0$w_buff1_used=FALSE (0) State 303 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard0$r_buff0_thd0=FALSE (0) State 304 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard0$r_buff1_thd0=FALSE (0) State 305 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard0$r_buff0_thd1=FALSE (0) State 306 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard0$r_buff1_thd1=FALSE (0) State 307 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard0$r_buff0_thd2=FALSE (0) State 308 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard0$r_buff1_thd2=FALSE (0) State 309 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- latch2=TRUE (1) State 310 file pgsql_two.c line 60 function worker_2 thread 1 ---------------------------------------------------- c::latch2$flush_delayed=FALSE (0) State 314 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- weak::choice0=FALSE (0) State 315 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- weak::choice2=FALSE (0) State 316 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::latch2$flush_delayed=FALSE (0) State 317 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::latch2$mem_tmp=TRUE (1) State 318 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- latch2=TRUE (1) State 319 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::latch2$w_buff0=FALSE (0) State 320 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::latch2$w_buff1=FALSE (0) State 321 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::latch2$w_buff0_used=FALSE (0) State 322 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::latch2$w_buff1_used=FALSE (0) State 323 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::latch2$r_buff0_thd2=FALSE (0) State 324 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::latch2$r_buff1_thd2=FALSE (0) State 325 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- weak::choice0=FALSE (0) State 326 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- weak::choice2=FALSE (0) State 327 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::flag2$flush_delayed=FALSE (0) State 328 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::flag2$mem_tmp=FALSE (0) State 329 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- flag2=FALSE (0) State 330 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::flag2$w_buff0=TRUE (1) State 331 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::flag2$w_buff1=FALSE (0) State 332 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::flag2$w_buff0_used=TRUE (1) State 333 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::flag2$w_buff1_used=FALSE (0) State 334 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::flag2$r_buff0_thd2=FALSE (0) State 335 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::flag2$r_buff1_thd2=FALSE (0) State 336 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- $tmp_guard=FALSE (0) State 337 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard1$w_buff0_used=FALSE (0) State 338 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard1$w_buff1_used=FALSE (0) State 339 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard1$r_buff0_thd0=FALSE (0) State 340 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard1$r_buff1_thd0=FALSE (0) State 341 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard1$r_buff0_thd1=FALSE (0) State 342 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard1$r_buff1_thd1=FALSE (0) State 343 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard1$r_buff0_thd2=FALSE (0) State 344 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::worker_2$tmp_guard1$r_buff1_thd2=FALSE (0) State 345 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- latch2=TRUE (1) State 346 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::latch2$flush_delayed=FALSE (0) State 347 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- flag2=FALSE (0) State 348 file pgsql_two.c line 63 function worker_2 thread 1 ---------------------------------------------------- c::flag2$flush_delayed=FALSE (0) Violated property: file pgsql_two.c line 63 function worker_2 assertion $tmp_guard VERIFICATION FAILED 24.32