Skip to content

How to set the boogie keep on verify all the asserts but not stop when it finds some asserts not holds #457

Closed Answered by shazqadeer
Luweicai asked this question in Q&A
Discussion options

You must be logged in to vote

I am going through some of your comments above. It seems like you have some static analysis on the side. This analysis is able to guarantee some facts. You want to provide those facts in the Boogie program in such a way that: (1) Boogie does not attempt to reverify those facts, and (2) Boogie uses those facts in its verification of other facts. Did I understand your intention correctly?

Replies: 10 comments 37 replies

Comment options

You must be logged in to vote
4 replies
@Luweicai
Comment options

@zvonimir
Comment options

@zvonimir
Comment options

@Luweicai
Comment options

Comment options

You must be logged in to vote
2 replies
@Luweicai
Comment options

@shazqadeer
Comment options

Comment options

You must be logged in to vote
2 replies
@Luweicai
Comment options

@shazqadeer
Comment options

Comment options

You must be logged in to vote
9 replies
@Luweicai
Comment options

@shazqadeer
Comment options

@Luweicai
Comment options

@Luweicai
Comment options

@shazqadeer
Comment options

Comment options

You must be logged in to vote
4 replies
@Luweicai
Comment options

@shazqadeer
Comment options

@Luweicai
Comment options

@Luweicai
Comment options

Answer selected by Luweicai
Comment options

You must be logged in to vote
0 replies
Comment options

You must be logged in to vote
1 reply
@Luweicai
Comment options

Comment options

You must be logged in to vote
3 replies
@rakamaric
Comment options

@Luweicai
Comment options

@Luweicai
Comment options

Comment options

You must be logged in to vote
10 replies
@shazqadeer
Comment options

@Luweicai
Comment options

@shazqadeer
Comment options

@Luweicai
Comment options

@shazqadeer
Comment options

Comment options

You must be logged in to vote
2 replies
@shazqadeer
Comment options

@Luweicai
Comment options

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Category
Q&A
Labels
None yet
5 participants