diff --git a/Settings.hs b/Settings.hs
index add915ea2d1e90ee40447cba442863e17abade2c..8d577fc700fe88c0369065393f4c44f1881e3096 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -1,5 +1,5 @@
 module Settings where
 
-testFile = "test"
-postCond = "true"
+testFile = "switch"
+postCond = "x == 2"
 invariant = "true"
\ No newline at end of file
diff --git a/Tests/switch.java b/Tests/switch.java
new file mode 100644
index 0000000000000000000000000000000000000000..87b08d7dfa91b667885f5576a26309a1ad451baf
--- /dev/null
+++ b/Tests/switch.java
@@ -0,0 +1,20 @@
+public class Class {
+    public static void main(String[] args)
+    {
+        int x, y;
+        
+        y = 0;
+        
+        switch (y) 
+        {
+            case 0:  x = 0;
+            case 1:  x = 1;
+                    break;
+            case 2:  x = 2;
+                     break;
+            default: x = 2;
+                     break;
+        }
+
+    }
+}
\ No newline at end of file
diff --git a/Tests/try-catch-finally.java b/Tests/try-catch-finally.java
index fdeaf100862684f4e2a260e0dfaef15f827c3c19..554e3943158f3635f52090b19dbbfabd159cd47c 100644
--- a/Tests/try-catch-finally.java
+++ b/Tests/try-catch-finally.java
@@ -8,7 +8,7 @@ class MyExc3 extends MyExc2 {}
 public class C1 {
     public static void main(String[] args) throws Exception {
         try {
-            x = 1;
+            int x = 1;
             
             try 
             {
diff --git a/WLP.hs b/WLP.hs
index cb10279868add0799d7ea627a234241b9a31fca3..8c16a290688181268226e9c5d2d192bfb5602586 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -107,13 +107,19 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
     
     -- Converts a switch into nested if-then-else statements. The switch is assumed to be non-trivial.
     desugarSwitch :: Exp -> [SwitchBlock] -> (Exp, Stmt, Stmt)
-    desugarSwitch e [SwitchBlock l bs]       = case l of
-                                                    SwitchCase e' -> (BinOp e Equal e', StmtBlock (Block bs), Empty)
-                                                    Default -> (true, StmtBlock (Block bs), Empty)
-    desugarSwitch e (SwitchBlock l bs:sbs)   = case l of
-                                                    SwitchCase e' -> (BinOp e Equal e', StmtBlock (Block bs), sbscode)
-                                                    Default -> (true, StmtBlock (Block (bs ++ [BlockStmt sbscode])), sbscode)
-        where sbscode = let (e, s1, s2) = desugarSwitch e sbs in IfThenElse e s1 s2
+    desugarSwitch e [SwitchBlock l bs]          = case l of
+                                                    SwitchCase e'   -> (BinOp e Equal e', StmtBlock (Block bs), Empty)
+                                                    Default         -> (true, StmtBlock (Block bs), Empty)
+    desugarSwitch e sbs@(SwitchBlock l bs:sbs') = case l of
+                                                    SwitchCase e'   -> (BinOp e Equal e', StmtBlock (switchBlockToBlock sbs), otherCases)
+                                                    Default         -> (true, StmtBlock (switchBlockToBlock sbs), otherCases)
+        where otherCases = let (e', s1, s2) = desugarSwitch e sbs' in IfThenElse e' s1 s2
+        
+    -- Gets the statements from a switch statement
+    switchBlockToBlock :: [SwitchBlock] -> Block
+    switchBlockToBlock []                       = Block []
+    switchBlockToBlock (SwitchBlock l bs:sbs)   = case switchBlockToBlock sbs of
+                                                    Block b -> Block (bs ++ b)
         
 throwException :: Exp -> Exp
 throwException e = false