| Commit message (Collapse) | Author | Age |
|
|
|
| |
bitvector values
|
| |
|
| |
|
| |
|
| |
|
| |
|
|\ |
|
| | |
|
| | |
|
|/ |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
caching and prioritization).
|
| |
|
|
|
|
| |
updated answer file
|
|\ |
|
| | |
|
|/ |
|
| |
|
|\ |
|
| | |
|
| |
| |
| |
| | |
typechecking
|
| |\ |
|
|/ / |
|
|/ |
|
|\ |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
few bug fixes, hack to support missing prover declarations.
|
| |
| |
| |
| | |
intervals domain
|
| |
| |
| |
| | |
(all pass)
|
|/ |
|
|
|
|
| |
also added improved error reporting suggested by Chris
|
|
|
|
| |
added another OG sample illustrating rely-guarantee encoding
|
| |
|
| |
|
|
|
|
| |
cleaned up the async type checking
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
Currently only predicate-abstraction domain is supported.
|
| |
|
|
|
|
|
|
|
|
|
| |
- moved doomed and predication code into separate projects;
for doomed there is a static dependency from BoogieDriver
but for predication even that dependency has been eliminated
- deleted Provers\Simplify and Provers\Z3
- removed Provers\Z3api from the solution
- consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs
|