diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala index ca8b32d86762c1f4ecaa838b416aa391a44916be..ba7be35c7170c9226d984140d6ec14585a1bb47c 100644 --- a/src/main/scala/leon/synthesis/Rules.scala +++ b/src/main/scala/leon/synthesis/Rules.scala @@ -137,6 +137,8 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 20) { if (others.isEmpty) { RuleSuccess(Solution(And(exprsA), Tuple(p.xs.map(id => simplestValue(Variable(id)))))) } else { + /* + * Disable for now, it is not that useful anyway val onSuccess: List[Solution] => Solution = { case List(s) => Solution(And(s.pre +: exprsA), s.term) case _ => Solution.none @@ -145,6 +147,8 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 20) { val sub = p.copy(phi = And(others)) RuleDecomposed(List(sub), onSuccess) + */ + RuleInapplicable } } else { RuleInapplicable diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala index 5020c522013cd5c039c339205d40750225430e8d..f8f9f56862b864a26bc0344121f0df11c810428e 100644 --- a/src/main/scala/leon/synthesis/Synthesizer.scala +++ b/src/main/scala/leon/synthesis/Synthesizer.scala @@ -55,11 +55,11 @@ class Synthesizer(val r: Reporter, // current solution if (task.minComplexity < bestSolutionSoFar().complexity) { if (!subProblems.isEmpty) { - val name = Option(task.rule).map(_.name).getOrElse("root") - println("["+name+"] Got: "+task.problem) - println("["+name+"] Decomposed into:") + val prefix = "[%-20s] ".format(Option(task.rule).map(_.name).getOrElse("root")) + println(prefix+"Got: "+task.problem) + println(prefix+"Decomposed into:") for(p <- subProblems) { - println("["+name+"] - "+p) + println(prefix+" - "+p) } }