1 files changed, 0 insertions, 121 deletions
diff --git a/Chalice/tests/general-tests/SmokeTestTest.chalice b/Chalice/tests/general-tests/SmokeTestTest.chalice
deleted file mode 100644
index 6ff283ec..00000000
--- a/Chalice/tests/general-tests/SmokeTestTest.chalice
+++ /dev/null
@@ -1,121 +0,0 @@
-// This file is meant as a test for Chalice's smoke testing feature (command line switch -smoke)
-class Cell {
-  var f: int;
-  
-  invariant acc(this.f) && f == 1
-  invariant f == 2 // SMOKE: contradiction
-  
-  method a1()
-    requires false // SMOKE: precondition is false
-  {}
-  
-  method a2()
-    requires acc(this.f,-2) // SMOKE: precondition is equivalent to false
-  {}
-  
-  method a3()
-    requires acc(this.f)
-  {
-    if (this.f > 0) {
-      this.f := 0;
-    }
-  }
-  
-  method a4()
-    requires acc(this.f)
-  {
-    if (false) {
-      this.f := 0; // SMOKE: unreachable
-    }
-  }
-  
-  method a5()
-    requires acc(this.f)
-  {
-    if (true) {
-      this.f := 0;
-    }
-  }
-  
-  method a6()
-    requires acc(this.f)
-  {
-    if (false) {
-      this.f := 0; // SMOKE: unreachable
-    } else {
-      this.f := 1;
-    }
-  }
-  
-  method a7(i: int, j: int)
-    requires i != j;
-  {
-    assume i == j; // SMOKE: introduces contradiction
-  }
-  
-  method a8()
-    requires acc(this.f)
-  {
-    while (true)
-      invariant acc(this.f)
-    {
-      this.f := this.f + 1
-    }
-    // SMOKE: unreachable, loop does not terminate
-  }
-  
-  method a9()
-    requires acc(this.f)
-  {
-    call a8()
-  }
-  
-  method a10()
-    requires acc(this.f)
-  {
-    if (true) {
-      this.f := 0;
-    } else {
-      this.f := 1; // SMOKE: unreachable
-    }
-  }
-  
-  function f1(): int
-    requires false // SMOKE: precondition is false
-  { 1 }
-  
-  method a11()
-  {
-    var i: int := 0
-    if (false) {
-      // SMOKE: unreachable
-    } else {
-      if (true) { assume false } // SMOKE: introduces contradiction
-      else { assume i == 1 } // SMOKE: introduces contradiction
-    }
-  }
-  
-  method a12()
-  {
-    assume false // SMOKE: introduces contradiction
-    while (false) {
-    
-    }
-  }
-  
-  method a13()
-    ensures false // ERROR: cannot prove false
-  {
-  }
-  
-  method a14()
-  {
-    call a13(); // SMOKE: statements afterwards not reachable anymore
-  }
-  
-  predicate valid {
-    1 == 2 // SMOKE: contradiction
-  }
-}
-
-channel C(msg: bool) where msg && !msg // SMOKE: contradiction
-\ No newline at end of file