diff --git a/src/Theory/Constraint/Solver/CaseDistinctions.hs b/src/Theory/Constraint/Solver/CaseDistinctions.hs
--- a/src/Theory/Constraint/Solver/CaseDistinctions.hs
+++ b/src/Theory/Constraint/Solver/CaseDistinctions.hs
@@ -128,8 +128,8 @@
         PremiseG _ fa -> not (isKUFact fa)
         DisjG _       -> doSplit
         -- Uncomment to get more extensive case splitting
-        -- SplitG _   -> doSplit
-        SplitG _      -> False
+        SplitG _   -> doSplit
+        -- SplitG _      -> False
 
     usefulGoal (_, (_, Useful)) = True
     usefulGoal _                = False
diff --git a/tamarin-prover-theory.cabal b/tamarin-prover-theory.cabal
--- a/tamarin-prover-theory.cabal
+++ b/tamarin-prover-theory.cabal
@@ -2,7 +2,7 @@
 
 cabal-version:      >= 1.8
 build-type:         Simple
-version:            0.8.5.0
+version:            0.8.5.1
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers
@@ -60,8 +60,8 @@
       , parallel          >= 3.2
       , HUnit             >= 1.2
 
-      , tamarin-prover-utils >= 0.8.5  && < 0.9
-      , tamarin-prover-term  >= 0.8.5  && < 0.9
+      , tamarin-prover-utils >= 0.8.5.1  && < 0.9
+      , tamarin-prover-term  >= 0.8.5.1  && < 0.9
 
 
     hs-source-dirs: src