Skip to content

Tests: more tests for dumping SMTLIB for quantified formulas.#573

Open
kfriedberger wants to merge 1 commit intomasterfrom
450-smtlib2-output-consistency-for-quantified-terms
Open

Tests: more tests for dumping SMTLIB for quantified formulas.#573
kfriedberger wants to merge 1 commit intomasterfrom
450-smtlib2-output-consistency-for-quantified-terms

Conversation

@kfriedberger
Copy link
Member

See #450

@kfriedberger kfriedberger linked an issue Jan 1, 2026 that may be closed by this pull request
@baierd
Copy link
Contributor

baierd commented Jan 19, 2026

I really like this! Do you still want to add more or is this done?

Also, I remember @daniel-raffler told me that setting the weight to 1 in Z3 might remove the weighting from the output. Do we want to try this?

@kfriedberger
Copy link
Member Author

kfriedberger commented Jan 24, 2026

This PR was just intended to implement tests for issue #450 . It does not yet solve any problem.

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

Labels

None yet

Development

Successfully merging this pull request may close these issues.

SMTLib2 Output Consistency for Quantified Terms

2 participants