Guest User

Untitled

a guest
Dec 22nd, 2015
19
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 43.88 KB | None | 0 0
  1. ===== The cycle =====
  2.  
  3. globals:
  4. key = @(48912:0| null)
  5. once = @(48914:0| { { 0, 0, 3, 0 } })
  6. stdin = @(48926:0| @(48927:0| { 48924:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
  7. stdout = @(48967:0| 48941:0 <...>)
  8. stderr = @(48969:0| 48950:0 <...>)
  9. __cxa_terminate_handler = @(49914:0| 159:0)
  10. __cxa_unexpected_handler = @(49916:0| 160:0)
  11. __cxa_new_handler = @(50390:0| null)
  12. __dso_handle = @(54063:0| null)
  13. _mpi_num_processes = @(54069:0| 2)
  14. _mpi_enable_mpi_comm_self = @(54071:0| 0)
  15. _mpi_exit_barrier = @(54073:0| 1)
  16. MPI_CHAR = @(54116:0| @(9:0| { { { @(10:0| { 0, 0 }), @(10:16| invalid), { { 10:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  17. MPI_SHORT = @(54118:0| @(11:0| { { { @(12:0| { 1, 0 }), @(12:16| invalid), { { 12:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  18. MPI_INT = @(54120:0| @(13:0| { { { @(14:0| { 2, 0 }), @(14:16| invalid), { { 14:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  19. MPI_LONG = @(54122:0| @(15:0| { { { @(16:0| { 3, 0 }), @(16:16| invalid), { { 16:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  20. MPI_LONG_LONG_INT = @(54124:0| @(17:0| { { { @(18:0| { 4, 0 }), @(18:16| invalid), { { 18:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  21. MPI_LONG_LONG = @(54126:0| @(19:0| { { { @(20:0| { 5, 0 }), @(20:16| invalid), { { 20:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  22. MPI_SIGNED_CHAR = @(54128:0| @(21:0| { { { @(22:0| { 6, 0 }), @(22:16| invalid), { { 22:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  23. MPI_UNSIGNED_CHAR = @(54130:0| @(23:0| { { { @(24:0| { 7, 0 }), @(24:16| invalid), { { 24:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  24. MPI_UNSIGNED_SHORT = @(54132:0| @(25:0| { { { @(26:0| { 8, 0 }), @(26:16| invalid), { { 26:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  25. MPI_UNSIGNED = @(54134:0| @(27:0| { { { @(28:0| { 9, 0 }), @(28:16| invalid), { { 28:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  26. MPI_UNSIGNED_LONG = @(54136:0| @(29:0| { { { @(30:0| { 10, 0 }), @(30:16| invalid), { { 30:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  27. MPI_UNSIGNED_LONG_LONG = @(54138:0| @(31:0| { { { @(32:0| { 11, 0 }), @(32:16| invalid), { { 32:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  28. MPI_FLOAT = @(54140:0| @(33:0| { { { @(34:0| { 12, 0 }), @(34:16| invalid), { { 34:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  29. MPI_DOUBLE = @(54142:0| @(35:0| { { { @(36:0| { 13, 0 }), @(36:16| invalid), { { 36:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  30. MPI_LONG_DOUBLE = @(54144:0| @(37:0| { { { @(38:0| { 14, 0 }), @(38:16| invalid), { { 38:16 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  31. MPI_WCHAR = @(54146:0| @(39:0| { { { @(40:0| { 15, 0 }), @(40:16| invalid), { { 40:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  32. MPI_C_BOOL = @(54148:0| @(41:0| { { { @(42:0| { 16, 0 }), @(42:16| invalid), { { 42:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  33. MPI_INT8_T = @(54150:0| @(43:0| { { { @(44:0| { 17, 0 }), @(44:16| invalid), { { 44:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  34. MPI_INT16_T = @(54152:0| @(45:0| { { { @(46:0| { 18, 0 }), @(46:16| invalid), { { 46:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  35. MPI_INT32_T = @(54154:0| @(47:0| { { { @(48:0| { 19, 0 }), @(48:16| invalid), { { 48:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  36. MPI_INT64_T = @(54156:0| @(49:0| { { { @(50:0| { 20, 0 }), @(50:16| invalid), { { 50:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  37. MPI_UINT8_T = @(54158:0| @(51:0| { { { @(52:0| { 21, 0 }), @(52:16| invalid), { { 52:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  38. MPI_UINT16_T = @(54160:0| @(53:0| { { { @(54:0| { 22, 0 }), @(54:16| invalid), { { 54:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  39. MPI_UINT32_T = @(54162:0| @(55:0| { { { @(56:0| { 23, 0 }), @(56:16| invalid), { { 56:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  40. MPI_UINT64_T = @(54164:0| @(57:0| { { { @(58:0| { 24, 0 }), @(58:16| invalid), { { 58:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  41. MPI_AINT = @(54166:0| @(59:0| { { { @(60:0| { 25, 0 }), @(60:16| invalid), { { 60:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  42. MPI_COUNT = @(54168:0| @(61:0| { { { @(62:0| { 26, 0 }), @(62:16| invalid), { { 62:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  43. MPI_OFFSET = @(54170:0| @(63:0| { { { @(64:0| { 27, 0 }), @(64:16| invalid), { { 64:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  44. MPI_C_COMPLEX = @(54172:0| @(65:0| { { { @(66:0| { 28, 0 }), @(66:16| invalid), { { 66:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  45. MPI_C_FLOAT_COMPLEX = @(54174:0| @(67:0| { { { @(68:0| { 29, 0 }), @(68:16| invalid), { { 68:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  46. MPI_C_DOUBLE_COMPLEX = @(54176:0| @(69:0| { { { @(70:0| { 30, 0 }), @(70:16| invalid), { { 70:16 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  47. MPI_C_LONG_DOUBLE_COMPLEX = @(54178:0| @(71:0| { { { @(72:0| { 31, 0 }), @(72:16| invalid), { { 72:16 <...> } } } }, 1, 0, 0, 0, 32, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  48. MPI_BYTE = @(54180:0| @(73:0| { { { @(74:0| { 7, 0 }), @(74:16| invalid), { { 74:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  49. MPI_PACKED = @(54182:0| @(75:0| { { { @(76:0| { 7, 0 }), @(76:16| invalid), { { 76:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  50. MPI_FLOAT_INT = @(54184:0| @(77:0| { { { @(78:0| { 12, 0 }), @(78:32| invalid), { { 78:32 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  51. MPI_DOUBLE_INT = @(54186:0| @(79:0| { { { @(80:0| { 13, 0 }), @(80:32| invalid), { { 80:32 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  52. MPI_LONG_INT = @(54188:0| @(81:0| { { { @(82:0| { 3, 0 }), @(82:32| invalid), { { 82:32 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  53. MPI_2INT = @(54190:0| @(83:0| { { { @(84:0| { 2, 0 }), @(84:32| invalid), { { 84:32 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  54. MPI_SHORT_INT = @(54192:0| @(85:0| { { { @(86:0| { 1, 0 }), @(86:32| invalid), { { 86:32 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  55. MPI_LONG_DOUBLE_INT = @(54194:0| @(87:0| { { { @(88:0| { 14, 0 }), @(88:32| invalid), { { 88:32 <...> } } } }, 1, 0, 0, 0, 32, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  56. MPI_MAX = @(54200:0| @(89:0| { 0 }))
  57. MPI_MIN = @(54202:0| @(90:0| { 1 }))
  58. MPI_SUM = @(54204:0| @(91:0| { 2 }))
  59. MPI_PROD = @(54206:0| @(92:0| { 3 }))
  60. MPI_MAXLOC = @(54208:0| @(93:0| { 4 }))
  61. MPI_MINLOC = @(54210:0| @(94:0| { 5 }))
  62. MPI_BAND = @(54212:0| @(95:0| { 6 }))
  63. MPI_BOR = @(54214:0| @(96:0| { 7 }))
  64. MPI_BXOR = @(54216:0| @(97:0| { 8 }))
  65. MPI_LAND = @(54218:0| @(98:0| { 9 }))
  66. MPI_LOR = @(54220:0| @(99:0| { 10 }))
  67. MPI_LXOR = @(54222:0| @(100:0| { 11 }))
  68. MPI_GROUP_EMPTY = @(54224:0| @(101:0| { { { null, null, { { null } } } } }))
  69. MPI_COMM_WORLD_ = @(54228:0| @(102:0| @(0:1| invalid)))
  70. MPI_COMM_SELF_ = @(54230:0| @(103:0| null))
  71. thread 0:
  72. #1: <_divine_start> [ entry.cpp:88 ] [ ctorcount = 6, ctors = 917274624, mainproto = 0, c = @(111:0| @(55986:96| invalid)), i = @(112:0| 6), r = @(113:0| 0?), i1 = @(114:0| 1) ]
  73. #2: <_divine_invoke_main_mpi> [ entry.cpp:49 ] [ mainproto = @(110:0| 0), r = @(116:0| 0), finalized = @(117:0| 1) ]
  74. thread 1:
  75. #1: <_divine_invoke_main_mpi> [ entry.cpp:33 ] [ mainproto = 110:0 <...>, r = @(119:0| 0?), finalized = @(120:0| 0?) ]
  76. #2: <_divine_invoke_main> [ entry.cpp:21 ] [ mainproto = 0, r = @(122:0| 0?) ]
  77. #3: <main> [ ../sanity_ltl.c:18 ] [ rank = @(124:0| 1) ]
  78. LTL: 0 ([ -2 ] -> 0; )
  79. fairness id = 1
  80.  
  81. globals:
  82. key = @(48912:0| null)
  83. once = @(48914:0| { { 0, 0, 3, 0 } })
  84. stdin = @(48926:0| @(48927:0| { 48924:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
  85. stdout = @(48967:0| 48941:0 <...>)
  86. stderr = @(48969:0| 48950:0 <...>)
  87. __cxa_terminate_handler = @(49914:0| 159:0)
  88. __cxa_unexpected_handler = @(49916:0| 160:0)
  89. __cxa_new_handler = @(50390:0| null)
  90. __dso_handle = @(54063:0| null)
  91. _mpi_num_processes = @(54069:0| 2)
  92. _mpi_enable_mpi_comm_self = @(54071:0| 0)
  93. _mpi_exit_barrier = @(54073:0| 1)
  94. MPI_CHAR = @(54116:0| @(9:0| { { { @(10:0| { 0, 0 }), @(10:16| invalid), { { 10:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  95. MPI_SHORT = @(54118:0| @(11:0| { { { @(12:0| { 1, 0 }), @(12:16| invalid), { { 12:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  96. MPI_INT = @(54120:0| @(13:0| { { { @(14:0| { 2, 0 }), @(14:16| invalid), { { 14:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  97. MPI_LONG = @(54122:0| @(15:0| { { { @(16:0| { 3, 0 }), @(16:16| invalid), { { 16:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  98. MPI_LONG_LONG_INT = @(54124:0| @(17:0| { { { @(18:0| { 4, 0 }), @(18:16| invalid), { { 18:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  99. MPI_LONG_LONG = @(54126:0| @(19:0| { { { @(20:0| { 5, 0 }), @(20:16| invalid), { { 20:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  100. MPI_SIGNED_CHAR = @(54128:0| @(21:0| { { { @(22:0| { 6, 0 }), @(22:16| invalid), { { 22:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  101. MPI_UNSIGNED_CHAR = @(54130:0| @(23:0| { { { @(24:0| { 7, 0 }), @(24:16| invalid), { { 24:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  102. MPI_UNSIGNED_SHORT = @(54132:0| @(25:0| { { { @(26:0| { 8, 0 }), @(26:16| invalid), { { 26:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  103. MPI_UNSIGNED = @(54134:0| @(27:0| { { { @(28:0| { 9, 0 }), @(28:16| invalid), { { 28:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  104. MPI_UNSIGNED_LONG = @(54136:0| @(29:0| { { { @(30:0| { 10, 0 }), @(30:16| invalid), { { 30:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  105. MPI_UNSIGNED_LONG_LONG = @(54138:0| @(31:0| { { { @(32:0| { 11, 0 }), @(32:16| invalid), { { 32:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  106. MPI_FLOAT = @(54140:0| @(33:0| { { { @(34:0| { 12, 0 }), @(34:16| invalid), { { 34:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  107. MPI_DOUBLE = @(54142:0| @(35:0| { { { @(36:0| { 13, 0 }), @(36:16| invalid), { { 36:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  108. MPI_LONG_DOUBLE = @(54144:0| @(37:0| { { { @(38:0| { 14, 0 }), @(38:16| invalid), { { 38:16 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  109. MPI_WCHAR = @(54146:0| @(39:0| { { { @(40:0| { 15, 0 }), @(40:16| invalid), { { 40:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  110. MPI_C_BOOL = @(54148:0| @(41:0| { { { @(42:0| { 16, 0 }), @(42:16| invalid), { { 42:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  111. MPI_INT8_T = @(54150:0| @(43:0| { { { @(44:0| { 17, 0 }), @(44:16| invalid), { { 44:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  112. MPI_INT16_T = @(54152:0| @(45:0| { { { @(46:0| { 18, 0 }), @(46:16| invalid), { { 46:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  113. MPI_INT32_T = @(54154:0| @(47:0| { { { @(48:0| { 19, 0 }), @(48:16| invalid), { { 48:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  114. MPI_INT64_T = @(54156:0| @(49:0| { { { @(50:0| { 20, 0 }), @(50:16| invalid), { { 50:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  115. MPI_UINT8_T = @(54158:0| @(51:0| { { { @(52:0| { 21, 0 }), @(52:16| invalid), { { 52:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  116. MPI_UINT16_T = @(54160:0| @(53:0| { { { @(54:0| { 22, 0 }), @(54:16| invalid), { { 54:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  117. MPI_UINT32_T = @(54162:0| @(55:0| { { { @(56:0| { 23, 0 }), @(56:16| invalid), { { 56:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  118. MPI_UINT64_T = @(54164:0| @(57:0| { { { @(58:0| { 24, 0 }), @(58:16| invalid), { { 58:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  119. MPI_AINT = @(54166:0| @(59:0| { { { @(60:0| { 25, 0 }), @(60:16| invalid), { { 60:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  120. MPI_COUNT = @(54168:0| @(61:0| { { { @(62:0| { 26, 0 }), @(62:16| invalid), { { 62:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  121. MPI_OFFSET = @(54170:0| @(63:0| { { { @(64:0| { 27, 0 }), @(64:16| invalid), { { 64:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  122. MPI_C_COMPLEX = @(54172:0| @(65:0| { { { @(66:0| { 28, 0 }), @(66:16| invalid), { { 66:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  123. MPI_C_FLOAT_COMPLEX = @(54174:0| @(67:0| { { { @(68:0| { 29, 0 }), @(68:16| invalid), { { 68:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  124. MPI_C_DOUBLE_COMPLEX = @(54176:0| @(69:0| { { { @(70:0| { 30, 0 }), @(70:16| invalid), { { 70:16 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  125. MPI_C_LONG_DOUBLE_COMPLEX = @(54178:0| @(71:0| { { { @(72:0| { 31, 0 }), @(72:16| invalid), { { 72:16 <...> } } } }, 1, 0, 0, 0, 32, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  126. MPI_BYTE = @(54180:0| @(73:0| { { { @(74:0| { 7, 0 }), @(74:16| invalid), { { 74:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  127. MPI_PACKED = @(54182:0| @(75:0| { { { @(76:0| { 7, 0 }), @(76:16| invalid), { { 76:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  128. MPI_FLOAT_INT = @(54184:0| @(77:0| { { { @(78:0| { 12, 0 }), @(78:32| invalid), { { 78:32 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  129. MPI_DOUBLE_INT = @(54186:0| @(79:0| { { { @(80:0| { 13, 0 }), @(80:32| invalid), { { 80:32 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  130. MPI_LONG_INT = @(54188:0| @(81:0| { { { @(82:0| { 3, 0 }), @(82:32| invalid), { { 82:32 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  131. MPI_2INT = @(54190:0| @(83:0| { { { @(84:0| { 2, 0 }), @(84:32| invalid), { { 84:32 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  132. MPI_SHORT_INT = @(54192:0| @(85:0| { { { @(86:0| { 1, 0 }), @(86:32| invalid), { { 86:32 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  133. MPI_LONG_DOUBLE_INT = @(54194:0| @(87:0| { { { @(88:0| { 14, 0 }), @(88:32| invalid), { { 88:32 <...> } } } }, 1, 0, 0, 0, 32, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  134. MPI_MAX = @(54200:0| @(89:0| { 0 }))
  135. MPI_MIN = @(54202:0| @(90:0| { 1 }))
  136. MPI_SUM = @(54204:0| @(91:0| { 2 }))
  137. MPI_PROD = @(54206:0| @(92:0| { 3 }))
  138. MPI_MAXLOC = @(54208:0| @(93:0| { 4 }))
  139. MPI_MINLOC = @(54210:0| @(94:0| { 5 }))
  140. MPI_BAND = @(54212:0| @(95:0| { 6 }))
  141. MPI_BOR = @(54214:0| @(96:0| { 7 }))
  142. MPI_BXOR = @(54216:0| @(97:0| { 8 }))
  143. MPI_LAND = @(54218:0| @(98:0| { 9 }))
  144. MPI_LOR = @(54220:0| @(99:0| { 10 }))
  145. MPI_LXOR = @(54222:0| @(100:0| { 11 }))
  146. MPI_GROUP_EMPTY = @(54224:0| @(101:0| { { { null, null, { { null } } } } }))
  147. MPI_COMM_WORLD_ = @(54228:0| @(102:0| @(0:1| invalid)))
  148. MPI_COMM_SELF_ = @(54230:0| @(103:0| null))
  149. thread 0:
  150. #1: <_divine_start> [ entry.cpp:88 ] [ ctorcount = 6, ctors = 917274624, mainproto = 0, c = @(111:0| @(55986:96| invalid)), i = @(112:0| 6), r = @(113:0| 0?), i1 = @(114:0| 1) ]
  151. #2: <_divine_invoke_main_mpi> [ entry.cpp:49 ] [ mainproto = @(110:0| 0), r = @(116:0| 0), finalized = @(117:0| 1) ]
  152. thread 1:
  153. #1: <_divine_invoke_main_mpi> [ entry.cpp:33 ] [ mainproto = 110:0 <...>, r = @(119:0| 0?), finalized = @(120:0| 0?) ]
  154. #2: <_divine_invoke_main> [ entry.cpp:21 ] [ mainproto = 0, r = @(122:0| 0?) ]
  155. #3: <main> [ ../sanity_ltl.c:18 ] [ rank = @(124:0| 1) ]
  156. LTL: 0 ([ -2 ] -> 0; )
  157. fairness id = 2
  158.  
  159. globals:
  160. key = @(48912:0| null)
  161. once = @(48914:0| { { 0, 0, 3, 0 } })
  162. stdin = @(48926:0| @(48927:0| { 48924:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
  163. stdout = @(48967:0| 48941:0 <...>)
  164. stderr = @(48969:0| 48950:0 <...>)
  165. __cxa_terminate_handler = @(49914:0| 159:0)
  166. __cxa_unexpected_handler = @(49916:0| 160:0)
  167. __cxa_new_handler = @(50390:0| null)
  168. __dso_handle = @(54063:0| null)
  169. _mpi_num_processes = @(54069:0| 2)
  170. _mpi_enable_mpi_comm_self = @(54071:0| 0)
  171. _mpi_exit_barrier = @(54073:0| 1)
  172. MPI_CHAR = @(54116:0| @(9:0| { { { @(10:0| { 0, 0 }), @(10:16| invalid), { { 10:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  173. MPI_SHORT = @(54118:0| @(11:0| { { { @(12:0| { 1, 0 }), @(12:16| invalid), { { 12:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  174. MPI_INT = @(54120:0| @(13:0| { { { @(14:0| { 2, 0 }), @(14:16| invalid), { { 14:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  175. MPI_LONG = @(54122:0| @(15:0| { { { @(16:0| { 3, 0 }), @(16:16| invalid), { { 16:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  176. MPI_LONG_LONG_INT = @(54124:0| @(17:0| { { { @(18:0| { 4, 0 }), @(18:16| invalid), { { 18:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  177. MPI_LONG_LONG = @(54126:0| @(19:0| { { { @(20:0| { 5, 0 }), @(20:16| invalid), { { 20:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  178. MPI_SIGNED_CHAR = @(54128:0| @(21:0| { { { @(22:0| { 6, 0 }), @(22:16| invalid), { { 22:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  179. MPI_UNSIGNED_CHAR = @(54130:0| @(23:0| { { { @(24:0| { 7, 0 }), @(24:16| invalid), { { 24:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  180. MPI_UNSIGNED_SHORT = @(54132:0| @(25:0| { { { @(26:0| { 8, 0 }), @(26:16| invalid), { { 26:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  181. MPI_UNSIGNED = @(54134:0| @(27:0| { { { @(28:0| { 9, 0 }), @(28:16| invalid), { { 28:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  182. MPI_UNSIGNED_LONG = @(54136:0| @(29:0| { { { @(30:0| { 10, 0 }), @(30:16| invalid), { { 30:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  183. MPI_UNSIGNED_LONG_LONG = @(54138:0| @(31:0| { { { @(32:0| { 11, 0 }), @(32:16| invalid), { { 32:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  184. MPI_FLOAT = @(54140:0| @(33:0| { { { @(34:0| { 12, 0 }), @(34:16| invalid), { { 34:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  185. MPI_DOUBLE = @(54142:0| @(35:0| { { { @(36:0| { 13, 0 }), @(36:16| invalid), { { 36:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  186. MPI_LONG_DOUBLE = @(54144:0| @(37:0| { { { @(38:0| { 14, 0 }), @(38:16| invalid), { { 38:16 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  187. MPI_WCHAR = @(54146:0| @(39:0| { { { @(40:0| { 15, 0 }), @(40:16| invalid), { { 40:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  188. MPI_C_BOOL = @(54148:0| @(41:0| { { { @(42:0| { 16, 0 }), @(42:16| invalid), { { 42:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  189. MPI_INT8_T = @(54150:0| @(43:0| { { { @(44:0| { 17, 0 }), @(44:16| invalid), { { 44:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  190. MPI_INT16_T = @(54152:0| @(45:0| { { { @(46:0| { 18, 0 }), @(46:16| invalid), { { 46:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  191. MPI_INT32_T = @(54154:0| @(47:0| { { { @(48:0| { 19, 0 }), @(48:16| invalid), { { 48:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  192. MPI_INT64_T = @(54156:0| @(49:0| { { { @(50:0| { 20, 0 }), @(50:16| invalid), { { 50:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  193. MPI_UINT8_T = @(54158:0| @(51:0| { { { @(52:0| { 21, 0 }), @(52:16| invalid), { { 52:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  194. MPI_UINT16_T = @(54160:0| @(53:0| { { { @(54:0| { 22, 0 }), @(54:16| invalid), { { 54:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  195. MPI_UINT32_T = @(54162:0| @(55:0| { { { @(56:0| { 23, 0 }), @(56:16| invalid), { { 56:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  196. MPI_UINT64_T = @(54164:0| @(57:0| { { { @(58:0| { 24, 0 }), @(58:16| invalid), { { 58:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  197. MPI_AINT = @(54166:0| @(59:0| { { { @(60:0| { 25, 0 }), @(60:16| invalid), { { 60:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  198. MPI_COUNT = @(54168:0| @(61:0| { { { @(62:0| { 26, 0 }), @(62:16| invalid), { { 62:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  199. MPI_OFFSET = @(54170:0| @(63:0| { { { @(64:0| { 27, 0 }), @(64:16| invalid), { { 64:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  200. MPI_C_COMPLEX = @(54172:0| @(65:0| { { { @(66:0| { 28, 0 }), @(66:16| invalid), { { 66:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  201. MPI_C_FLOAT_COMPLEX = @(54174:0| @(67:0| { { { @(68:0| { 29, 0 }), @(68:16| invalid), { { 68:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  202. MPI_C_DOUBLE_COMPLEX = @(54176:0| @(69:0| { { { @(70:0| { 30, 0 }), @(70:16| invalid), { { 70:16 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  203. MPI_C_LONG_DOUBLE_COMPLEX = @(54178:0| @(71:0| { { { @(72:0| { 31, 0 }), @(72:16| invalid), { { 72:16 <...> } } } }, 1, 0, 0, 0, 32, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  204. MPI_BYTE = @(54180:0| @(73:0| { { { @(74:0| { 7, 0 }), @(74:16| invalid), { { 74:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  205. MPI_PACKED = @(54182:0| @(75:0| { { { @(76:0| { 7, 0 }), @(76:16| invalid), { { 76:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  206. MPI_FLOAT_INT = @(54184:0| @(77:0| { { { @(78:0| { 12, 0 }), @(78:32| invalid), { { 78:32 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  207. MPI_DOUBLE_INT = @(54186:0| @(79:0| { { { @(80:0| { 13, 0 }), @(80:32| invalid), { { 80:32 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  208. MPI_LONG_INT = @(54188:0| @(81:0| { { { @(82:0| { 3, 0 }), @(82:32| invalid), { { 82:32 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  209. MPI_2INT = @(54190:0| @(83:0| { { { @(84:0| { 2, 0 }), @(84:32| invalid), { { 84:32 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  210. MPI_SHORT_INT = @(54192:0| @(85:0| { { { @(86:0| { 1, 0 }), @(86:32| invalid), { { 86:32 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  211. MPI_LONG_DOUBLE_INT = @(54194:0| @(87:0| { { { @(88:0| { 14, 0 }), @(88:32| invalid), { { 88:32 <...> } } } }, 1, 0, 0, 0, 32, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  212. MPI_MAX = @(54200:0| @(89:0| { 0 }))
  213. MPI_MIN = @(54202:0| @(90:0| { 1 }))
  214. MPI_SUM = @(54204:0| @(91:0| { 2 }))
  215. MPI_PROD = @(54206:0| @(92:0| { 3 }))
  216. MPI_MAXLOC = @(54208:0| @(93:0| { 4 }))
  217. MPI_MINLOC = @(54210:0| @(94:0| { 5 }))
  218. MPI_BAND = @(54212:0| @(95:0| { 6 }))
  219. MPI_BOR = @(54214:0| @(96:0| { 7 }))
  220. MPI_BXOR = @(54216:0| @(97:0| { 8 }))
  221. MPI_LAND = @(54218:0| @(98:0| { 9 }))
  222. MPI_LOR = @(54220:0| @(99:0| { 10 }))
  223. MPI_LXOR = @(54222:0| @(100:0| { 11 }))
  224. MPI_GROUP_EMPTY = @(54224:0| @(101:0| { { { null, null, { { null } } } } }))
  225. MPI_COMM_WORLD_ = @(54228:0| @(102:0| @(0:1| invalid)))
  226. MPI_COMM_SELF_ = @(54230:0| @(103:0| null))
  227. thread 0:
  228. #1: <_divine_start> [ entry.cpp:88 ] [ ctorcount = 6, ctors = 917274624, mainproto = 0, c = @(111:0| @(55986:96| invalid)), i = @(112:0| 6), r = @(113:0| 0?), i1 = @(114:0| 1) ]
  229. #2: <_divine_invoke_main_mpi> [ entry.cpp:49 ] [ mainproto = @(110:0| 0), r = @(116:0| 0), finalized = @(117:0| 1) ]
  230. thread 1:
  231. #1: <_divine_invoke_main_mpi> [ entry.cpp:33 ] [ mainproto = 110:0 <...>, r = @(119:0| 0?), finalized = @(120:0| 0?) ]
  232. #2: <_divine_invoke_main> [ entry.cpp:21 ] [ mainproto = 0, r = @(122:0| 0?) ]
  233. #3: <main> [ ../sanity_ltl.c:18 ] [ rank = @(124:0| 1) ]
  234. LTL: 0 ([ -2 ] -> 0; )
  235. fairness id = 3
  236.  
  237. globals:
  238. key = @(48912:0| null)
  239. once = @(48914:0| { { 0, 0, 3, 0 } })
  240. stdin = @(48926:0| @(48927:0| { 48924:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
  241. stdout = @(48967:0| 48941:0 <...>)
  242. stderr = @(48969:0| 48950:0 <...>)
  243. __cxa_terminate_handler = @(49914:0| 159:0)
  244. __cxa_unexpected_handler = @(49916:0| 160:0)
  245. __cxa_new_handler = @(50390:0| null)
  246. __dso_handle = @(54063:0| null)
  247. _mpi_num_processes = @(54069:0| 2)
  248. _mpi_enable_mpi_comm_self = @(54071:0| 0)
  249. _mpi_exit_barrier = @(54073:0| 1)
  250. MPI_CHAR = @(54116:0| @(9:0| { { { @(10:0| { 0, 0 }), @(10:16| invalid), { { 10:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  251. MPI_SHORT = @(54118:0| @(11:0| { { { @(12:0| { 1, 0 }), @(12:16| invalid), { { 12:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  252. MPI_INT = @(54120:0| @(13:0| { { { @(14:0| { 2, 0 }), @(14:16| invalid), { { 14:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  253. MPI_LONG = @(54122:0| @(15:0| { { { @(16:0| { 3, 0 }), @(16:16| invalid), { { 16:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  254. MPI_LONG_LONG_INT = @(54124:0| @(17:0| { { { @(18:0| { 4, 0 }), @(18:16| invalid), { { 18:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  255. MPI_LONG_LONG = @(54126:0| @(19:0| { { { @(20:0| { 5, 0 }), @(20:16| invalid), { { 20:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  256. MPI_SIGNED_CHAR = @(54128:0| @(21:0| { { { @(22:0| { 6, 0 }), @(22:16| invalid), { { 22:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  257. MPI_UNSIGNED_CHAR = @(54130:0| @(23:0| { { { @(24:0| { 7, 0 }), @(24:16| invalid), { { 24:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  258. MPI_UNSIGNED_SHORT = @(54132:0| @(25:0| { { { @(26:0| { 8, 0 }), @(26:16| invalid), { { 26:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  259. MPI_UNSIGNED = @(54134:0| @(27:0| { { { @(28:0| { 9, 0 }), @(28:16| invalid), { { 28:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  260. MPI_UNSIGNED_LONG = @(54136:0| @(29:0| { { { @(30:0| { 10, 0 }), @(30:16| invalid), { { 30:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  261. MPI_UNSIGNED_LONG_LONG = @(54138:0| @(31:0| { { { @(32:0| { 11, 0 }), @(32:16| invalid), { { 32:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  262. MPI_FLOAT = @(54140:0| @(33:0| { { { @(34:0| { 12, 0 }), @(34:16| invalid), { { 34:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  263. MPI_DOUBLE = @(54142:0| @(35:0| { { { @(36:0| { 13, 0 }), @(36:16| invalid), { { 36:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  264. MPI_LONG_DOUBLE = @(54144:0| @(37:0| { { { @(38:0| { 14, 0 }), @(38:16| invalid), { { 38:16 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  265. MPI_WCHAR = @(54146:0| @(39:0| { { { @(40:0| { 15, 0 }), @(40:16| invalid), { { 40:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  266. MPI_C_BOOL = @(54148:0| @(41:0| { { { @(42:0| { 16, 0 }), @(42:16| invalid), { { 42:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  267. MPI_INT8_T = @(54150:0| @(43:0| { { { @(44:0| { 17, 0 }), @(44:16| invalid), { { 44:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  268. MPI_INT16_T = @(54152:0| @(45:0| { { { @(46:0| { 18, 0 }), @(46:16| invalid), { { 46:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  269. MPI_INT32_T = @(54154:0| @(47:0| { { { @(48:0| { 19, 0 }), @(48:16| invalid), { { 48:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  270. MPI_INT64_T = @(54156:0| @(49:0| { { { @(50:0| { 20, 0 }), @(50:16| invalid), { { 50:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  271. MPI_UINT8_T = @(54158:0| @(51:0| { { { @(52:0| { 21, 0 }), @(52:16| invalid), { { 52:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  272. MPI_UINT16_T = @(54160:0| @(53:0| { { { @(54:0| { 22, 0 }), @(54:16| invalid), { { 54:16 <...> } } } }, 1, 0, 0, 0, 2, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  273. MPI_UINT32_T = @(54162:0| @(55:0| { { { @(56:0| { 23, 0 }), @(56:16| invalid), { { 56:16 <...> } } } }, 1, 0, 0, 0, 4, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  274. MPI_UINT64_T = @(54164:0| @(57:0| { { { @(58:0| { 24, 0 }), @(58:16| invalid), { { 58:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  275. MPI_AINT = @(54166:0| @(59:0| { { { @(60:0| { 25, 0 }), @(60:16| invalid), { { 60:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  276. MPI_COUNT = @(54168:0| @(61:0| { { { @(62:0| { 26, 0 }), @(62:16| invalid), { { 62:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  277. MPI_OFFSET = @(54170:0| @(63:0| { { { @(64:0| { 27, 0 }), @(64:16| invalid), { { 64:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  278. MPI_C_COMPLEX = @(54172:0| @(65:0| { { { @(66:0| { 28, 0 }), @(66:16| invalid), { { 66:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  279. MPI_C_FLOAT_COMPLEX = @(54174:0| @(67:0| { { { @(68:0| { 29, 0 }), @(68:16| invalid), { { 68:16 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  280. MPI_C_DOUBLE_COMPLEX = @(54176:0| @(69:0| { { { @(70:0| { 30, 0 }), @(70:16| invalid), { { 70:16 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  281. MPI_C_LONG_DOUBLE_COMPLEX = @(54178:0| @(71:0| { { { @(72:0| { 31, 0 }), @(72:16| invalid), { { 72:16 <...> } } } }, 1, 0, 0, 0, 32, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  282. MPI_BYTE = @(54180:0| @(73:0| { { { @(74:0| { 7, 0 }), @(74:16| invalid), { { 74:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  283. MPI_PACKED = @(54182:0| @(75:0| { { { @(76:0| { 7, 0 }), @(76:16| invalid), { { 76:16 <...> } } } }, 1, 0, 0, 0, 1, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  284. MPI_FLOAT_INT = @(54184:0| @(77:0| { { { @(78:0| { 12, 0 }), @(78:32| invalid), { { 78:32 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  285. MPI_DOUBLE_INT = @(54186:0| @(79:0| { { { @(80:0| { 13, 0 }), @(80:32| invalid), { { 80:32 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  286. MPI_LONG_INT = @(54188:0| @(81:0| { { { @(82:0| { 3, 0 }), @(82:32| invalid), { { 82:32 <...> } } } }, 1, 0, 0, 0, 16, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  287. MPI_2INT = @(54190:0| @(83:0| { { { @(84:0| { 2, 0 }), @(84:32| invalid), { { 84:32 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  288. MPI_SHORT_INT = @(54192:0| @(85:0| { { { @(86:0| { 1, 0 }), @(86:32| invalid), { { 86:32 <...> } } } }, 1, 0, 0, 0, 8, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  289. MPI_LONG_DOUBLE_INT = @(54194:0| @(87:0| { { { @(88:0| { 14, 0 }), @(88:32| invalid), { { 88:32 <...> } } } }, 1, 0, 0, 0, 32, 8, { { null, null, { { null } } } }, { { null, null, { { null } } } }, { { null, null, { { null } } } } }))
  290. MPI_MAX = @(54200:0| @(89:0| { 0 }))
  291. MPI_MIN = @(54202:0| @(90:0| { 1 }))
  292. MPI_SUM = @(54204:0| @(91:0| { 2 }))
  293. MPI_PROD = @(54206:0| @(92:0| { 3 }))
  294. MPI_MAXLOC = @(54208:0| @(93:0| { 4 }))
  295. MPI_MINLOC = @(54210:0| @(94:0| { 5 }))
  296. MPI_BAND = @(54212:0| @(95:0| { 6 }))
  297. MPI_BOR = @(54214:0| @(96:0| { 7 }))
  298. MPI_BXOR = @(54216:0| @(97:0| { 8 }))
  299. MPI_LAND = @(54218:0| @(98:0| { 9 }))
  300. MPI_LOR = @(54220:0| @(99:0| { 10 }))
  301. MPI_LXOR = @(54222:0| @(100:0| { 11 }))
  302. MPI_GROUP_EMPTY = @(54224:0| @(101:0| { { { null, null, { { null } } } } }))
  303. MPI_COMM_WORLD_ = @(54228:0| @(102:0| @(0:1| invalid)))
  304. MPI_COMM_SELF_ = @(54230:0| @(103:0| null))
  305. thread 0:
  306. #1: <_divine_start> [ entry.cpp:88 ] [ ctorcount = 6, ctors = 917274624, mainproto = 0, c = @(111:0| @(55986:96| invalid)), i = @(112:0| 6), r = @(113:0| 0?), i1 = @(114:0| 1) ]
  307. #2: <_divine_invoke_main_mpi> [ entry.cpp:49 ] [ mainproto = @(110:0| 0), r = @(116:0| 0), finalized = @(117:0| 1) ]
  308. thread 1:
  309. #1: <_divine_invoke_main_mpi> [ entry.cpp:33 ] [ mainproto = 110:0 <...>, r = @(119:0| 0?), finalized = @(120:0| 0?) ]
  310. #2: <_divine_invoke_main> [ entry.cpp:21 ] [ mainproto = 0, r = @(122:0| 0?) ]
  311. #3: <main> [ ../sanity_ltl.c:18 ] [ rank = @(124:0| 1) ]
  312. LTL: 0 ([ -2 ] -> 0; )
  313. fairness id = 0
  314.  
  315. done
Add Comment
Please, Sign In to add comment