diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 228923bb49b4a3d3a6dd6f0374f09cff569fdae0..7dbb9331a4eb79b7a3d5a5b449091dba608636c6 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -51,7 +51,8 @@ case object ADTSplit extends Rule("ADT Split.") {
            val args   = ccd.fieldsIds.map(id => FreshIdentifier(id.name, true).setType(id.getType)).toList
 
            val subPhi = subst(id -> CaseClass(ccd, args.map(Variable(_))), p.phi)
-           val subProblem = Problem(args ::: oas, p.pc, subPhi, p.xs)
+           val subPC  = subst(id -> CaseClass(ccd, args.map(Variable(_))), p.pc)
+           val subProblem = Problem(args ::: oas, subPC, subPhi, p.xs)
            val subPattern = CaseClassPattern(None, ccd, args.map(id => WildcardPattern(Some(id))))
 
            (ccd, subProblem, subPattern)