Unsat cores

[gsingla21]

Does boolector support getting unsat cores? I wasn't able to find the API for the same.

[mpreiner]

Boolector does not provide a boolector_get_unsat_core, but you can have something similar by using boolector_assume instead of boolector_assert and then after an unsat check-sat call query the failed assumptions via boolector_get_failed_assumptions, which will essentially give you an unsat core.

[mpreiner]

@gsingla21 Fyi: Boolector is succeeded by our new solver Bitwuzla (https://github.com/bitwuzla/bitwuzla), which supports unsat cores.