  There are already quite a few tools for solving the Satisfiability Modulo
Theories (SMT) problems. In this paper, we present \texttt{VolCE}, a tool for
counting the solutions of SMT constraints, or in other words, for computing the
volume of the solution space. Its input is essentially a set of Boolean
combinations of linear constraints, where the numeric variables are either all
integers or all reals, and each variable is bounded. The tool extends SMT
solving with integer solution counting and volume computation/estimation for
convex polytopes. Effective heuristics are adopted, which enable the tool to
deal with high-dimensional problem instances efficiently and accurately.
