sanity Use Build stability test - makes sure the current build doesn't encounter a runtime error (a smoke test) test0 Use Name resolution tests test1 Use Typechecking tests test2 Use VC generation test7 Use Some tests for VCVariety.BlockNested test20 Use Types introduced in Boogie2 test21 Use Verify Boogie 2 programs aitest0 Use Constant propagation test aitest1 Use Linear ineqality test aitest9 Use Test for the abstract domain of intervals lock Use SLAM example test13 Use error messages for failing asserts vs. loop invariants inline Use Procedure inlining textbook Use Some textbook examples test15 Use Benchmarks for error messages bitvectors Use Smoke tests for bitvectors smoke Use Soundness smoke testing test16 Use Tests loop unrolling codeexpr Use Tests code expressions prover Use Tests checking various prover options test17 Postponed Tests inference of parameterized contracts z3api Postponed Test for Z3 Managed .NET API prover houdini Use Test for Houdini decision procedure datatypes Use Test for datatypes generalizedarray Use Test for generalized array theory livevars Use STORM benchmarks for testing correctness of live variable analysis stratifiedinline Use Stratified inlining benchmarks extractloops Use Extract loops benchmarks havoc0 Use HAVOC-generated bpl files AbsHoudini Postponed Test for abstract houdini snapshots Use Tests for program snapshot verification symdiff Use Tests for symdiff