can angr be configured to use STP instead of Z3 for constraint solving?

angr / claripy

An abstraction layer for constraint solvers.

BSD 2-Clause "Simplified" License

277 stars 90 forks source link

can angr be configured to use STP instead of Z3 for constraint solving? #281

Closed moliam closed 2 years ago

moliam commented 6 years ago

AS TITLE.

zardus commented 6 years ago

We only have a backend for Z3 in claripy. A backend to STP could be written, but nothing like this exists.

rhelmot commented 6 years ago

For reference: here is the z3 backend implementation (the only place z3 is imported in all of angr) and here is the base class with the API that's being implemented.