Skip to content

Add support for non-incremental mode

Viktor Kuncak requested to merge github/fork/jad-hamza/no-incremental into master

Created by: jad-hamza

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.

Merge request reports