ASTREE focuses on numerical programs and corresponding abstract domains (due to its focus on avionics), but abstract interpretation as a concept can be used to formalize essentially any program analysis. What would it take to turn ASTREE into a symbolic execution engine? In particular, what would be the abstract domain, transfer function, and widening operator? What are the benefits and limitations of the resulting engine when compared to KLEE?