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.

Sign up for GitHub

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

Jump to bottom

Proof platform: Better error message when Z3 encoding not supported, and extend GetYear support #227

Merged

denismerigoux merged 2 commits into master from afromher_z3

Mar 15, 2022

Collaborator

R1kM commented Mar 15, 2022 •

edited

Loading

Done with @denismerigoux

This PR relates to the proof platform, and more specifically to the Z3 encoding.
Specifically, it:

Adds a more informative error message when a dcalc construct is not yet supported in the Z3 encoding, by indicating which Catala variable the failing VC is associated with
Extends the support for translating the GetYear operator, by allowing an equality comparison with a literal.

R1kM added 2 commits

March 15, 2022 18:09


          [Z3encoding] Print variable name when encoding is not supported

d760d88


          [Z3Backend] Support GetYear equality comparison

4b1ace2

denismerigoux approved these changes

View reviewed changes

denismerigoux merged commit f3cf8ae into master

R1kM deleted the afromher_z3 branch

March 15, 2022 17:21

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet