diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala index f430ceef6329ec7cf53ab2752163a0059479d557..a4eaaa451a2c38a6160624a21d3a8bd518b1ae26 100644 --- a/src/main/scala/leon/synthesis/SynthesisPhase.scala +++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala @@ -99,7 +99,11 @@ object SynthesisPhase extends LeonPhase[Program, Program] { } if (options.manualSearch) { - options = options.copy(rules = rules.AsChoose +: options.rules) + options = options.copy( + rules = rules.AsChoose +: + condabd.rules.ConditionAbductionSynthesisTwoPhase +: + options.rules + ) } options diff --git a/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala b/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala index d1b0622b7cea9b3fb0e0269043bea3fabbba5984..9e7f018ebe5e930f7fe976d4bb5413c314f16cb1 100755 --- a/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala +++ b/src/main/scala/leon/synthesis/condabd/SynthesizerExamples.scala @@ -652,7 +652,6 @@ class SynthesizerForRuleExamples( , _root_.leon.codegen.CodeGenParams(maxFunctionInvocations = 500, checkContracts = true)) val res = _evaluator.eval(newCandidate, exMapping) - println(res) // if (newCandidate.toString contains "tree.value < value") // interactivePause