simultaneous guessing

guessing instances one-by-one doesn't play well with how symbolic
execution interprets proofs (namely, demonic split on
(antiframe, frame) pairs)

(with Rasmus)