Fix array load-from prefix and from-load axiom

Use s_ldf_prefix in from-load axiom. In addition, the from-load
axiom must compare all stores pair-wise.
Add mutable Tracer::flips()
Allow directional append_guard