This project is intended as a reimplementation of "Stochastic Local Search for Satisfiability Modulo Theories" in Racket. But now it serves as an incomplete QF_(BV)FP solver.

Just Racket (what else should you need?)

Maybe Z3, too. Z3 needs to be installed if the options --try-real-models and --elim-eqs are enabled.

See racket main.rkt -h