Here is the list of submissions I have received for the test runs:
Spacer: all tracks
PCSat: LIA, LIA-Lin
Ultimate Tree Automizer: all tracks
Ultimate Unihorn Automizer: all tracks
Eldarica-abs: LIA, LIA-lin
ic3ia: LIA-lin, LIA-lin-arrays, LRA-TS
Hors Concours: Eldarica: LIA, LIA-lin, LIA-lin-arrays
We have now put online information about the next edition of the competition, CHC-COMP 2021:
The web page in particular lists the tracks we are planning to evaluate, and tentative deadlines for submitting benchmarks, tools, and competition results.
If you are interested in joining CHC-COMP this year, please contact the organizers within the next couple of days, and provide the following pieces of information:
Or feel free to provide this information in this forum.
Of course we hope for a similar number of participants as in the last years, and maybe a couple of new tools as well; please submit in large numbers and make sure that CHC-COMP stays alive!
Best wishes, Grigory & Philipp
ALLcategory? With non linear clauses and quantifier free clause bodies
the following solvers have registered for CHC-COMP 2021:
Golem: LIA-Lin, LRA-TS, LRA-TS-parallel
Spacer: LIA-Lin, LIA-NonLin, LIA-Lin-Arrays, LIA-NonLin-Arrays, LRA-TS, LRA-TS-parallel, ADT-NonLin
PCSat: LIA-Lin, LIA-NonLin, ADT-NonLin
Ultimate TreeAutomizer: LIA-Lin, LIA-NonLin, LIA-Lin-Arrays, LIA-NonLin-Arrays, LRA-TS, LRA-TS-parallel
Ultimate UniHorn: LIA-Lin, LIA-NonLin, LIA-Lin-Arrays, LIA-NonLin-Arrays, LRA-TS, LRA-TS-parallel
Eldarica (HC): LIA-Lin, LIA-NonLin, LIA-Lin-Arrays, LIA-NonLin-Arrays, ADT-NonLin
We removed the ADT-Lin track, since we could not put together a useful set of benchmarks for this track.
The deadline for sending us the final version of the solvers is March 18.
You can find example benchmarks in the CHC space on StarExec, https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=442129
Regards, Grigory & Philipp
Industrytrack for next CHC comp? 😬
abi, you're right.
chc_is_modeldoes not work even for
examples/from repository (it gives
Z3 parsing error)