In 2020 we only had a word-level track based on the BTOR2 format, which is described in our CAV'18 paper. The Btor2Tools tool suite provides a generic parser Btor2Parser and a simulator BtorSIM, which are useful for parsing and random simulation of BTOR2 models, as well as for witness checking. There is also a simple bounded model checker BtorMC, distributed as part of Boolector.
Due to the low number of submissions of AIGER model checkers we did not run a single safety property track using the AIGER format as in earlier competitions until 2017. Instead we were running model checkers only supporting the AIGER format on bit-blasted word-level models. This allowed to compare AIGER model checker directly with word-level model checkers, exept that we can not bit-blast arrays which puts AIGER model checker at a big disadvantage in the overall ranking.
Forschungs-