================================ TASS Error Log ================================
               model : race2 (numProcs = 3)
          sourceFile : examples/collectiveInvariant/race/race2.c
                mode : VERIFY
              prover : CVC3
            deadlock : POTENTIAL
           reduction : URGENT
            simplify : true
         bufferBound : 1
             verbose : false
         loop method : true
   collectiveAsserts : false
               cqmin : true
        detectCycles : false
          repository : examples/collectiveInvariant/race/TASSREP
            frontend : ANTLR
          errorBound : 10


Number of errors reported........... 14
Number of distinct errors........... 3

--------------------------------------------------------------------------------

Error 0: Execution error (kind: ASSERTION_VIOLATION, certainty: MAYBE)
Collective assertions remained when program halted at State 24
 with:
  Process 0 at location 8: libmpi.c 252.4--252.46: "recv(_tmp, any(thesource), _tag, thesize);"
  Process 1 at location 11: libmpi.c 307.4--307.37: "recv(_tmp, 0, MPIX_BARRIER_EXIT);"
  Process 2 at location 4: libmpi.c 181.2--181.26: "send(_tmp, _dest, _tag);"

Trace logged in race2_0.trace

--------------------------------------------------------------------------------

Error 1: Execution error (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
Collective assertion L1 can be violated.
    path condition : SIZEOF_TYPE(2) + -1 >= 0 && Y0 + -2 = 0
         assertion : false
Source location: race2.c 27.34--27.43: "L1 s == t"
Trace logged in race2_1.trace

--------------------------------------------------------------------------------

Error 2: Execution error (kind: ASSERTION_VIOLATION, certainty: MAYBE)
Collective assertions remained when program halted at State 189
 with:
  Process 0 at location 8: libmpi.c 252.4--252.46: "recv(_tmp, any(thesource), _tag, thesize);"
  Process 1 at location 4: libmpi.c 181.2--181.26: "send(_tmp, _dest, _tag);"
  Process 2 at location 11: libmpi.c 307.4--307.37: "recv(_tmp, 0, MPIX_BARRIER_EXIT);"

Trace logged in race2_2.trace

--------------------------------------------------------------------------------
