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

Make functional congruence constraints optional #881

Merged

daniel-larraz merged 3 commits into kind2-mc:develop from daniel-larraz:enforce-func-congruence

Apr 12, 2022

Contributor

daniel-larraz commented Apr 6, 2022 •

edited

Loading

Now functional congruence is only enforced on abstract functions when --enforce_func_congruence is true (default value: false).

daniel-larraz added 3 commits

April 6, 2022 15:25


          Add flag to enforce functional congruence on abstract functions

5a9dfc2


          Document new flag and default behaviour on abstract functions

524b398


          Run regression tests with --enforce_func_congruence set to true

a010db2

daniel-larraz mentioned this pull request

When calling a node with a contract, guarantee is not always provable #736

Open

daniel-larraz merged commit 7476b5f into kind2-mc:develop

daniel-larraz deleted the enforce-func-congruence branch

January 5, 2023 10:06

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

Labels

None yet