Add quantified array abstraction and regression coverage

[cvick32]

Summary

• Add Yardbird-managed abstraction for quantifiers and array lambdas, including witness functions and ground instantiation rules
• Prevent concrete validation and counterexample reporting for quantified inputs
• Preserve background axiom terms across BMC frames and support nested array sort declarations
• Fix round-tripping of quoted reserved SMT-LIB symbols
• Add distributed protocol encoding documentation and regression coverage

Testing

• Added quantifier abstraction, parser, background-term, transition, transcript, and distributed protocol regression tests
• Documented release/debug validation bounds and benchmark results