Fix symbolic naming bug
Fill in gaps in Terms<T>
Add unsat core interface and Z3 implementation
Use vector for guards
Create standalone RAII class for solver push/pop
Introduce non-chronological symbolic execution

This new symbolic execution technique leverages the "unsat core"
to reduce the number of SAT solver calls. The idea is inspired by
non-chronological backtracking in modern SAT solvers where decisions
are reversed based on a conflict analysis of the implication graph.
In symbolic execution, decisions correspond to branches.