======================== 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
      simplifyProver : false
         bufferBound : 10
             verbose : false
         loop method : false
          repository : examples/diffusion/TASSREP
            frontend : null
          errorBound : 5
            NX_BOUND = 5
        NSTEPS_BOUND = 2


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

------------------------------------------------------------------
Error 0: logged in diffusion_seq_5_2_0.trace, diffusion_par_bad_5_2_0.trace
Execution error (kind: FUNCTIONAL_COMPATIBILITY, certainty: PROVEABLE):
It is possible for the final values of implementation and specification to disagree:
Implementation output variable data at State 1029.

  Expected value : m0v7<0,m0v7[0]<0,X1[0]><1,X1[1]><2,X1[2]>><1,m0v7[1]<0,X1[0]><1,X4*X1[0] + -2*X4*X1[1] + X4*X1[2] + X1[1]><2,X1[2]>><2,m0v7[2]<0,X1[0]><1,-2*X4^2*X1[0] + 4*X4^2*X1[1] + -2*X4^2*X1[2] + 2*X4*X1[0] + -4*X4*X1[1] + 2*X4*X1[2] + X1[1]><2,X1[2]>>

  Actual value   : m1v7<0,m1v7[0]<0,X1[0]><1,X1[1]><2,X1[2]>><1,m1v7[1]<0,X1[0]><1,-2*X4*X1[1] + X4*X1[2] + X4*m1p2h1[0] + X1[1]><2,X1[2]>><2,m1v7[2]<0,X1[0]><1,4*X4^2*X1[1] + -2*X4^2*X1[2] + -2*X4^2*m1p2h1[0] + X4*X1[0] + -4*X4*X1[1] + 2*X4*X1[2] + X4*m1p2h1[0] + X1[1]><2,X1[2]>>

 with:
  Process 0: terminated
  Process 1: terminated
  Process 2: terminated
  Process 3: terminated
  Process 4: terminated

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