In this paper, we improve the algorithms of Lauder-Wan \cite{LW} and Harvey
\cite{Ha} to compute the zeta function of a system of $m$ polynomial equations
in $n$ variables over the finite field $\FF_q$ of $q$ elements, for $m$ large.
The dependence on $m$ in the original algorithms was exponential in $m$. Our
main result is a reduction of the exponential dependence on $m$ to a polynomial
dependence on $m$. As an application, we speed up a doubly exponential time
algorithm from a software verification paper \cite{BJK} (on universal
equivalence of programs over finite fields) to singly exponential time. One key
new ingredient is an effective version of the classical Kronecker theorem which
(set-theoretically) reduces the number of defining equations for a "large"
polynomial system over $\FF_q$ when $q$ is suitably large.