Boogie: Added boolean code expressions (sans well-formedness checks on the input).

1 files changed, 7 insertions, 6 deletions

diff --git a/Test/alltests.txt b/Test/alltests.txt
index 588a5eda..4b12e6fd 100644
--- a/Test/alltests.txt
+++ b/Test/alltests.txt
@@ -1,4 +1,4 @@
-sanity		 Use    Build stability test - makes sure the current build doesn't encounter a runtime error (a smoke test)

+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

@@ -15,15 +15,16 @@ 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 methodology of visible-state semantics and loop unrolling

+test16           Use    Tests loop unrolling

+codeexpr         Use    Tests code expressions

 test17           Postponed    Tests inference of parameterized contracts

 z3api            Postponed    Test for Z3 Managed .NET API prover

 houdini          Postponed    Test for Houdini decision procedure

 dafny0           Use    Dafny functionality tests

-dafny1		 Use	Various Dafny examples

+dafny1           Use    Various Dafny examples

 havoc0           Use    HAVOC-generated bpl files

 VSI-Benchmarks   Use    Solutions to Verified Software Initiative verification challenges

 vacid0           Use    Dafny attempts to VACID Edition 0 benchmarks

-livevars	 Use	STORM benchmarks for testing correctness of live variable analysis

-lazyinline	 Use	Lazy inlining benchmarks

-stratifiedinline	 Use	Stratified inlining benchmarks

+livevars         Use    STORM benchmarks for testing correctness of live variable analysis

+lazyinline       Use    Lazy inlining benchmarks

+stratifiedinline Use    Stratified inlining benchmarks