Does a finite first-order theory which has a model always have a finite model?
Solution 1:
Noah and Brian have given one of the canonical examples of a finitely axiomatizable theory with no finite model (their examples are essentially the same). I'll give the other - it shows that this behavior is possible even in a relational language without definable functions, so thinking about constant symbols and terms is a red herring (unless you think about Skolemization, as Noah says).
Let $L$ be the language consisting of a single binary relation symbol $\leq$, and let $T$ be the theory asserting that $\leq$ is a non-empty linear order with no greatest element. That is, $T$ contains the three linear order axioms, together with the sentences $\forall x\, \exists y\, (x\leq y\land \lnot (x = y))$ and $\exists x\, x = x$ (to rule out the empty structure, if your semantics for first-order logic allows it).
So it's not true that every finitely axiomatizable theory has a finite model. In fact, the problem of determining whether a given theory has a finite model is undecidable in general. This is known as Trakhtenbrot's theorem.
Time for a tangent: If your guess were correct, and every finitely axiomatizable first-order theory had a finite model, then in fact the decision problem for first-order logic would be decidable. That is, one could write a computer program that takes as input a first-order sentence $\varphi$ and outputs "yes" or "no" according to whether $\varphi$ has a model. This program would start enumerating the finite $L$-structures and checking whether they are models of $\varphi$, while simultaneously searching for proofs of $\lnot \varphi$. If $\varphi$ has no model, a proof of $\lnot\varphi$ will eventually be found (by the completeness theorem), while if $\varphi$ has a model, a finite model will eventually be found.
Of course, the decision problem for first-order logic is well-known to be undecidable. But there are classes of first-order sentences (e.g. in a relational language the universal sentences $\forall \overline{x}\, \varphi(\overline{x})$ with $\varphi$ quantifier-free) which do have the finite model property (if they have a model, then they have a finite model) and hence these classes are decidable by the argument above.
Solution 2:
No, this is incorrect. In the language consisting of a single unary function symbol $f$, consider the following statements about $f$:
$f$ is injective.
$f$ is not surjective.
It is a good exercise to show that these can be written as first-order sentences; but any model of the conjunction of these sentences must be infinite.
The point is that the "constants" you mention are not just things named by constant symbols, but also terms (actually, even broader than this - constant symbols in the larger, "Skolemized" language - but for now it's enough to consider terms). Even a finite language can have infinitely many terms.
Solution 3:
Take a theory with one unary function symbol $f$, one constant symbol $a$, and axioms
$$\begin{align*} &\forall x\Big(\big(\exists y\big(f(y)=x\big)\leftrightarrow x\ne a\Big)\;,\text{ and}\\ &\forall x\,\forall y\big(f(x)=f(y)\to x=y\big)\;. \end{align*}$$
For intuition, think of $\Bbb N$, $0$, and the successor function.