Enabled smoke lit test.

2 files changed, 24 insertions, 0 deletions

diff --git a/Test/smoke/smoke0.bpl b/Test/smoke/smoke0.bpl
index 85deb324..7fb4f6fe 100644
--- a/Test/smoke/smoke0.bpl
+++ b/Test/smoke/smoke0.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -smoke %s > %t

+// RUN: %diff %s.expect %t

 procedure a(x:int)

 {

   var y : int;

diff --git a/Test/smoke/smoke0.bpl.expect b/Test/smoke/smoke0.bpl.expect
new file mode 100644
index 00000000..fff67ab8
--- /dev/null
+++ b/Test/smoke/smoke0.bpl.expect
@@ -0,0 +1,22 @@
+found unreachable code:
+implementation b(x: int)
+{
+  var y: int;
+
+
+  0:
+    goto anon0;
+
+  anon0:
+    goto anon3_Then;
+
+  anon3_Then:
+    assume {:partition} x < 0;
+    y := 1;
+    assert false;
+    return;
+}
+
+
+
+Boogie program verifier finished with 4 verified, 0 errors