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

invariant for relationAnalysis: Lincons with fractional coefficients not outputted #1328

Closed
michael-schwarz opened this issue Jan 13, 2024 · 0 comments · Fixed by #1493
Closed

invariant for relationAnalysis: Lincons with fractional coefficients not outputted #1328

michael-schwarz opened this issue Jan 13, 2024 · 0 comments · Fixed by #1493
Assignees
@DrMichaelPetter
Labels
bug feature relational Relational analyses (Apron, affeq, lin2var) sv-comp SV-COMP (analyses, results), witnesses
Milestone
SV-COMP 2025

Comments

@michael-schwarz
Copy link
Member

[...] The invariant is given as i#318-1/3j#319+1/3k#320+4/3=0 which then likely does not survive conversion to a CIL expression. I suggest we open a new issue, as this is a general problem of relationAnalysis [...]

Originally posted by @michael-schwarz in #1327 (comment)
@michael-schwarz michael-schwarz added feature bug sv-comp SV-COMP (analyses, results), witnesses labels Jan 13, 2024
@michael-schwarz michael-schwarz added the relational Relational analyses (Apron, affeq, lin2var) label Jan 26, 2024
@DrMichaelPetter DrMichaelPetter mentioned this issue May 28, 2024
Merged
@sim642 sim642 added this to the SV-COMP 2025 milestone Jul 2, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@DrMichaelPetter DrMichaelPetter

Labels
bug feature relational Relational analyses (Apron, affeq, lin2var) sv-comp SV-COMP (analyses, results), witnesses
Projects
None yet
Milestone
SV-COMP 2025
Development

Successfully merging a pull request may close this issue.

make cil_exp_of_linexpr1 work with fractional expressions goblint/analyzer
3 participants
@sim642 @DrMichaelPetter @michael-schwarz