CBMC version 5.0 64-bit linux Parsing fake.c Converting Type-checking fake Generating GOTO Program Adding CPROVER library Function Pointer Removal Partial Inlining Generic Property Instrumentation Starting Bounded Model Checking Adding SC constraints size of program expression: 14627 steps no slicing due to threads Generated 9 VCC(s), 9 remaining after simplification Passing problem to propositional reduction Running propositional reduction Post-processing Solving with MiniSAT 2.2.0 with simplifier 113947 variables, 501366 clauses SAT checker: negated claim is SATISFIABLE, i.e., does not hold Runtime decision procedure: 19.991s Building error trace Counterexample: State 32 thread 0 ---------------------------------------------------- argv'[268435456]=irep("(\"nil\")")[268435456] (?) State 35 file fake.c line 179 thread 0 ---------------------------------------------------- argc=268435456 (00010000000000000000000000000000) State 36 file fake.c line 179 thread 0 ---------------------------------------------------- argv=argv' (0000010000000000000000000000000000000000000000000000000000000000) State 37 file fake.c line 181 function main thread 0 ---------------------------------------------------- tu=0 (0000000000000000000000000000000000000000000000000000000000000000) State 38 file fake.c line 182 function main thread 0 ---------------------------------------------------- tpr=0 (0000000000000000000000000000000000000000000000000000000000000000) State 41 file tiny.c line 86 function rcu_idle_enter thread 0 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 42 file tiny.c line 87 function rcu_idle_enter thread 0 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 45 file tiny.c line 89 function rcu_idle_enter thread 0 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 48 file fake.c line 97 function local_irq_save thread 0 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 51 file fake.c line 99 function local_irq_save thread 0 ---------------------------------------------------- irq_lock=1 (00000000000000000000000000000001) State 59 file tiny.c line 93 function rcu_idle_enter thread 0 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 63 file tiny.c line 96 function rcu_idle_enter thread 0 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 68 file tiny.c line 222 function rcu_sched_qs thread 0 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 71 file tiny.c line 224 function rcu_sched_qs thread 0 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 74 file fake.c line 97 function local_irq_save thread 0 ---------------------------------------------------- local_irq_depth=2 (00000000000000000000000000000010) State 80 file tiny.c line 225 function rcu_sched_qs thread 0 ---------------------------------------------------- rcp=&rcu_sched_ctrlblk.rcucblist (0000001000000000000000000000000000000000000000000000000000000000) State 89 file tiny.c line 226 function rcu_sched_qs thread 0 ---------------------------------------------------- rcp=&rcu_bh_ctrlblk.rcucblist (0000001100000000000000000000000000000000000000000000000000000000) State 98 file tiny.c line 228 function rcu_sched_qs thread 0 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 99 file fake.c line 110 function local_irq_restore thread 0 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 103 file tiny.c line 77 function rcu_idle_enter_common thread 0 ---------------------------------------------------- rcu_dynticks_nesting=0 (0000000000000000000000000000000000000000000000000000000000000000) State 107 file tiny.c line 97 function rcu_idle_enter thread 0 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 108 file fake.c line 110 function local_irq_restore thread 0 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 109 file fake.c line 112 function local_irq_restore thread 0 ---------------------------------------------------- irq_lock=0 (00000000000000000000000000000000) State 202 file fake.c line 63 function fake_acquire_cpu thread 2 ---------------------------------------------------- cpu_lock=1 (00000000000000000000000000000001) State 207 file tiny.c line 143 function rcu_idle_exit thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 208 file tiny.c line 144 function rcu_idle_exit thread 2 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 211 file tiny.c line 146 function rcu_idle_exit thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 214 file fake.c line 97 function local_irq_save thread 2 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 217 file fake.c line 99 function local_irq_save thread 2 ---------------------------------------------------- irq_lock=1 (00000000000000000000000000000001) State 221 file tiny.c line 147 function rcu_idle_exit thread 2 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 229 file tiny.c line 152 function rcu_idle_exit thread 2 ---------------------------------------------------- rcu_dynticks_nesting=90071992547409920 (0000000101000000000000000000000000000000000000000000000000000000) State 232 file tiny.c line 153 function rcu_idle_exit thread 2 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 238 file tiny.c line 154 function rcu_idle_exit thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 239 file fake.c line 110 function local_irq_restore thread 2 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 240 file fake.c line 112 function local_irq_restore thread 2 ---------------------------------------------------- irq_lock=0 (00000000000000000000000000000000) State 251 file fake.c line 134 function rcu_reader thread 2 ---------------------------------------------------- __unbuffered_tpr_x=0 (00000000000000000000000000000000) State 262 file tiny.c line 86 function rcu_idle_enter thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 263 file tiny.c line 87 function rcu_idle_enter thread 2 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 266 file tiny.c line 89 function rcu_idle_enter thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 269 file fake.c line 97 function local_irq_save thread 2 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 272 file fake.c line 99 function local_irq_save thread 2 ---------------------------------------------------- irq_lock=1 (00000000000000000000000000000001) State 283 file tiny.c line 93 function rcu_idle_enter thread 2 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 287 file tiny.c line 96 function rcu_idle_enter thread 2 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 292 file tiny.c line 222 function rcu_sched_qs thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 295 file tiny.c line 224 function rcu_sched_qs thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 298 file fake.c line 97 function local_irq_save thread 2 ---------------------------------------------------- local_irq_depth=2 (00000000000000000000000000000010) State 304 file tiny.c line 225 function rcu_sched_qs thread 2 ---------------------------------------------------- rcp=&rcu_sched_ctrlblk.rcucblist (0000001000000000000000000000000000000000000000000000000000000000) State 313 file tiny.c line 226 function rcu_sched_qs thread 2 ---------------------------------------------------- rcp=&rcu_bh_ctrlblk.rcucblist (0000001100000000000000000000000000000000000000000000000000000000) State 322 file tiny.c line 228 function rcu_sched_qs thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 323 file fake.c line 110 function local_irq_restore thread 2 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 327 file tiny.c line 77 function rcu_idle_enter_common thread 2 ---------------------------------------------------- rcu_dynticks_nesting=0 (0000000000000000000000000000000000000000000000000000000000000000) State 331 file tiny.c line 97 function rcu_idle_enter thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 332 file fake.c line 110 function local_irq_restore thread 2 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 333 file fake.c line 112 function local_irq_restore thread 2 ---------------------------------------------------- irq_lock=0 (00000000000000000000000000000000) State 337 file fake.c line 76 function fake_release_cpu thread 2 ---------------------------------------------------- cpu_lock=0 (00000000000000000000000000000000) State 345 file fake.c line 63 function fake_acquire_cpu thread 1 ---------------------------------------------------- cpu_lock=1 (00000000000000000000000000000001) State 350 file tiny.c line 143 function rcu_idle_exit thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 351 file tiny.c line 144 function rcu_idle_exit thread 1 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 354 file tiny.c line 146 function rcu_idle_exit thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 357 file fake.c line 97 function local_irq_save thread 1 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 360 file fake.c line 99 function local_irq_save thread 1 ---------------------------------------------------- irq_lock=1 (00000000000000000000000000000001) State 364 file tiny.c line 147 function rcu_idle_exit thread 1 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 372 file tiny.c line 152 function rcu_idle_exit thread 1 ---------------------------------------------------- rcu_dynticks_nesting=90071992547409920 (0000000101000000000000000000000000000000000000000000000000000000) State 375 file tiny.c line 153 function rcu_idle_exit thread 1 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 381 file tiny.c line 154 function rcu_idle_exit thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 382 file fake.c line 110 function local_irq_restore thread 1 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 383 file fake.c line 112 function local_irq_restore thread 1 ---------------------------------------------------- irq_lock=0 (00000000000000000000000000000000) State 388 file fake.c line 148 function thread_update thread 1 ---------------------------------------------------- x=1 (00000000000000000000000000000001) State 398 file tiny.c line 86 function rcu_idle_enter thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 399 file tiny.c line 87 function rcu_idle_enter thread 1 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 402 file tiny.c line 89 function rcu_idle_enter thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 405 file fake.c line 97 function local_irq_save thread 1 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 408 file fake.c line 99 function local_irq_save thread 1 ---------------------------------------------------- irq_lock=1 (00000000000000000000000000000001) State 419 file tiny.c line 93 function rcu_idle_enter thread 1 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 423 file tiny.c line 96 function rcu_idle_enter thread 1 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 428 file tiny.c line 222 function rcu_sched_qs thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 431 file tiny.c line 224 function rcu_sched_qs thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 434 file fake.c line 97 function local_irq_save thread 1 ---------------------------------------------------- local_irq_depth=2 (00000000000000000000000000000010) State 440 file tiny.c line 225 function rcu_sched_qs thread 1 ---------------------------------------------------- rcp=&rcu_sched_ctrlblk.rcucblist (0000001000000000000000000000000000000000000000000000000000000000) State 449 file tiny.c line 226 function rcu_sched_qs thread 1 ---------------------------------------------------- rcp=&rcu_bh_ctrlblk.rcucblist (0000001100000000000000000000000000000000000000000000000000000000) State 461 file tiny.c line 228 function rcu_sched_qs thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 462 file fake.c line 110 function local_irq_restore thread 1 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 466 file tiny.c line 77 function rcu_idle_enter_common thread 1 ---------------------------------------------------- rcu_dynticks_nesting=0 (0000000000000000000000000000000000000000000000000000000000000000) State 470 file tiny.c line 97 function rcu_idle_enter thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 471 file fake.c line 110 function local_irq_restore thread 1 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 472 file fake.c line 112 function local_irq_restore thread 1 ---------------------------------------------------- irq_lock=0 (00000000000000000000000000000000) State 476 file fake.c line 76 function fake_release_cpu thread 1 ---------------------------------------------------- cpu_lock=0 (00000000000000000000000000000000) State 484 file fake.c line 63 function fake_acquire_cpu thread 1 ---------------------------------------------------- cpu_lock=1 (00000000000000000000000000000001) State 489 file tiny.c line 143 function rcu_idle_exit thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 490 file tiny.c line 144 function rcu_idle_exit thread 1 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 493 file tiny.c line 146 function rcu_idle_exit thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 496 file fake.c line 97 function local_irq_save thread 1 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 499 file fake.c line 99 function local_irq_save thread 1 ---------------------------------------------------- irq_lock=1 (00000000000000000000000000000001) State 503 file tiny.c line 147 function rcu_idle_exit thread 1 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 511 file tiny.c line 152 function rcu_idle_exit thread 1 ---------------------------------------------------- rcu_dynticks_nesting=90071992547409920 (0000000101000000000000000000000000000000000000000000000000000000) State 514 file tiny.c line 153 function rcu_idle_exit thread 1 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 520 file tiny.c line 154 function rcu_idle_exit thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 521 file fake.c line 110 function local_irq_restore thread 1 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 522 file fake.c line 112 function local_irq_restore thread 1 ---------------------------------------------------- irq_lock=0 (00000000000000000000000000000000) State 530 file fake.c line 152 function thread_update thread 1 ---------------------------------------------------- y=1 (00000000000000000000000000000001) State 535 file tiny.c line 86 function rcu_idle_enter thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 536 file tiny.c line 87 function rcu_idle_enter thread 1 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 539 file tiny.c line 89 function rcu_idle_enter thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 542 file fake.c line 97 function local_irq_save thread 1 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 545 file fake.c line 99 function local_irq_save thread 1 ---------------------------------------------------- irq_lock=1 (00000000000000000000000000000001) State 556 file tiny.c line 93 function rcu_idle_enter thread 1 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 560 file tiny.c line 96 function rcu_idle_enter thread 1 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 565 file tiny.c line 222 function rcu_sched_qs thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 568 file tiny.c line 224 function rcu_sched_qs thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 571 file fake.c line 97 function local_irq_save thread 1 ---------------------------------------------------- local_irq_depth=2 (00000000000000000000000000000010) State 577 file tiny.c line 225 function rcu_sched_qs thread 1 ---------------------------------------------------- rcp=&rcu_sched_ctrlblk.rcucblist (0000001000000000000000000000000000000000000000000000000000000000) State 586 file tiny.c line 226 function rcu_sched_qs thread 1 ---------------------------------------------------- rcp=&rcu_bh_ctrlblk.rcucblist (0000001100000000000000000000000000000000000000000000000000000000) State 595 file tiny.c line 228 function rcu_sched_qs thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 596 file fake.c line 110 function local_irq_restore thread 1 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 600 file tiny.c line 77 function rcu_idle_enter_common thread 1 ---------------------------------------------------- rcu_dynticks_nesting=0 (0000000000000000000000000000000000000000000000000000000000000000) State 604 file tiny.c line 97 function rcu_idle_enter thread 1 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 605 file fake.c line 110 function local_irq_restore thread 1 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 606 file fake.c line 112 function local_irq_restore thread 1 ---------------------------------------------------- irq_lock=0 (00000000000000000000000000000000) State 610 file fake.c line 76 function fake_release_cpu thread 1 ---------------------------------------------------- cpu_lock=0 (00000000000000000000000000000000) State 620 file fake.c line 63 function fake_acquire_cpu thread 2 ---------------------------------------------------- cpu_lock=1 (00000000000000000000000000000001) State 625 file tiny.c line 143 function rcu_idle_exit thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 626 file tiny.c line 144 function rcu_idle_exit thread 2 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 629 file tiny.c line 146 function rcu_idle_exit thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 632 file fake.c line 97 function local_irq_save thread 2 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 635 file fake.c line 99 function local_irq_save thread 2 ---------------------------------------------------- irq_lock=1 (00000000000000000000000000000001) State 639 file tiny.c line 147 function rcu_idle_exit thread 2 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 647 file tiny.c line 152 function rcu_idle_exit thread 2 ---------------------------------------------------- rcu_dynticks_nesting=90071992547409920 (0000000101000000000000000000000000000000000000000000000000000000) State 650 file tiny.c line 153 function rcu_idle_exit thread 2 ---------------------------------------------------- oldval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 656 file tiny.c line 154 function rcu_idle_exit thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 657 file fake.c line 110 function local_irq_restore thread 2 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 658 file fake.c line 112 function local_irq_restore thread 2 ---------------------------------------------------- irq_lock=0 (00000000000000000000000000000000) State 668 file fake.c line 140 function rcu_reader thread 2 ---------------------------------------------------- __unbuffered_tpr_y=1 (00000000000000000000000000000001) State 678 file tiny.c line 86 function rcu_idle_enter thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 679 file tiny.c line 87 function rcu_idle_enter thread 2 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 682 file tiny.c line 89 function rcu_idle_enter thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 685 file fake.c line 97 function local_irq_save thread 2 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 688 file fake.c line 99 function local_irq_save thread 2 ---------------------------------------------------- irq_lock=1 (00000000000000000000000000000001) State 699 file tiny.c line 93 function rcu_idle_enter thread 2 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 703 file tiny.c line 96 function rcu_idle_enter thread 2 ---------------------------------------------------- newval=0 (0000000000000000000000000000000000000000000000000000000000000000) State 708 file tiny.c line 222 function rcu_sched_qs thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 711 file tiny.c line 224 function rcu_sched_qs thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 714 file fake.c line 97 function local_irq_save thread 2 ---------------------------------------------------- local_irq_depth=2 (00000000000000000000000000000010) State 720 file tiny.c line 225 function rcu_sched_qs thread 2 ---------------------------------------------------- rcp=&rcu_sched_ctrlblk.rcucblist (0000001000000000000000000000000000000000000000000000000000000000) State 729 file tiny.c line 226 function rcu_sched_qs thread 2 ---------------------------------------------------- rcp=&rcu_bh_ctrlblk.rcucblist (0000001100000000000000000000000000000000000000000000000000000000) State 738 file tiny.c line 228 function rcu_sched_qs thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 739 file fake.c line 110 function local_irq_restore thread 2 ---------------------------------------------------- local_irq_depth=1 (00000000000000000000000000000001) State 743 file tiny.c line 77 function rcu_idle_enter_common thread 2 ---------------------------------------------------- rcu_dynticks_nesting=0 (0000000000000000000000000000000000000000000000000000000000000000) State 747 file tiny.c line 97 function rcu_idle_enter thread 2 ---------------------------------------------------- flags=0 (0000000000000000000000000000000000000000000000000000000000000000) State 748 file fake.c line 110 function local_irq_restore thread 2 ---------------------------------------------------- local_irq_depth=0 (00000000000000000000000000000000) State 749 file fake.c line 112 function local_irq_restore thread 2 ---------------------------------------------------- irq_lock=0 (00000000000000000000000000000000) State 758 file -pthread_create line 20 function __actual_thread_spawn thread 2 ---------------------------------------------------- arg=NULL (0000000000000000000000000000000000000000000000000000000000000000) State 762 file fake.c line 76 function fake_release_cpu thread 2 ---------------------------------------------------- cpu_lock=0 (00000000000000000000000000000000) Violated property: file fake.c line 193 function main assertion __unbuffered_tpr_y == 0 || __unbuffered_tpr_x == 1 || ({ __sync_synchronize(); noassert; }) FALSE VERIFICATION FAILED real 0m21.630s user 0m21.349s sys 0m0.263s