The verification toolset and intermediate language [Viper](https://www.pm.inf.ethz.ch/research/viper.html) uses a symbolic execution backend as a default: https://github.com/viperproject/silicon Silicon itself uses Z3.
The verification toolset and intermediate language Viper uses a symbolic execution backend as a default: https://github.com/viperproject/silicon
Silicon itself uses Z3.