================================ TASS Error Log ================================
       specification : diffusionSeq (numProcs = 1)
      specSourceFile : examples/collectiveInvariant/diffusion_full/diffusion_seq.c
      implementation : diffusionPar (numProcs = 2)
      implSourceFile : examples/collectiveInvariant/diffusion_full/diffusion_par.c
                mode : COMPARE
              prover : CVC3
            deadlock : IGNORE
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : true
   collectiveAsserts : true
               cqmin : true
        detectCycles : false
          repository : examples/collectiveInvariant/diffusion_full/TASSREP
            frontend : ANTLR
          errorBound : 1
            NX_BOUND = 4


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

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

Error 0: Execution error (kind: ASSERTION_VIOLATION, certainty: PROVEABLE)
Collective assertion LOOP can be violated.
    path condition : X3 >= 0 && X0 + -1*X3 >= 0 && SIZEOF_TYPE(3) + -1 >= 0 && X3 + -1*Y10 >= 0 && Y3[0][0] + -1*Y0[0][0] = 0 && Y3[0][1] + -1*Y0[0][1] = 0 && Y3[0][2] + -1*Y0[0][2] = 0 && Y3[0][3] + -1*Y0[0][3] = 0 && Y3[1][0] + -1*Y0[1][0] = 0 && Y3[1][1] + -1*Y0[1][1] = 0 && Y3[1][2] + -1*Y0[1][2] = 0 && Y3[1][3] + -1*Y0[1][3] = 0 && Y10 + -1 >= 0 && X3 + -1*Y10 + 1 >= 0 && X3 + -1*Y1 >= 0 && Y5[1] + -1*Y2[0] = 0 && Y5[2] + -1*Y2[1] = 0 && Y10 + -1*Y1 = 0 && X3 + -1*Y4 >= 0 && Y4 + -1 >= 0 && X3 + -1*Y4 + 1 >= 0 && Y6[1] + -1*Y2[2] = 0 && Y6[2] + -1*Y2[3] = 0
         assertion : X3 + -1*Y10 >= 0 && Y5[1] + -1*Y2[0] = 0 && Y10 + -1*Y1 = 0 && X3 + -1*Y4 >= 0 && Y6[2] + -1*Y2[3] = 0 && Y1 + -1*Y4 = 0 && Y4 >= 0 && X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + -1*X4*Y2[0] + 2*X4*Y2[1] + -1*X4*Y2[2] + Y5[2] + -1*Y2[1] = 0 && (FORALL __TASS_bound_1.(-1*__TASS_bound_1 + -1 >= 0 || (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]})[Y4]{null,null,X4*Y5[2] + -2*X4*Y6[1] + X4*Y6[2] + Y6[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]})[Y4]{null,null,X4*Y5[2] + -2*X4*Y6[1] + X4*Y6[2] + Y6[1]})[Y4]{null,null,null,Y6[2]})[__TASS_bound_1][0] + -1*(Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]})[Y1]{null,null,X4*Y2[1] + -2*X4*Y2[2] + X4*Y2[3] + Y2[2]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]})[Y1]{null,null,X4*Y2[1] + -2*X4*Y2[2] + X4*Y2[3] + Y2[2]})[Y1]{null,null,null,Y2[3]})[__TASS_bound_1][0] = 0 || __TASS_bound_1 + -1*Y4 + -1 >= 0)) && (FORALL __TASS_bound_1.(-1*__TASS_bound_1 + -1 >= 0 || (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]})[Y4]{null,null,X4*Y5[2] + -2*X4*Y6[1] + X4*Y6[2] + Y6[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]})[Y4]{null,null,X4*Y5[2] + -2*X4*Y6[1] + X4*Y6[2] + Y6[1]})[Y4]{null,null,null,Y6[2]})[__TASS_bound_1][1] + -1*(Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]})[Y1]{null,null,X4*Y2[1] + -2*X4*Y2[2] + X4*Y2[3] + Y2[2]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]})[Y1]{null,null,X4*Y2[1] + -2*X4*Y2[2] + X4*Y2[3] + Y2[2]})[Y1]{null,null,null,Y2[3]})[__TASS_bound_1][1] = 0 || __TASS_bound_1 + -1*Y4 + -1 >= 0)) && (FORALL __TASS_bound_1.(-1*__TASS_bound_1 + -1 >= 0 || (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]})[Y4]{null,null,X4*Y5[2] + -2*X4*Y6[1] + X4*Y6[2] + Y6[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]})[Y4]{null,null,X4*Y5[2] + -2*X4*Y6[1] + X4*Y6[2] + Y6[1]})[Y4]{null,null,null,Y6[2]})[__TASS_bound_1][2] + -1*(Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]})[Y1]{null,null,X4*Y2[1] + -2*X4*Y2[2] + X4*Y2[3] + Y2[2]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]})[Y1]{null,null,X4*Y2[1] + -2*X4*Y2[2] + X4*Y2[3] + Y2[2]})[Y1]{null,null,null,Y2[3]})[__TASS_bound_1][2] = 0 || __TASS_bound_1 + -1*Y4 + -1 >= 0)) && (FORALL __TASS_bound_1.(-1*__TASS_bound_1 + -1 >= 0 || (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]})[Y4]{null,null,X4*Y5[2] + -2*X4*Y6[1] + X4*Y6[2] + Y6[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]} WITH [Y4] := (Y3 WITH [Y4] := Y3[Y4]{Y5[1]})[Y4]{null,X4*Y5[1] + -2*X4*Y5[2] + X4*Y6[1] + Y5[2]})[Y4]{null,null,X4*Y5[2] + -2*X4*Y6[1] + X4*Y6[2] + Y6[1]})[Y4]{null,null,null,Y6[2]})[__TASS_bound_1][3] + -1*(Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]})[Y1]{null,null,X4*Y2[1] + -2*X4*Y2[2] + X4*Y2[3] + Y2[2]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]} WITH [Y1] := (Y0 WITH [Y1] := Y0[Y1]{Y2[0]})[Y1]{null,X4*Y2[0] + -2*X4*Y2[1] + X4*Y2[2] + Y2[1]})[Y1]{null,null,X4*Y2[1] + -2*X4*Y2[2] + X4*Y2[3] + Y2[2]})[Y1]{null,null,null,Y2[3]})[__TASS_bound_1][3] = 0 || __TASS_bound_1 + -1*Y4 + -1 >= 0)) && Y10 >= 0 && X4*Y5[2] + -2*X4*Y6[1] + X4*Y6[2] + -1*X4*Y2[1] + 2*X4*Y2[2] + -1*X4*Y2[3] + Y6[1] + -1*Y2[2] = 0
Source location: diffusion_seq.c 47.29--47.38: "LOOP true"
Trace logged in diffusionSeq-diffusionPar_0.trace

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