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.

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

Misc tactics and debugging improvements #3300

Merged
merged 10 commits into from
May 21, 2024
Merged

Misc tactics and debugging improvements #3300

merged 10 commits into from
May 21, 2024

Commits on May 21, 2024

  1. Tc: pretty printing basic_type_error

    @mtzguido
    mtzguido committed May 21, 2024
    Configuration menu
    Copy the full SHA
    c6e8e18 View commit details
    Browse the repository at this point in the history

  2. Tactics: add a ForceSMT guard_policy 

    Forces the guard immediately, raising an exception if it cannot be
discharged, but allows for use of SMT.
    @mtzguido
    mtzguido committed May 21, 2024
    Configuration menu
    Copy the full SHA
    8257736 View commit details
    Browse the repository at this point in the history

  3. Tactics: nit on debug message

    @mtzguido
    mtzguido committed May 21, 2024
    Configuration menu
    Copy the full SHA
    74e4ded View commit details
    Browse the repository at this point in the history

  4. Tactics: minor refactor

    @mtzguido
    mtzguido committed May 21, 2024
    Configuration menu
    Copy the full SHA
    ea6f6af View commit details
    Browse the repository at this point in the history

  5. Syntax.Free: use a binary operator for union 

    Much more readable.
    @mtzguido
    mtzguido committed May 21, 2024
    Configuration menu
    Copy the full SHA
    6a082fa View commit details
    Browse the repository at this point in the history

  6. Syntax.Free: consider vars in residual comp of match

    @mtzguido
    mtzguido committed May 21, 2024
    Configuration menu
    Copy the full SHA
    dcdda27 View commit details
    Browse the repository at this point in the history

  7. Tactics: adding a norm_well_typed_term reflection call

    @mtzguido
    mtzguido committed May 21, 2024
    Configuration menu
    Copy the full SHA
    3da0899 View commit details
    Browse the repository at this point in the history

  8. SMTEncoding: introduce --debug SMTFail to print a diagnostic for fail… 

    …ing queries
    @mtzguido
    mtzguido committed May 21, 2024
    Configuration menu
    Copy the full SHA
    2b7166e View commit details
    Browse the repository at this point in the history

  9. snap

    @mtzguido
    mtzguido committed May 21, 2024
    Configuration menu
    Copy the full SHA
    3c11db4 View commit details
    Browse the repository at this point in the history

  10. Update expected output

    @mtzguido
    mtzguido committed May 21, 2024
    Configuration menu
    Copy the full SHA
    047e0fe View commit details
    Browse the repository at this point in the history