TEXT   185
CBMC version 5 5 64 bit x86 64 linux Parsing
Guest on 23rd December 2024 02:16:34 AM


  1. CBMC version 5.5 64-bit x86_64 linux
  2. Parsing CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c
  3. Converting
  4. Type-checking _cs_27_Boop_simple_vf_false-unreach-call
  5. Generating GOTO Program
  6. Adding CPROVER library (x86_64)
  7. Removal of function pointers and virtual functions
  8. Partial Inlining
  9. Generic Property Instrumentation
  10. Starting Bounded Model Checking
  11. Unwinding loop thr1.0 iteration 1 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 292 function thr1 thread 0
  12. Unwinding loop thr1.0 iteration 2 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 292 function thr1 thread 0
  13. Unwinding loop thr1.0 iteration 3 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 292 function thr1 thread 0
  14. Unwinding loop thr1.0 iteration 4 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 292 function thr1 thread 0
  15. Unwinding loop thr1.0 iteration 5 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 292 function thr1 thread 0
  16. Unwinding loop thr1.0 iteration 6 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 292 function thr1 thread 0
  17. Unwinding loop thr1.0 iteration 7 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 292 function thr1 thread 0
  18. Unwinding loop thr1.0 iteration 8 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 292 function thr1 thread 0
  19. Unwinding loop thr1.0 iteration 9 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 292 function thr1 thread 0
  20. Not unwinding loop thr1.0 iteration 10 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 292 function thr1 thread 0
  21. Unwinding loop thr1.1 iteration 1 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 333 function thr1 thread 0
  22. Unwinding loop thr1.1 iteration 2 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 333 function thr1 thread 0
  23. Unwinding loop thr1.1 iteration 3 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 333 function thr1 thread 0
  24. Unwinding loop thr1.1 iteration 4 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 333 function thr1 thread 0
  25. Unwinding loop thr1.1 iteration 5 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 333 function thr1 thread 0
  26. Unwinding loop thr1.1 iteration 6 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 333 function thr1 thread 0
  27. Unwinding loop thr1.1 iteration 7 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 333 function thr1 thread 0
  28. Unwinding loop thr1.1 iteration 8 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 333 function thr1 thread 0
  29. Unwinding loop thr1.1 iteration 9 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 333 function thr1 thread 0
  30. Not unwinding loop thr1.1 iteration 10 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 333 function thr1 thread 0
  31. Unwinding loop thr2.0 iteration 1 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  32. Unwinding loop thr2.0 iteration 2 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  33. Unwinding loop thr2.0 iteration 3 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  34. Unwinding loop thr2.0 iteration 4 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  35. Unwinding loop thr2.0 iteration 5 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  36. Unwinding loop thr2.0 iteration 6 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  37. Unwinding loop thr2.0 iteration 7 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  38. Unwinding loop thr2.0 iteration 8 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  39. Unwinding loop thr2.0 iteration 9 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  40. Not unwinding loop thr2.0 iteration 10 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  41. Unwinding loop main_thread.0 iteration 1 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 396 function main_thread thread 0
  42. Unwinding loop thr2.0 iteration 1 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  43. Unwinding loop thr2.0 iteration 2 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  44. Unwinding loop thr2.0 iteration 3 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  45. Unwinding loop thr2.0 iteration 4 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  46. Unwinding loop thr2.0 iteration 5 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  47. Unwinding loop thr2.0 iteration 6 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  48. Unwinding loop thr2.0 iteration 7 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  49. Unwinding loop thr2.0 iteration 8 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  50. Unwinding loop thr2.0 iteration 9 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  51. Not unwinding loop thr2.0 iteration 10 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  52. Unwinding loop main_thread.0 iteration 2 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 396 function main_thread thread 0
  53. Unwinding loop thr2.0 iteration 1 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  54. Unwinding loop thr2.0 iteration 2 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  55. Unwinding loop thr2.0 iteration 3 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  56. Unwinding loop thr2.0 iteration 4 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  57. Unwinding loop thr2.0 iteration 5 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  58. Unwinding loop thr2.0 iteration 6 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  59. Unwinding loop thr2.0 iteration 7 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  60. Unwinding loop thr2.0 iteration 8 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  61. Unwinding loop thr2.0 iteration 9 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  62. Not unwinding loop thr2.0 iteration 10 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  63. Unwinding loop main_thread.0 iteration 3 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 396 function main_thread thread 0
  64. Unwinding loop thr2.0 iteration 1 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  65. Unwinding loop thr2.0 iteration 2 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  66. Unwinding loop thr2.0 iteration 3 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  67. Unwinding loop thr2.0 iteration 4 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  68. Unwinding loop thr2.0 iteration 5 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  69. Unwinding loop thr2.0 iteration 6 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  70. Unwinding loop thr2.0 iteration 7 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  71. Unwinding loop thr2.0 iteration 8 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  72. Unwinding loop thr2.0 iteration 9 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  73. Not unwinding loop thr2.0 iteration 10 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  74. Unwinding loop main_thread.0 iteration 4 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 396 function main_thread thread 0
  75. Unwinding loop thr2.0 iteration 1 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  76. Unwinding loop thr2.0 iteration 2 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  77. Unwinding loop thr2.0 iteration 3 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  78. Unwinding loop thr2.0 iteration 4 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  79. Unwinding loop thr2.0 iteration 5 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  80. Unwinding loop thr2.0 iteration 6 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  81. Unwinding loop thr2.0 iteration 7 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  82. Unwinding loop thr2.0 iteration 8 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  83. Unwinding loop thr2.0 iteration 9 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  84. Not unwinding loop thr2.0 iteration 10 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  85. Unwinding loop main_thread.0 iteration 5 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 396 function main_thread thread 0
  86. Unwinding loop thr2.0 iteration 1 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  87. Unwinding loop thr2.0 iteration 2 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  88. Unwinding loop thr2.0 iteration 3 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  89. Unwinding loop thr2.0 iteration 4 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  90. Unwinding loop thr2.0 iteration 5 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  91. Unwinding loop thr2.0 iteration 6 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  92. Unwinding loop thr2.0 iteration 7 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  93. Unwinding loop thr2.0 iteration 8 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  94. Unwinding loop thr2.0 iteration 9 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  95. Not unwinding loop thr2.0 iteration 10 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  96. Unwinding loop main_thread.0 iteration 6 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 396 function main_thread thread 0
  97. Unwinding loop thr2.0 iteration 1 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  98. Unwinding loop thr2.0 iteration 2 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  99. Unwinding loop thr2.0 iteration 3 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  100. Unwinding loop thr2.0 iteration 4 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  101. Unwinding loop thr2.0 iteration 5 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  102. Unwinding loop thr2.0 iteration 6 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  103. Unwinding loop thr2.0 iteration 7 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  104. Unwinding loop thr2.0 iteration 8 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  105. Unwinding loop thr2.0 iteration 9 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  106. Not unwinding loop thr2.0 iteration 10 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  107. Unwinding loop main_thread.0 iteration 7 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 396 function main_thread thread 0
  108. Unwinding loop thr2.0 iteration 1 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  109. Unwinding loop thr2.0 iteration 2 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  110. Unwinding loop thr2.0 iteration 3 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  111. Unwinding loop thr2.0 iteration 4 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  112. Unwinding loop thr2.0 iteration 5 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  113. Unwinding loop thr2.0 iteration 6 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  114. Unwinding loop thr2.0 iteration 7 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  115. Unwinding loop thr2.0 iteration 8 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  116. Unwinding loop thr2.0 iteration 9 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  117. Not unwinding loop thr2.0 iteration 10 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  118. Unwinding loop main_thread.0 iteration 8 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 396 function main_thread thread 0
  119. Unwinding loop thr2.0 iteration 1 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  120. Unwinding loop thr2.0 iteration 2 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  121. Unwinding loop thr2.0 iteration 3 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  122. Unwinding loop thr2.0 iteration 4 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  123. Unwinding loop thr2.0 iteration 5 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  124. Unwinding loop thr2.0 iteration 6 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  125. Unwinding loop thr2.0 iteration 7 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  126. Unwinding loop thr2.0 iteration 8 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  127. Unwinding loop thr2.0 iteration 9 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  128. Not unwinding loop thr2.0 iteration 10 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  129. Unwinding loop main_thread.0 iteration 9 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 396 function main_thread thread 0
  130. Unwinding loop thr2.0 iteration 1 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  131. Unwinding loop thr2.0 iteration 2 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  132. Unwinding loop thr2.0 iteration 3 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  133. Unwinding loop thr2.0 iteration 4 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  134. Unwinding loop thr2.0 iteration 5 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  135. Unwinding loop thr2.0 iteration 6 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  136. Unwinding loop thr2.0 iteration 7 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  137. Unwinding loop thr2.0 iteration 8 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  138. Unwinding loop thr2.0 iteration 9 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  139. Not unwinding loop thr2.0 iteration 10 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 201 function thr2 thread 0
  140. Not unwinding loop main_thread.0 iteration 10 (10 max) file CBMC5.5/MUCSeq/_cs_27_Boop_simple_vf_false-unreach-call.c line 396 function main_thread thread 0
  141. size of program expression: 19297 steps
  142. simple slicing removed 3 assignments
  143. Generated 1 VCC(s), 1 remaining after simplification
  144. Passing problem to propositional reduction
  145. converting SSA
  146. Running propositional reduction
  147. Post-processing
  148. Solving with MiniSAT 2.2.1 with simplifier
  149. 601519 variables, 2545173 clauses
  150. SAT checker: instance is SATISFIABLE
  151. Runtime decision procedure: 52.706s
  152.  
  153. ** Results:
  154. [main.assertion.1] assertion (signed int)__CS_error != 1: FAILURE
  155.  
  156. ** 1 of 1 failed (1 iteration)
  157. VERIFICATION FAILED
Raw Paste

Login or Register to edit or fork this paste. It's free.