Automate the exploit generation process

[StefanosChaliasos]

ie when using smt or sage to find a solution that passes some manual oracle produce the witness.json file automatically

[StefanosChaliasos]

In some bugs, the sage script is not that useful. We should make sage scripts to produce the malicious witness given some hints.

[StefanosChaliasos]

Most probably, we will be better off using CVC5 with modulo arithmetic theory.

Relevant papers:

• An SMT-LIB Theory of Finite Fields
• Split Gröbner Bases for Satisfiability Modulo Finite Fields