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

Jump to bottom

(fmf-fun) Segmentation fault on UFLIA formula #4483

Closed
muchang opened this issue May 9, 2020 · 1 comment · Fixed by #4226
Closed

(fmf-fun) Segmentation fault on UFLIA formula #4483

muchang opened this issue May 9, 2020 · 1 comment · Fixed by #4226
Assignees
@HanielB

Comments

@muchang
Copy link

muchang commented May 9, 2020

Hi,
For this case, CVC4 throws out a segmentation fault:

[567] % cvc4 small.smt2
unknown
[568] % cvc4 --fmf-fun small.smt2
CVC4 suffered a segfault.
Offending address is 0x40
Looks like a NULL pointer was dereferenced.
Aborted
[569] % 
[569] % cat small.smt2
(set-logic ALL)
(declare-fun a (Int) Bool)
(assert (forall ((b (-> Int Int)) (c Int)) (a (b c))))
(check-sat)
[570] %

OS: Ubuntu 18.04
Commit: 00badd3
@ajreynol
Copy link
Member

ajreynol commented May 9, 2020

Probably fixed by #4226.

@ajreynol ajreynol mentioned this issue Jun 1, 2020
Merged
ajreynol added a commit that referenced this issue Jun 2, 2020
@ajreynol
Do not handle universal quantification on functions in model-based FMF (
e492611 
#4226)

Fixes #4225, fixes cvc5/cvc5-projects#159, fixes cvc5/cvc5-projects#157, fixes #4289, fixes #4483.

This makes it so that the main model-based instantiation algorithm is not applied to quantified formulas with universally quantified functions.

Identation changed in a FMF function, this was refactored to conform to guidelines, and further cleaned.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@HanielB HanielB

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Do not handle universal quantification on functions in model-based FMF ajreynol/CVC4
3 participants
@HanielB @ajreynol @muchang