In versions through 1.2 of the SMT-LIB language, overloading of user-defined symbols was allowed. Since version 2.0 of standard, overloading is restricted to theory symbol.
Nevertheless, some SMT-solvers still allow overloading of user-defined symbols and that happens to be handy for my use case: proof obligations are easily generated automatically with overloading, not so much without... I would like to add cvc4 to my portfolio of SMT solvers, but I found out that it produces a parsing error on overloaded user-symbols.
I am aware that this is the correct way to be compliant with the SMT-LIB standard, but I would like to know the following: Is there an option to CVC4 that disables such check and where the parser is able to disambiguate overloaded user symbols?
Unfortunately, CVC4 does not have an option to support overloaded user symbols. Each user symbol must be unique.