Answering because all the existing answers say that it's undefined behaviour, which is not true, so I have nothing I can upvote.
In C89 (thanks to pmg for the reference to a draft standard), 5.1.2.2.3:
A return from the initial call to the
  main function  is
  equivalent  to  calling  the  exit  function  with the value
  returned by the main function as its argument. If  the  }
  that   terminates   the   main   function  is  reached,  the
  termination status  returned  to  the  host  environment  is
  unspecified.
In C99, quoting from n1256, 5.1.2.2.3:
If the return type of the main
  function is a type compatible with
  int, a return from the initial call to
  the main function is equivalent to
  calling the exit function with the
  value returned by the main function as
  its argument; reaching the } that
  terminates the main function returns a
  value of 0. If the return type is not
  compatible with int, the termination
  status returned to the host
  environment is unspecified.
So, it's not "undefined behaviour": it behaves as if the main function returns, but in C89 the value returned is not specified by the standard. For your example program, on your implementation, the value returned appears to consistently be 12, presumably for the reason Ben Voigt says. Since you're on linux, it's probably not a big change to compile your code as C99 (or anyway, compile it using gcc's almost-compliant C99 mode).
For any function that returns a value, other than main, it is undefined behaviour, unless the caller doesn't use the return value (n1256, 6.9.1/12):
If the } that terminates a function is
  reached, and the value of the function
  call is used by the caller, the
  behavior is undefined.
I'm not sure whether the initial call to main should be mentioned as excluded from this general rule. It doesn't need to be: from the POV of the standard, that call doesn't have a caller, so I think that the value of the function call is not "used by the caller", even though it becomes the termination status for the program.