diff --git a/src/test/resources/regression/synthesis/Holes/Hole1.scala b/src/test/resources/regression/synthesis/Holes/Hole1.scala index ce983abae037c19a9fdf57f23d2da612d15269d0..37990792d8b83a2ea1ebbfac0c628487153a5053 100644 --- a/src/test/resources/regression/synthesis/Holes/Hole1.scala +++ b/src/test/resources/regression/synthesis/Holes/Hole1.scala @@ -5,7 +5,7 @@ import leon.collection._ import leon.lang.synthesis._ object Holes { - def abs3(a: Int) = { + def abs3(a: BigInt) = { if (?(a > 0, a < 0)) { a } else { diff --git a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala index b676a3633f5def8701b940e01212a5631b10ab96..723c8319d7290523ad0e660ee722e41f13f226f4 100644 --- a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala +++ b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala @@ -20,33 +20,30 @@ class SynthesisRegressionSuite extends LeonRegressionSuite { } private def testSynthesis(cat: String, f: File, bound: Int) { + val ctx = createLeonContext("--synthesis") - var chooses = List[SourceInfo]() - var program: Program = null - var ctx: LeonContext = null - var opts: SynthesisSettings = null + val pipeline = leon.frontends.scalac.ExtractionPhase andThen new leon.utils.PreprocessingPhase - test(cat+": "+f.getName+" Compilation") { - ctx = createLeonContext("--synthesis") - - opts = SynthesisSettings(searchBound = Some(bound)) - - val pipeline = leon.frontends.scalac.ExtractionPhase andThen new leon.utils.PreprocessingPhase - - val (ctx2, pgm2) = pipeline.run(ctx, f.getAbsolutePath :: Nil) - - program = pgm2 - - chooses = SourceInfo.extractFromProgram(ctx2, program) + val (ctx2, program) = try { + pipeline.run(ctx, f.getAbsolutePath :: Nil) + } catch { + case LeonFatalError(msg) => + test(s"$cat: ${f.getName}") { + fail(s"Compilation failed: ${msg.getOrElse("")}") + } + return } + val chooses = SourceInfo.extractFromProgram(ctx2, program) + val settings = SynthesisSettings(searchBound = Some(bound)) + for (ci <- chooses) { - test(cat+": "+f.getName+" - "+ci.fd.id.name) { - val synthesizer = new Synthesizer(ctx, program, ci, opts) + test(s"$cat: ${f.getName} - ${ci.fd.id.name}") { + val synthesizer = new Synthesizer(ctx, program, ci, settings) try { val (_, sols) = synthesizer.synthesize() if (sols.isEmpty) { - fail("Solution was not found. (Search bound: "+bound+")") + fail(s"Solution was not found. (Search bound: $bound)") } } finally { synthesizer.shutdown()