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.

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

Segemation fault when quantifying over polymorphic function #7049

Closed
dewert99 opened this issue Dec 8, 2023 · 0 comments
Closed

Segemation fault when quantifying over polymorphic function #7049

dewert99 opened this issue Dec 8, 2023 · 0 comments

Comments

@dewert99
Copy link

dewert99 commented Dec 8, 2023

Thank you for working on adding support for polymorphism

Running the following smt2 file

(declare-type-var T)
(declare-fun f (T) bool)
(assert (forall ((x Int)) (f x)))
(check-sat)

causes a segmentation fault

This is with Z3 version 4.12.4 - 64 bit

NikolajBjorner added a commit that referenced this issue Dec 14, 2023
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

No branches or pull requests

1 participant