2 files changed, 90 insertions, 0 deletions
diff --git a/Test/doomed/runtest.bat b/Test/doomed/runtest.bat
new file mode 100644
index 00000000..215804cf
--- /dev/null
+++ b/Test/doomed/runtest.bat
@@ -0,0 +1,11 @@
+@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set BGEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (smoke0.bpl) do (
+  echo -------------------- %%f --------------------
+  %BGEXE% /vc:doomed %* %%f
+)
+
diff --git a/Test/doomed/smoke0.bpl b/Test/doomed/smoke0.bpl
new file mode 100644
index 00000000..db01233f
--- /dev/null
+++ b/Test/doomed/smoke0.bpl
@@ -0,0 +1,79 @@
+procedure a(x:int)
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    y := 2;
+  }
+}
+
+
+procedure b(x:int)
+  requires x>0;
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    y := 2;
+  }
+}
+
+
+
+procedure c(x:int)
+  requires x>0;
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+    assert false;
+  } else {
+    y := 2;
+  }
+}
+
+procedure d(x:int)
+  requires x>0;
+{
+  var y : int;
+
+  if(x<0) {
+    assert false;
+    y := 1;
+  } else {
+    y := 2;
+  }
+}
+
+
+procedure doomed1(x:int)
+{
+  var y : int;
+  y := 0;
+  if(x<0) {
+    y := 1;
+  } else {
+    assert y!=0;
+  }
+}
+
+
+procedure doomed2(x:int)
+{
+  var y : int;
+  y := 0;
+  if(x!=0) {
+    y := 1;
+  } else {
+    assert x!=0;    
+  }
+}
+
+
+
+