3 files changed, 61 insertions, 1 deletions
diff --git a/Test/doomed/doomed.bpl b/Test/doomed/doomed.bpl
new file mode 100644
index 00000000..a153e468
--- /dev/null
+++ b/Test/doomed/doomed.bpl
@@ -0,0 +1,27 @@
+
+procedure a(x:int)
+  requires x>0;
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    y := 2;
+  }
+}
+
+
+procedure b(x:int)
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    y := 2;
+  }
+  assert y!=2;
+}
+
+
diff --git a/Test/doomed/notdoomed.bpl b/Test/doomed/notdoomed.bpl
new file mode 100644
index 00000000..86bf76d1
--- /dev/null
+++ b/Test/doomed/notdoomed.bpl
@@ -0,0 +1,28 @@
+procedure a(x:int)
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    y := 2;
+  }
+}
+
+
+procedure b(x:int)
+{
+  var y : int;
+
+  if(x<0) {
+    y := 1;
+  } else {
+    y := 2;
+    assert false;
+  }
+}
+
+
+
+
+
diff --git a/Test/doomed/runtest.bat b/Test/doomed/runtest.bat
index 215804cf..9dda44cf 100644
--- a/Test/doomed/runtest.bat
+++ b/Test/doomed/runtest.bat
@@ -4,7 +4,12 @@ setlocal
 set BOOGIEDIR=..\..\Binaries
 set BGEXE=%BOOGIEDIR%\Boogie.exe
 
-for %%f in (smoke0.bpl) do (
+for %%f in (doomed.bpl) do (
+  echo -------------------- %%f --------------------
+  %BGEXE% /vc:doomed %* %%f
+)
+
+for %%f in (notdoomed.bpl) do (
   echo -------------------- %%f --------------------
   %BGEXE% /vc:doomed %* %%f
 )