One of the most difficult aspects in formally verifying infinite
  state systems is reasoning about quantifiers. In this paper, we
  introduce a novel interactive approach to quantifier reasoning using
  an SMT solver. We automatically abstract the verification condition in
  a way that eliminates function cycles. The user refines this
  abstraction in response to spurious counterexamples by proposing
  ground terms to instantiate quantifiers. In applying this approach
  to the verification of Byzantine and non-Byzantine fault tolerance
  protocols, we found that few manual instantiations were
  needed. Moreover, the counterexamples provided valuable guidance for
  the user, in contrast to the timeouts produced by the traditional
  approach.