From 67b813154cbd98c1425de4c1f0d1792f8564776b Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 21 Nov 2012 01:41:03 +0100
Subject: [PATCH] Gah, that bug was hard to track down. onSuccess should never
 alter global state, i.e. fundefs' bodies

---
 .../scala/leon/synthesis/heuristics/ADTInduction.scala   | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index 30cbe5bfd..2117dc915 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -36,14 +36,13 @@ class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80)
       }
 
       if (isRecursive) {
-        val newFun = new FunDef(FreshIdentifier("rec", true), resType, VarDecl(inductOn, inductOn.getType) +: residualArgDefs)
 
         val innerPhi = substAll(residualMap + (origId -> Variable(inductOn)), p.phi)
         val innerPC  = substAll(residualMap + (origId -> Variable(inductOn)), p.c)
 
         val subProblemsInfo = for (dcd <- cd.knownDescendents) yield dcd match {
           case ccd : CaseClassDef =>
-            var recCalls = Map[List[Identifier], Expr]()
+            var recCalls = Map[List[Identifier], List[Expr]]()
             var postFs   = List[Expr]()
 
             val newIds = ccd.fieldsIds.map(id => FreshIdentifier(id.name, true).setType(id.getType)).toList
@@ -53,7 +52,7 @@ class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80)
                 val postXs  = p.xs map (id => FreshIdentifier("r", true).setType(id.getType))
                 val postXsMap = (p.xs zip postXs).toMap.mapValues(Variable(_))
 
-                recCalls += postXs -> FunctionInvocation(newFun, Variable(id) +: residualArgs.map(id => Variable(id)))
+                recCalls += postXs -> (Variable(id) +: residualArgs.map(id => Variable(id)))
 
                 postFs ::= substAll(postXsMap + (inductOn -> Variable(id)), innerPhi)
                 id :: postXs
@@ -78,11 +77,13 @@ class ADTInduction(synth: Synthesizer) extends Rule("ADT Induction", synth, 80)
           case sols =>
             var globalPre = List[Expr]()
 
+            val newFun = new FunDef(FreshIdentifier("rec", true), resType, VarDecl(inductOn, inductOn.getType) +: residualArgDefs)
+
             val cases = for ((sol, (problem, pre, ccd, ids, calls)) <- (sols zip subProblemsInfo)) yield {
               globalPre ::= And(pre, sol.pre)
 
               val caze = CaseClassPattern(None, ccd, ids.map(id => WildcardPattern(Some(id))))
-              SimpleCase(caze, calls.foldLeft(sol.term){ case (t, (binders, call)) => LetTuple(binders, call, t) })
+              SimpleCase(caze, calls.foldLeft(sol.term){ case (t, (binders, callargs)) => LetTuple(binders, FunctionInvocation(newFun, callargs), t) })
             }
 
             val funPre = subst(origId -> Variable(inductOn), Or(globalPre))
-- 
GitLab