From a452cb200b78bbf567fdc603817be25cd92a666a Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 29 Apr 2016 18:24:29 +0200
Subject: [PATCH] Focus should add conditions in the right order
---
src/main/scala/leon/repair/rules/Focus.scala | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index 99a248d70..562e1845f 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))
}
--
GitLab