This paper describes the operation and implementation of the arithmetic proof rule for the quantifier free integer arithmetic used in the PL/CV 2 program verification system. The general arithmetic satisfiability problem underlying the rule is shown to be NP complete.