Skip to content

Conversation

hgvk94
Copy link
Contributor

@hgvk94 hgvk94 commented Aug 3, 2024

This affects the array solver so please double check if this is the optimal solution.

@NikolajBjorner
Copy link
Contributor

I would change the implementation of is_diseq directly

NikolajBjorner added a commit that referenced this pull request Aug 3, 2024
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
NikolajBjorner added a commit that referenced this pull request Aug 3, 2024
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
Copy link
Contributor

@hgvk94 - this is still in "draft" status

@hgvk94
Copy link
Contributor Author

hgvk94 commented Feb 19, 2025

Looks like your implementation works better than mine. Closing this PR.

@hgvk94 hgvk94 closed this Feb 19, 2025
arbipher pushed a commit to arbipher/z3 that referenced this pull request Apr 17, 2025
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
arbipher pushed a commit to arbipher/z3 that referenced this pull request Apr 17, 2025
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
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

Successfully merging this pull request may close these issues.

2 participants