Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

parse_logic does not recognize QF_FPBV #227

Open
christophejunke opened this issue Feb 24, 2025 · 0 comments
Open

parse_logic does not recognize QF_FPBV #227

christophejunke opened this issue Feb 24, 2025 · 0 comments

Comments

@christophejunke
Copy link

Some benchmarks and solvers apparently support the syntax QF_FPBV (in that order) for QF_BVFP. For example, the following repository has a lot of examples of this:
https://github.com/florianschanda/smtlib_schanda

The code in typecheck/logic.ml seems to require BV to appear first:

and parse_bv c = function

I couldn't find an explicit rule about how logics should be named, but I guess that since this variation occurs in the wild, it might be preferable to support it if possible.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant