Skip to content
Snippets Groups Projects
Commit 1330900a authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Nicer that way, one test per choose

parent 78d442b7
No related branches found
No related tags found
No related merge requests found
...@@ -77,28 +77,28 @@ class SynthesisSuite extends FunSuite { ...@@ -77,28 +77,28 @@ class SynthesisSuite extends FunSuite {
fullName fullName
} }
test("Synthesizing %3d: [%s]".format(nextInt(), displayName)) { assert(file.exists && file.isFile && file.canRead,
assert(file.exists && file.isFile && file.canRead, "Benchmark [%s] is not a readable file".format(displayName))
"Benchmark [%s] is not a readable file".format(displayName))
val ctx = LeonContext( val ctx = LeonContext(
settings = Settings( settings = Settings(
synthesis = true, synthesis = true,
xlang = false, xlang = false,
verify = false verify = false
), ),
files = List(file), files = List(file),
reporter = new SilentReporter reporter = new SilentReporter
) )
val opts = SynthesizerOptions() val opts = SynthesizerOptions()
val pipeline = leon.plugin.ExtractionPhase andThen ExtractProblemsPhase val pipeline = leon.plugin.ExtractionPhase andThen ExtractProblemsPhase
val (results, solver) = pipeline.run(ctx)(file.getPath :: Nil) val (results, solver) = pipeline.run(ctx)(file.getPath :: Nil)
for ((f, ps) <- results; p <- ps) { for ((f, ps) <- results; p <- ps) {
test("Synthesizing %3d: %-20s [%s]".format(nextInt(), f.id.toString, displayName)) {
block(solver, f, p) block(solver, f, p)
} }
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment