A python library to automate the developing of symbolic tests that works on top of Z3 bindings.
- esprima
- z3
- jsbeautifier
You can see some examples of bounded model checking (both in STM-LIB2 and z3py) in doc/examples. The file sample6.py is also available on the official z3 repository
Currently I am developing:
- undefined variables and objects
- the bindings for the JS standard library
- Function call support
- References (and pointers) support
- Multithread support