In answer set programming, a program verification task can be sometimes accomplished by transforming rules into first-order sentences so that the task is reduced to reasoning in classical logic, and invoking a resolution theorem prover. The proof assistant anthem, which implements this idea, allows us to reason about programs written in mini-gringo—a subset of the input language of the grounder gringo. The goal of this paper is to extend the syntax of terms permitted in that subset. First, instead of the specific choice of arithmetic functions made in earlier publications on mini-gringo, we approach integer arithmetic in an abstract way, so that different choices are allowed for different dialects of the language. Second, symbolic constants can be used now as function symbols. This generalization preserves the main property of the more limited form of the language established in earlier work: mini-gringo rules can be faithfully represented by first-order sentences.