| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Scala uses structural equality for case classes); landed first piece of refinement code
|
| |
|
|
| |
(i.e. if function app was inside old, the flag was ignored); != was not properly translated for sequences
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
statement is just like a call statement now
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
unnecessary one
|
| | |
|
| | |
|
| |
|
|
| |
specified
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
revise code comments
|
| | |
|
| |
|
|
| |
either lazyInline or stratifiedInline is greater than 1, the extracted procedure is decorated with the attribute "{:inline 1}". The implementation involved moving the procedure GraphFromImpl from VC.cs to Absy.ssc.
|
| | |
|
| | |
|
| |
|
|
| |
Chalice
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
input).
|
| | |
|
| | |
|
| |
|
|
| |
locally
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
alive though???
|
| |
|
|
| |
-z3bv option to Z3-specific -proverOpt:OPTIMIZE_FOR_BV=true. Start with the prover-specific help (still needs changes in the yet-unconverted part).
|
| | |
|
| | |
|
| |
|
|
| |
for better performance on VCs that are heavy on bitvector arithmetic
|
| | |
|
| |
|
|
| |
svn-ignoring some build artifacts
|
| |
|
|
| |
added classic sqrt refinement; assertions on acc(s[*].f) have now positions attached
|
| | |
|
MichalMoskal