Skip to content

Issues: verifast/verifast

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

Clear current search query, filters, and sorts
19 Open 22 Closed
19 Open 22 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Error: Sort mismatch at argument #1 for function (declare-fun |(int)| (inductive) Int) supplied sort is Int
#182 by necto was closed Aug 29, 2019
Z3v4.5 forgets conclusions of autolemmas triggered by terms constructed while executing an assert statement
#157 by necto was closed Feb 23, 2019
5
labs and llabs support
#154 by necto was closed Mar 14, 2019
Disallow nonpositive fractions
#153 opened Feb 4, 2019 by necto
6
Exception failure when defining SIZE_MAX macro and include stdint.h
#151 by necto was closed Jan 6, 2019
2
Feature request: trivial fixpoint equality
#149 opened Jan 2, 2019 by necto
1
Feature Request: Support for ghost typedef
#148 opened Dec 7, 2018 by necto
1
Is there a way to list all the "unsatisfied requirement"s with verifast?
#126 by necto was closed Mar 19, 2018
2
vfide build fails with
#111 by necto was closed Jan 8, 2018
2
redux crashes on a query with nth and inductive datatype.
#110 by necto was closed Dec 27, 2020
1
[z3v4.5] fails to prove equality involving complex list manipulations
#109 opened Jan 7, 2018 by necto
*&p is not equivalent to p
#85 opened May 8, 2017 by necto
2
Why does not VeriFast use CIL parser?
#82 opened Mar 17, 2017 by necto
3
assertion might not hold (0 == (0x01 & 0x10))
#81 opened Jan 11, 2017 by necto
4
Redux crashes when a term like 'default_value' is used at different types
#68 by necto was closed Dec 27, 2020
4
Increment array cell: -> Fatal error. (unhelpful crash message)
#67 by necto was closed Nov 25, 2016
Recursive fixpoint: Inductive argument is not detected as a switch pattern var.
#54 opened Oct 30, 2016 by necto
2
VeriFast "forgets" loop invariant on loop exit.
#52 by necto was closed Oct 19, 2016
7
How to prove 0 < x => 0/x == 0 ?
#51 by necto was closed Oct 18, 2016
2
SMT solver incompleteness due to trigger premise checking
#49 by necto was closed Oct 12, 2016
1
Z3 support?
#48 by necto was closed Jan 7, 2018
2
[feature request] Dereferencing pointers of type uint16 is not yet supported.
#42 by necto was closed Sep 2, 2016
3
How to add two uint16_t numbers?
#41 opened Aug 24, 2016 by necto
5
support for array typedefs
#40 opened Aug 7, 2016 by necto
Arrays in structures: "Parse error: Array cannot be of this type."
#39 by necto was closed Aug 8, 2016
ProTip! Type g i on any issue or pull request to go back to the issue listing page.