================================ TASS Error Log ================================
       specification : laplaceSpec (numProcs = 1)
      specSourceFile : examples/collectiveAssert/laplaceSpec.c
      implementation : laplaceImpl (numProcs = 4)
      implSourceFile : examples/collectiveAssert/laplaceImpl.c
                mode : COMPARE
              prover : CVC3
            deadlock : ABSOLUTE
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : true
               cqmin : true
        detectCycles : false
          repository : examples/collectiveAssert/TASSREP
            frontend : ANTLR
          errorBound : 1
            NX_BOUND = 4
            NY_BOUND = 6
          TIME_BOUND = 3


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

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

Error 0: Execution error (kind: ASSERTION_VIOLATION, certainty: MAYBE)
Cannot prove that collective assertion ERROR holds.
    path condition : X2 > 0  && -1*X2 + 1 > 0  && SIZEOF_TYPE(3) + -1 >= 0 && SIZEOF_TYPE(7) + -1 >= 0 && X3[0][1]^2 + 2*X3[0][1]*X3[1][0] + -8*X3[0][1]*X3[1][1] + 2*X3[0][1]*X3[1][2] + 2*X3[0][1]*X3[2][1] + X3[1][0]^2 + -8*X3[1][0]*X3[1][1] + 2*X3[1][0]*X3[1][2] + 2*X3[1][0]*X3[2][1] + 17*X3[1][1]^2 + -8*X3[1][1]*X3[1][2] + 2*X3[1][1]*X3[2][0] + -16*X3[1][1]*X3[2][1] + 2*X3[1][1]*X3[2][2] + 2*X3[1][1]*X3[3][1] + X3[1][2]^2 + 2*X3[1][2]*X3[2][1] + X3[2][0]^2 + -8*X3[2][0]*X3[2][1] + 2*X3[2][0]*X3[2][2] + 2*X3[2][0]*X3[3][1] + 18*X3[2][1]^2 + -8*X3[2][1]*X3[2][2] + 2*X3[2][1]*X3[3][0] + -16*X3[2][1]*X3[3][1] + 2*X3[2][1]*X3[3][2] + 2*X3[2][1]*X3[4][1] + X3[2][2]^2 + 2*X3[2][2]*X3[3][1] + X3[3][0]^2 + -8*X3[3][0]*X3[3][1] + 2*X3[3][0]*X3[3][2] + 2*X3[3][0]*X3[4][1] + 17*X3[3][1]^2 + -8*X3[3][1]*X3[3][2] + -8*X3[3][1]*X3[4][1] + X3[3][2]^2 + 2*X3[3][2]*X3[4][1] + X3[4][1]^2 + -16*X2 >= 0
         assertion : X3[0][1]^2 + 2*X3[0][1]*X3[1][0] + -8*X3[0][1]*X3[1][1] + 2*X3[0][1]*X3[1][2] + 28/15*X3[0][1]*X3[2][1] + -2/15*X3[0][1]*X3[3][0] + 8/15*X3[0][1]*X3[3][1] + -2/15*X3[0][1]*X3[3][2] + -2/15*X3[0][1]*X3[4][1] + X3[1][0]^2 + -8*X3[1][0]*X3[1][1] + 2*X3[1][0]*X3[1][2] + 28/15*X3[1][0]*X3[2][1] + -2/15*X3[1][0]*X3[3][0] + 8/15*X3[1][0]*X3[3][1] + -2/15*X3[1][0]*X3[3][2] + -2/15*X3[1][0]*X3[4][1] + 254/15*X3[1][1]^2 + -8*X3[1][1]*X3[1][2] + 28/15*X3[1][1]*X3[2][0] + -224/15*X3[1][1]*X3[2][1] + 28/15*X3[1][1]*X3[2][2] + 8/15*X3[1][1]*X3[3][0] + -4/15*X3[1][1]*X3[3][1] + 8/15*X3[1][1]*X3[3][2] + 8/15*X3[1][1]*X3[4][1] + X3[1][2]^2 + 28/15*X3[1][2]*X3[2][1] + -2/15*X3[1][2]*X3[3][0] + 8/15*X3[1][2]*X3[3][1] + -2/15*X3[1][2]*X3[3][2] + -2/15*X3[1][2]*X3[4][1] + 14/15*X3[2][0]^2 + -112/15*X3[2][0]*X3[2][1] + 28/15*X3[2][0]*X3[2][2] + 28/15*X3[2][0]*X3[3][1] + 84/5*X3[2][1]^2 + -112/15*X3[2][1]*X3[2][2] + 28/15*X3[2][1]*X3[3][0] + -224/15*X3[2][1]*X3[3][1] + 28/15*X3[2][1]*X3[3][2] + 28/15*X3[2][1]*X3[4][1] + 14/15*X3[2][2]^2 + 28/15*X3[2][2]*X3[3][1] + X3[3][0]^2 + -8*X3[3][0]*X3[3][1] + 2*X3[3][0]*X3[3][2] + 2*X3[3][0]*X3[4][1] + 254/15*X3[3][1]^2 + -8*X3[3][1]*X3[3][2] + -8*X3[3][1]*X3[4][1] + X3[3][2]^2 + 2*X3[3][2]*X3[4][1] + X3[4][1]^2 = 0
Source location: laplaceSpec.c 64.26--64.36: "ERROR true"
Trace logged in laplaceSpec-laplaceImpl_0.trace

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