diff --git a/src/main/scala/leon/synthesis/Search.scala b/src/main/scala/leon/synthesis/Search.scala index e9501009d89730cfccd6694f27d518c81cd52c4d..15efbc18f36377e2478f6479a3ada9c01ae11c63 100644 --- a/src/main/scala/leon/synthesis/Search.scala +++ b/src/main/scala/leon/synthesis/Search.scala @@ -11,7 +11,9 @@ import scala.annotation.tailrec import leon.utils.Interruptible import java.util.concurrent.atomic.AtomicBoolean -class Search(val ctx: LeonContext, ci: SourceInfo, p: Problem, val strat: Strategy) extends Interruptible { +class Search(val ctx: LeonContext, ci: SourceInfo, val strat: Strategy) extends Interruptible { + + val p: Problem = ci.problem val g = new Graph(p) val interrupted = new AtomicBoolean(false) diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala index 8baabbe2574fb80f78e606bb047d3c7b717d6752..c9be0bf707f930a6a2c126a8a42c341c5069037e 100644 --- a/src/main/scala/leon/synthesis/Synthesizer.scala +++ b/src/main/scala/leon/synthesis/Synthesizer.scala @@ -20,8 +20,6 @@ class Synthesizer(val context : LeonContext, val ci: SourceInfo, val settings: SynthesisSettings) { - val problem = ci.problem - val reporter = context.reporter lazy val sctx = new SynthesisContext(context, settings, ci.fd, program) @@ -44,14 +42,14 @@ class Synthesizer(val context : LeonContext, strat1 } - new Search(context, ci, problem, strat2) + new Search(context, ci, strat2) } private var lastTime: Long = 0 def synthesize(): (Search, Stream[Solution]) = { reporter.ifDebug { printer => - printer(problem.eb.asString("Tests available for synthesis")(context)) + printer(ci.problem.eb.asString("Tests available for synthesis")(context)) } val s = getSearch diff --git a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala index 72bc14f658c9bfb4467256e20101187c805a2871..681ac62872148afbdcc7e78ebc8b043dff74cf0f 100644 --- a/src/test/scala/leon/integration/solvers/StringRenderSuite.scala +++ b/src/test/scala/leon/integration/solvers/StringRenderSuite.scala @@ -85,7 +85,7 @@ class StringRenderSuite extends LeonTestSuiteWithProgram with Matchers with Scal def applyStringRenderOn(functionName: String): (FunDef, Program) = { val ci = synthesisInfos(functionName) - val search = new Search(ctx, ci, ci.problem, new CostBasedStrategy(ctx, CostModels.default)) + val search = new Search(ctx, ci, new CostBasedStrategy(ctx, CostModels.default)) val synth = new Synthesizer(ctx, program, ci, SynthesisSettings(rules = Seq(StringRender))) val orNode = search.g.root if (!orNode.isExpanded) {