search

epfl-lara / inox

Solver for higher-order functional programs, used by Stainless
Apache License 2.0
88 stars 20 forks source link

Add support for non-incremental mode #140

Closed jad-hamza closed 3 years ago

jad-hamza commented 3 years ago

Thanks @samarion for the help

Built on top of https://github.com/epfl-lara/inox/pull/137

I wonder now if it wouldn't have been better to make new solver names such as noinc:smt-z3 instead of one global option. That way we could mix incremental and non-incremental solvers in one run. But this will do for now, I'll that for a future PR.