search

SMT-LIB / benchmark-submission

Repository for the submission of SMT-LIB benchmarks for the 2024 release.
0 stars 13 forks source link

Dolmen warning on reserved solver-generated function symbols #12

Closed Tomaqa closed 5 months ago

Tomaqa commented 5 months ago

On my benchmarks, dolmen produces warnings such as:

Shadowing: `.def_1066` is reserved for solver-generated function symbols other than abstract values

Is this a problem in SMT-COMP?

hansjoergschurr commented 5 months ago

Yes, SMT-LIB problems should not use such symbols, because the solvers should be free to introduce symbols that start with . without having to worry that there is a name-clash with input symbols. Usually it is enough to systematically rename such symbols using sed.

Tomaqa commented 5 months ago

OK. It would be nice if the README states explicitly that not only errors but also warnings of dolmen count.

hansjoergschurr commented 5 months ago

This is a good point. I believe the best option would be to have an option in Dolmen that makes this an error. I will bring this up with the Dolmen maintainers, and we will improve this aspect for next years submission system.