================================ TASS Error Log ================================
               model : multierr (numProcs = 1)
          sourceFile : examples/multierr/multierr.c
                mode : VERIFY
              prover : CVC3
            deadlock : ABSOLUTE
           reduction : URGENT
            simplify : true
         bufferBound : 10
             verbose : false
         loop method : false
   collectiveAsserts : false
               cqmin : true
        detectCycles : false
          repository : examples/multierr/TASSREP
            frontend : ANTLR
          errorBound : 100


Number of errors reported........... 7
Number of distinct errors........... 6

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

Error 0: Execution error (kind: DIVISION_BY_ZERO, certainty: PROVEABLE)
Denominator in division can be zero:
X0
Source location: multierr.c 14.9--14.13: "10/n"
Trace logged in multierr_0.trace

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

Error 1: Execution error (kind: INT_DIVISION, certainty: PROVEABLE)
It is possible for the denominator of the integer division operation 
to be negative.  This is strongly discouraged:
  denominator    : X0
  path condition : true
Source location: multierr.c 14.9--14.13: "10/n"
Trace logged in multierr_1.trace

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

Error 2: Execution error (kind: ARRAY_DECLARATION, certainty: PROVEABLE)
Extent 0 of array can be negative:
  extent expression  : extent
        extent value : X1
      path condition : X0 != 0 && X0 >= 0
Source location: multierr.c 17.10--17.16: "extent"
Trace logged in multierr_2.trace

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

Error 3: Execution error (kind: OUT_OF_BOUNDS, certainty: PROVEABLE)
It is possible for the array index to be out of bounds:
  array expression : a
  index expression : 3
       index value : 3
      array extent : X1
    path condition : X0 != 0 && X0 >= 0 && X1 >= 0 && X0 + -1 >= 0
Source location: multierr.c 25.1--25.5: "a[3]"
Trace logged in multierr_3.trace

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

Error 4: Execution error (kind: MEMORY_LEAK, certainty: PROVEABLE)
Memory leak detected in process 0 heap cell 0 value:
m0p0h0
Source location: multierr.c 42.0--42.0: "}"
Trace logged in multierr_4.trace

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

Error 5: Execution error (kind: POINTER, certainty: PROVEABLE)
Attempt to call free on a pointer that was not returned by malloc:
&a[0]
Source location: multierr.c 32.1--32.9: "free(q);"
Trace logged in multierr_5.trace

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