在 SMT-LIB 语言 1.2 之前的版本中，允许重载用户定义的符号。自标准 2.0 版以来，重载仅限于理论符号。
尽管如此，一些 SMT 求解器仍然允许重载用户定义的符号，这恰好对我的用例很方便：证明义务很容易通过重载自动生成，而不是没有......我想将 cvc4 添加到我的投资组合中的 SMT 求解器，但我发现它会在重载的用户符号上产生解析错误。
我知道这是符合 SMT-LIB 标准的正确方法，但我想知道以下内容：CVC4 是否有一个选项可以禁用此类检查以及解析器能够消除重载用户符号的歧义？