================================ TASS Error Log ================================
       specification : diffusion_seq (numProcs = 1)
      specSourceFile : examples/collectiveAssert/diffusion_seq.c
      implementation : ghost (numProcs = 3)
      implSourceFile : examples/collectiveAssert/ghost.c
                mode : COMPARE
              prover : CVC3
            deadlock : ABSOLUTE
           reduction : URGENT
            simplify : true
      simplifyProver : false
         bufferBound : 10
             verbose : false
         loop method : true
   collectiveAsserts : true
          repository : examples/collectiveAssert/TASSREP
            frontend : MINIMP
          errorBound : 1
        NSTEPS_BOUND = 2
            NX_BOUND = 6
                  NP = 3


Number of errors reported........... 1
Number of distinct errors........... 1

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

Error 0: Execution error (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
Out of order collective assertion: Process 0 of model ghost arrived at assertion:
Collective Assertion of ghost.c 98.31--98.106: "GHOSTS v[nxl] == PROC[right].v[0] && v[1] == PROC[left].v[PROC[left].nxl+1]" (3 processes)
Expected to see assertion:
Collective Assertion of diffusion_seq.c 45.26--45.38: "COMPARE true" (4 processes)
 with:
  Process 0 at location 4: diffusion_seq.c 45.26--45.38: "COMPARE true"
  Process 1 at location 7: ghost.c 98.31--98.106: "GHOSTS v[nxl] == PROC[right].v[0] && v[1] == PROC[left].v[PROC[left].nxl+1]"
  Process 2 at location 4: libmpi.c 169.2--169.26: "send(_tmp, _dest, _tag);"
  Process 3 at location 5 (unknown source)

Trace logged in diffusion_seq_ghost.trace

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