TEXT   181
CBMC version 5 4 64 bit x86 64 linux
Guest on 6th December 2024 12:16:41 AM


  1. CBMC version 5.5 64-bit x86_64 linux
  2. Parsing Z6.3_tso.c
  3. Converting
  4. Type-checking Z6.3_tso
  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 sysinit.0 iteration 1 file Z6.3_tso.h line 29 function sysinit thread 0
  12. Unwinding loop sysinit.0 iteration 2 file Z6.3_tso.h line 29 function sysinit thread 0
  13. Unwinding loop sysinit.0 iteration 3 file Z6.3_tso.h line 29 function sysinit thread 0
  14. Unwinding loop sysinit.1 iteration 1 file Z6.3_tso.h line 36 function sysinit thread 0
  15. Unwinding loop sysinit.1 iteration 2 file Z6.3_tso.h line 36 function sysinit thread 0
  16. Unwinding loop sysinit.1 iteration 3 file Z6.3_tso.h line 36 function sysinit thread 0
  17. Unwinding loop sysinit.1 iteration 4 file Z6.3_tso.h line 36 function sysinit thread 0
  18. Unwinding loop sysinit.2 iteration 1 file Z6.3_tso.h line 48 function sysinit thread 0
  19. Unwinding loop sysinit.2 iteration 2 file Z6.3_tso.h line 48 function sysinit thread 0
  20. Unwinding loop sysinit.2 iteration 3 file Z6.3_tso.h line 48 function sysinit thread 0
  21. Unwinding loop sysinit.3 iteration 1 file Z6.3_tso.h line 53 function sysinit thread 0
  22. Unwinding loop sysinit.3 iteration 2 file Z6.3_tso.h line 53 function sysinit thread 0
  23. Unwinding loop sysinit.3 iteration 3 file Z6.3_tso.h line 53 function sysinit thread 0
  24. Unwinding loop sysinit.3 iteration 4 file Z6.3_tso.h line 53 function sysinit thread 0
  25. Unwinding loop sysinit.4 iteration 1 file Z6.3_tso.h line 66 function sysinit thread 0
  26. Unwinding loop sysinit.4 iteration 2 file Z6.3_tso.h line 66 function sysinit thread 0
  27. Unwinding loop sysinit.4 iteration 3 file Z6.3_tso.h line 66 function sysinit thread 0
  28. Unwinding loop sysinit.5 iteration 1 file Z6.3_tso.h line 71 function sysinit thread 0
  29. Unwinding loop sysinit.5 iteration 2 file Z6.3_tso.h line 71 function sysinit thread 0
  30. Unwinding loop sysinit.5 iteration 3 file Z6.3_tso.h line 71 function sysinit thread 0
  31. Unwinding loop sysinit.5 iteration 4 file Z6.3_tso.h line 71 function sysinit thread 0
  32. size of program expression: 954 steps
  33. simple slicing removed 3 assignments
  34. Generated 1 VCC(s), 1 remaining after simplification
  35. Passing problem to propositional reduction
  36. converting SSA
  37. Running propositional reduction
  38. Post-processing
  39. Solving with MiniSAT 2.2.1 with simplifier
  40. 12658 variables, 27981 clauses
  41. SAT checker: instance is UNSATISFIABLE
  42. Runtime decision procedure: 0.049s
  43.  
  44. ** Results:
  45. [main.assertion.1] assertion !(y == 2 && r1 == 1 && r2 == 0): SUCCESS
  46.  
  47. ** 0 of 1 failed (1 iteration)
  48. VERIFICATION SUCCESSFUL
Raw Paste

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