diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala index 99a248d708367fcc0f68ba7dfe1bb1bd7816289a..562e1845f9099ab38da406d6704304fe9723bc3f 100644 --- a/src/main/scala/leon/repair/rules/Focus.scala +++ b/src/main/scala/leon/repair/rules/Focus.scala @@ -170,7 +170,7 @@ case object Focus extends PreprocessingRule("Focus") { eb2.eb } - val newPc = Path.empty withBindings vars.map(id => id -> map(id)).toSeq merge cond + val newPc = cond withBindings vars.map(id => id -> map(id)) Some(Problem(p.as, ws(c.rhs), p.pc merge newPc, p.phi, p.xs, eb3)) } else { @@ -187,9 +187,9 @@ case object Focus extends PreprocessingRule("Focus") { if (existsFailing(elsePc.toClause, Map(), evaluator)) { val newCase = MatchCase(WildcardPattern(None), None, NoTree(scrut.getType)) - val eb = qeb.filterIns(elsePc.toClause) + val qeb2 = qeb.filterIns(elsePc.toClause) - val newProblem = Problem(p.as, andJoin(wss), p.pc merge elsePc, p.phi, p.xs, eb) + val newProblem = Problem(p.as, andJoin(wss), p.pc merge elsePc, p.phi, p.xs, qeb2) casesInfos :+= (newCase -> (Some(newProblem), elsePc)) }