================================ 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 : MINIMP
          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:
Implementation output variable data at State 1595.

  Expected value : m0v6<0,m0v6[0]<0,X1[0]><1,X1[1]><2,X1[2]>><1,m0v6[1]<0,X1[0]><1,X3*X1[0] + -2*X3*X1[1] + X3*X1[2] + X1[1]><2,X1[2]>><2,m0v6[2]<0,X1[0]><1,-2*X3^2*X1[0] + 4*X3^2*X1[1] + -2*X3^2*X1[2] + 2*X3*X1[0] + -4*X3*X1[1] + 2*X3*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*X3*X1[1] + X3*X1[2] + X3*m1p2h1[0] + X1[1]><2,X1[2]>><2,m1v7[2]<0,X1[0]><1,4*X3^2*X1[1] + -2*X3^2*X1[2] + -2*X3^2*m1p2h1[0] + X3*X1[0] + -4*X3*X1[1] + 2*X3*X1[2] + X3*m1p2h1[0] + X1[1]><2,X1[2]>>

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

Trace logged in diffusion_seq_5_2_0.trace, diffusion_par_bad_5_2_0.trace

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