From 1724c1a609d6cf83ad173a3ae90bac4a80f0ca1f Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 4 Apr 2013 15:33:59 +0200
Subject: [PATCH] Fix pc being propagated to ADTSplit's sub problems
---
src/main/scala/leon/synthesis/rules/ADTSplit.scala | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 228923bb4..7dbb9331a 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)
--
GitLab