usage of extends, unique, and complete

first post: schaef wrote: I'm translating Java into Boogie and I don't seem to understand wha...

latest post: zcheng wrote: aha, that is exactly what I just did. I thought at first that was a...

Discussions are moving to new Boogie mailing list

first post: danliew wrote: Hi All, A new mailing list has been set up for Boogie which can b...

Axiom about global variable

first post: rustanleino wrote: Here is a question I recently received: I have an axiom: axiom (f...

latest post: rustanleino wrote: Axioms are not allowed to have free variables. You have to introdu...

answered by: rustanleino wrote: Axioms are not allowed to have free variables. You have to introdu...

Printing invariants before and after Houdini refinements

first post: Saeed_D wrote: I want to print the program invariants inferred by boogie before a...

Switching to immutable Expr classes

first post: danliew wrote: Hi All, I make heavy use of Boogie's Expr classes in a project I'...

latest post: allydonaldson wrote: I like the idea of immutable expressions. I'm not clear on why the...

Bitvector Expressions are a second class citizen in Boogie and this needs to change

first post: danliew wrote: Hi, Bitvector support really feel like a hack in Boogie You hav...

latest post: allydonaldson wrote: I really like this proposal.

Adding unit tests to Boogie

first post: danliew wrote: Boogie currently doesn't have any unit tests and I think this needs...

latest post: danliew wrote: The unit tests are now in Boogie and are [documented here](https://...

[Dafny]Cannot verify the assertion which is the loop invariant

first post: Yuyan wrote: I specified the LCP problem: (http://rise4fun.com/Dafny/QPa8). I ...

latest post: jiplucap wrote: Hi Rustan, Yes you are right, I just wanted to communicate this sol...

Generating the Z3 model from Boogie file

first post: tsans wrote: Hello, Is it possible to generate the Z3 file from Boogie. I've l...

latest post: tsans wrote: Perfect. Thanks. Small typo, it's "proverLog": ``` $ boogie /prov...

answered by: danliew wrote: I presume you want SMTLIB query that is passed to Z3? If that is th...

Implementing a stack

first post: tsans wrote: Hello, I'm still learning Boogie and I'm hitting another brick wa...

latest post: tsans wrote: I've made some progress but still not there yet. I've defined empty...