Open StefanosChaliasos opened 3 months ago
In some bugs, the sage script is not that useful. We should make sage scripts to produce the malicious witness given some hints.
Most probably, we will be better off using CVC5 with modulo arithmetic theory.
Relevant papers:
ie when using smt or sage to find a solution that passes some manual oracle produce the witness.json file automatically