We won CHC Comp again !!! Last year, we had won all tracks except LRA. This time we won ALL tracks, including LRA. Sadly, we did not improve much on LRA. This is still a big TODO.
An interesting addition to this year’s CHC Comp was the ADT track. We were semi-prepared as we have been working on ways to extend Spacer to CHCs with ADTs and RDFs for the past 8 months. Our work is applicable to CHCs over ADTs in addition to other theories like integer arithmetic. However, the benchmarks in the competition were purely over ADTs. They defined sorts like int, nat using ADTs and functions like +, * using RDFs. Spacer did not do too badly even in this scenario, even though it was not designed for this situation.
We submitted a portfolio solver for this years competition. It runs global guidance on one thread and quic3 on another.