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)
some fixes

In particular, [Symexec.abstract_afs] makes it more complete,
because [Symexec.execute_one_triple] introduces fewer demonic splits.

(with NikosT)
todo note
lightweight matching of spatial parts
bugfix

(with NikosT)
small improvements

(with Rasmus & NikosT)
Merge branch 'alt-abd' into z3integration

Conflicts:
	TODO
	src/prover/expression.ml
	src/prover/expression.mli
	src/prover/prover.ml
	src/symexec/symexec.ml
	tests/infer_tests/cfg.star