================================ TASS Error Log ================================
       specification : diffusion_seq_5_2 (numProcs = 1)
      specSourceFile : examples/diffusion/diffusion_seq.c
      implementation : diffusion_par_bad_5_2 (numProcs = 5)
      implSourceFile : examples/diffusion/diffusion_par_bad.c
                mode : COMPARE
              prover : CVC3
            deadlock : IGNORE
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
               cqmin : true
        detectCycles : false
          repository : examples/diffusion/TASSREP
            frontend : ANTLR
          errorBound : 5
            NX_BOUND = 5
        NSTEPS_BOUND = 2


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

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

Error 0: Execution error (kind: FUNCTIONAL_COMPATIBILITY, certainty: PROVEABLE)
It is possible for the final values of implementation and specification to disagree:

Specification  output data[1][1]:
  X3*X1[0] + -2*X3*X1[1] + X3*X1[2] + X1[1]

Implementation output data[1][1]:
  -2*X3*X1[1] + X3*X1[2] + X3*m1p2h1[0] + X1[1]

path condition:
  X4 > 0  && SIZEOF_TYPE(3) + -1 >= 0
 with:
  Process 0: <terminated>
  Process 1: <terminated>
  Process 2: <terminated>
  Process 3: <terminated>
  Process 4: <terminated>
  Process 5: <terminated>

Trace logged in diffusion_seq_5_2-diffusion_par_bad_5_2_0.trace

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