diff --git a/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala b/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
index da717fe778a33335ad77845ebbad7af97d649f65..72bffc37c94b5791af3b16582e3d6a4e740c90c5 100644
--- a/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala
@@ -155,7 +155,7 @@ class CegisCore(ctx: InferenceContext,
}
val t3 = System.currentTimeMillis()
val elapsedTime = (t3 - startTime)
- val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver),
+ val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extededUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver),
timeoutMillis - elapsedTime))
val (res1, newModel) = if (solveAsInt) {
val intctr = And(newctr, initRealCtr)
@@ -214,7 +214,7 @@ class CegisCore(ctx: InferenceContext,
val debugMinimization = false
def minimizeReals(inputCtr: Expr, objective: Expr): (Option[Boolean], Model) = {
- val sol = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
+ val sol = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extendedUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
val (res, model1) = sol.solveSAT(inputCtr)
res match {
case Some(true) => {
@@ -253,7 +253,7 @@ class CegisCore(ctx: InferenceContext,
}
val boundCtr = LessEquals(objective, currval)
- val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
+ val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extendedUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
val (res, newModel) = sol.solveSAT(And(inputCtr, boundCtr))
res match {
case Some(true) => {
@@ -296,7 +296,7 @@ class CegisCore(ctx: InferenceContext,
}
def minimizeIntegers(inputCtr: Expr, objective: Expr): (Option[Boolean], Model) = {
- val sol = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
+ val sol = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extendedUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
val (res, model1) = sol.solveSAT(inputCtr)
res match {
case Some(true) => {
@@ -328,7 +328,7 @@ class CegisCore(ctx: InferenceContext,
} else 2 * upperBound
}
val boundCtr = LessEquals(objective, InfiniteIntegerLiteral(currval))
- val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
+ val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extededUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
val (res, newModel) = sol.solveSAT(And(inputCtr, boundCtr))
res match {
case Some(true) => {
@@ -367,4 +367,4 @@ class CegisCore(ctx: InferenceContext,
}
}
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
index 5831fcda02e1a14e9f0aa6bb0085b6b87fbcc22e..11a560be07ec4c678ad479971dedd8a079149f88 100644
--- a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
@@ -273,8 +273,9 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
//new ExtendedUFSolver(leonctx, program, useBitvectors = true, bitvecSize = bvsize) with TimeoutSolver
} else {
//new AbortableSolver(() => new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver, ctx)
- SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() =>
- new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver), timeout * 1000))
+ SimpleSolverAPI(new TimeoutSolverFactory(
+ SolverFactory.getFromName(leonctx, program)("smt-z3-u"),
+ timeout * 1000))
}
if (verbose) reporter.info("solving...")
val (res, model) =
@@ -324,4 +325,4 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
(res, model)
}
}
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala b/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala
index b22f402ae5180edcb7efb5ec7e9997e9c1eaf174..3e40886a549b4685dc3597ddd36754708d54371e 100644
--- a/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala
@@ -63,8 +63,9 @@ class UniversalQuantificationSolver(ctx: InferenceContext, program: Program,
if (usePortfolio) {
if (useIncrementalSolvingForVCs)
throw new IllegalArgumentException("Cannot perform incremental solving with portfolio solvers!")
- SolverFactory(() => new PortfolioSolver(leonctx, Seq(new SMTLIBCVC4Solver(leonctx, program),
- new SMTLIBZ3Solver(leonctx, program))) with TimeoutSolver)
+ new PortfolioSolverFactory(leonctx, Seq(
+ SolverFactory.getFromName(leonctx, program)("smt-cvc4-u"),
+ SolverFactory.getFromName(leonctx, program)("smt-z3-u")))
} else
SolverFactory.uninterpreted(leonctx, program)
@@ -360,7 +361,7 @@ class UniversalQuantificationSolver(ctx: InferenceContext, program: Program,
solver.pop()
solRes
} else
- SimpleSolverAPI(SolverFactory(() => solver)).solveSAT(instExpr)
+ SimpleSolverAPI(SolverFactory(solver.name, () => solver)).solveSAT(instExpr)
} { vccTime =>
if (verbose) reporter.info("checked VC inst... in " + vccTime / 1000.0 + "s")
updateCounterTime(vccTime, "VC-check-time", "disjuncts")
@@ -370,7 +371,7 @@ class UniversalQuantificationSolver(ctx: InferenceContext, program: Program,
/*ctrTracker.getVC(fd).checkUnflattening(tempVarMap,
SimpleSolverAPI(SolverFactory(() => solverFactory.getNewSolver())),
defaultEval)*/
- verifyModel(funData.simpleParts, packedModel, SimpleSolverAPI(SolverFactory(() => solverFactory.getNewSolver())))
+ verifyModel(funData.simpleParts, packedModel, SimpleSolverAPI(solverFactory))
//val unflatPath = ctrTracker.getVC(fd).pickSatFromUnflatFormula(funData.simpleParts, packedModel, defaultEval)
}
//for statistics
@@ -379,7 +380,7 @@ class UniversalQuantificationSolver(ctx: InferenceContext, program: Program,
unflatten(simplifyArithmetic(instantiateTemplate(ctrTracker.getVC(fd).eliminateBlockers, tempVarMap)))
Stats.updateCounterStats(atomNum(compressedVC), "Compressed-VC-size", "disjuncts")
time {
- SimpleSolverAPI(SolverFactory(() => solverFactory.getNewSolver())).solveSAT(compressedVC)
+ SimpleSolverAPI(solverFactory).solveSAT(compressedVC)
} { compTime =>
Stats.updateCumTime(compTime, "TotalCompressVCCTime")
reporter.info("checked compressed VC... in " + compTime / 1000.0 + "s")
diff --git a/src/main/scala/leon/invariant/util/Minimizer.scala b/src/main/scala/leon/invariant/util/Minimizer.scala
index ddf7c01dda693e9067376a2f1b01942ad7e007c2..a05b9d72b49f104c3b0a7eb227a4e8d331c1161a 100644
--- a/src/main/scala/leon/invariant/util/Minimizer.scala
+++ b/src/main/scala/leon/invariant/util/Minimizer.scala
@@ -54,8 +54,9 @@ class Minimizer(ctx: InferenceContext, program: Program) {
*/
def minimizeBounds(nestMap: Map[Variable, Int])(inputCtr: Expr, initModel: Model): Model = {
val orderedTempVars = nestMap.toSeq.sortWith((a, b) => a._2 >= b._2).map(_._1)
- lazy val solver = new SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() =>
- new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver), ctx.vcTimeout * 1000))
+ lazy val solver = new SimpleSolverAPI(new TimeoutSolverFactory(
+ SolverFactory.getFromName(leonctx,program)("smt-z3-u"),
+ ctx.vcTimeout * 1000))
reporter.info("minimizing...")
var currentModel = initModel
@@ -189,4 +190,4 @@ class Minimizer(ctx: InferenceContext, program: Program) {
functionNesting(template)
nestMap
}
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/invariant/util/SolverUtil.scala b/src/main/scala/leon/invariant/util/SolverUtil.scala
index e0f3fe000b8ddd332f7cf6557b6874613c7c3982..97d94021d00d3ad798595822c4f7fe7129966eea 100644
--- a/src/main/scala/leon/invariant/util/SolverUtil.scala
+++ b/src/main/scala/leon/invariant/util/SolverUtil.scala
@@ -72,7 +72,7 @@ object SolverUtil {
if (idmap.keys.nonEmpty) {
val newpathcond = replace(idmap, expr)
//check if this is solvable
- val solver = SimpleSolverAPI(SolverFactory(() => new ExtendedUFSolver(ctx, prog)))
+ val solver = SimpleSolverAPI(SolverFactory("extendedUF", () => new ExtendedUFSolver(ctx, prog)))
solver.solveSAT(newpathcond)._1 match {
case Some(true) => {
println("Path satisfiable for a?,c? -->6,2 ")
@@ -143,4 +143,4 @@ object SolverUtil {
}
}
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index e295adafbb5468eba718b803ca7477d3703a7394..f2cddbf38cd0f6a2fc9237062623d7b292c262d1 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -13,7 +13,7 @@ import purescala.Definitions._
import scala.reflect.runtime.universe._
import _root_.smtlib.interpreters._
-abstract class SolverFactory[+S <: Solver : TypeTag] {
+abstract class SolverFactory[+S <: Solver] {
def getNewSolver(): S
def shutdown(): Unit = {}
@@ -22,12 +22,13 @@ abstract class SolverFactory[+S <: Solver : TypeTag] {
s.free()
}
- val name = typeOf[S].toString.split("\\.").last.replaceAll("Solver", "")+"*"
+ val name: String
}
object SolverFactory {
- def apply[S <: Solver : TypeTag](builder: () => S): SolverFactory[S] = {
+ def apply[S <: Solver : TypeTag](nme: String, builder: () => S): SolverFactory[S] = {
new SolverFactory[S] {
+ val name = nme
def getNewSolver() = builder()
}
}
@@ -80,36 +81,19 @@ object SolverFactory {
}
def getFromName(ctx: LeonContext, program: Program)(name: String): SolverFactory[TimeoutSolver] = name match {
- case "fairz3" =>
- SolverFactory(() => new FairZ3Solver(ctx, program) with TimeoutSolver)
-
- case "unrollz3" =>
- SolverFactory(() => new Z3UnrollingSolver(ctx, program, new UninterpretedZ3Solver(ctx, program)) with TimeoutSolver)
-
- case "enum" =>
- SolverFactory(() => new EnumerationSolver(ctx, program) with TimeoutSolver)
-
- case "ground" =>
- SolverFactory(() => new GroundSolver(ctx, program) with TimeoutSolver)
-
- case "smt-z3" =>
- SolverFactory(() => new Z3UnrollingSolver(ctx, program, new SMTLIBZ3Solver(ctx, program)) with TimeoutSolver)
-
- case "smt-z3-q" =>
- SolverFactory(() => new SMTLIBZ3QuantifiedSolver(ctx, program) with TimeoutSolver)
-
- case "smt-cvc4" =>
- SolverFactory(() => new CVC4UnrollingSolver(ctx, program, new SMTLIBCVC4Solver(ctx, program)) with TimeoutSolver)
-
- case "smt-cvc4-proof" =>
- SolverFactory(() => new SMTLIBCVC4ProofSolver(ctx, program) with TimeoutSolver)
-
- case "smt-cvc4-cex" =>
- SolverFactory(() => new SMTLIBCVC4CounterExampleSolver(ctx, program) with TimeoutSolver)
-
- case "isabelle" =>
- new isabelle.IsabelleSolverFactory(ctx, program)
-
+ case "enum" => SolverFactory(name, () => new EnumerationSolver(ctx, program) with TimeoutSolver)
+ case "ground" => SolverFactory(name, () => new GroundSolver(ctx, program) with TimeoutSolver)
+ case "fairz3" => SolverFactory(name, () => new FairZ3Solver(ctx, program) with TimeoutSolver)
+ case "unrollz3" => SolverFactory(name, () => new Z3UnrollingSolver(ctx, program, new UninterpretedZ3Solver(ctx, program)) with TimeoutSolver)
+ case "smt-z3" => SolverFactory(name, () => new Z3UnrollingSolver(ctx, program, new SMTLIBZ3Solver(ctx, program)) with TimeoutSolver)
+ case "smt-z3-q" => SolverFactory(name, () => new SMTLIBZ3QuantifiedSolver(ctx, program) with TimeoutSolver)
+ case "smt-cvc4" => SolverFactory(name, () => new CVC4UnrollingSolver(ctx, program, new SMTLIBCVC4Solver(ctx, program)) with TimeoutSolver)
+ case "smt-cvc4-proof" => SolverFactory(name, () => new SMTLIBCVC4ProofSolver(ctx, program) with TimeoutSolver)
+ case "smt-cvc4-cex" => SolverFactory(name, () => new SMTLIBCVC4CounterExampleSolver(ctx, program) with TimeoutSolver)
+ case "smt-z3-u" => SolverFactory(name, () => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
+ case "smt-cvc4-u" => SolverFactory(name, () => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
+ case "nativez3-u" => SolverFactory(name, () => new UninterpretedZ3Solver(ctx, program) with TimeoutSolver)
+ case "isabelle" => new isabelle.IsabelleSolverFactory(ctx, program)
case _ =>
ctx.reporter.error(s"Unknown solver $name")
showSolvers(ctx)
@@ -137,29 +121,30 @@ object SolverFactory {
// Fast solver used by simplifications, to discharge simple tautologies
def uninterpreted(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
val names = ctx.findOptionOrDefault(GlobalOptions.optSelectedSolvers)
-
+ val fromName = getFromName(ctx, program) _
+
if ((names contains "fairz3") && !hasNativeZ3) {
if (hasZ3) {
if (!reported) {
ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-z3.")
reported = true
}
- SolverFactory(() => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
+ fromName("smt-z3-u")
} else if (hasCVC4) {
if (!reported) {
ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-cvc4.")
reported = true
}
- SolverFactory(() => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
+ fromName("smt-cvc4-u")
} else {
ctx.reporter.fatalError("No SMT solver available: native Z3 api could not load and 'cvc4' or 'z3' binaries were not found in PATH.")
}
} else if(names contains "smt-cvc4") {
- SolverFactory(() => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
+ fromName("smt-cvc4-u")
} else if(names contains "smt-z3") {
- SolverFactory(() => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
+ fromName("smt-z3-u")
} else if ((names contains "fairz3") && hasNativeZ3) {
- SolverFactory(() => new UninterpretedZ3Solver(ctx, program) with TimeoutSolver)
+ fromName("nativez3-u")
} else {
ctx.reporter.fatalError("No SMT solver available: native Z3 api could not load and 'cvc4' or 'z3' binaries were not found in PATH.")
}
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
index f6a70043182fc237298c30d3b6ffa5c943233bea..d5027a440761b8f8671cd2c96826312335a0d35c 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala
@@ -6,7 +6,7 @@ package combinators
import scala.reflect.runtime.universe._
-class PortfolioSolverFactory[S <: Solver](ctx: LeonContext, sfs: Seq[SolverFactory[S]])(implicit tag: TypeTag[S]) extends SolverFactory[PortfolioSolver[S] with TimeoutSolver] {
+class PortfolioSolverFactory[S <: Solver](ctx: LeonContext, sfs: Seq[SolverFactory[S]]) extends SolverFactory[PortfolioSolver[S] with TimeoutSolver] {
def getNewSolver(): PortfolioSolver[S] with TimeoutSolver = {
new PortfolioSolver[S](ctx, sfs.map(_.getNewSolver())) with TimeoutSolver
@@ -21,5 +21,7 @@ class PortfolioSolverFactory[S <: Solver](ctx: LeonContext, sfs: Seq[SolverFacto
case _ =>
ctx.reporter.error("Failed to reclaim a non-portfolio solver.")
}
+
+ val name = sfs.map(_.name).mkString("Pfolio(", ",", ")")
}
diff --git a/src/main/scala/leon/solvers/combinators/SolverPool.scala b/src/main/scala/leon/solvers/combinators/SolverPool.scala
index 2d38591f69b3bcb3417ab59f335edc5e20543bd0..4df3a27b842167b4788ed2c07e16417fec5f553f 100644
--- a/src/main/scala/leon/solvers/combinators/SolverPool.scala
+++ b/src/main/scala/leon/solvers/combinators/SolverPool.scala
@@ -17,7 +17,9 @@ import scala.reflect.runtime.universe._
* growing/shrinking pool size...
*/
-class SolverPoolFactory[+S <: Solver](ctx: LeonContext, sf: SolverFactory[S])(implicit tag: TypeTag[S]) extends SolverFactory[S] {
+class SolverPoolFactory[+S <: Solver](ctx: LeonContext, sf: SolverFactory[S]) extends SolverFactory[S] {
+
+ val name = "Pool(" + sf.name + ")"
var poolSize = 0
val poolMaxSize = 5
diff --git a/src/main/scala/leon/solvers/isabelle/IsabelleSolverFactory.scala b/src/main/scala/leon/solvers/isabelle/IsabelleSolverFactory.scala
index 0e356aa5559c4d00326971401f3e9c7e79546327..11dfe40d392d1b0bb88fee7e1d7f9f1a2166450b 100644
--- a/src/main/scala/leon/solvers/isabelle/IsabelleSolverFactory.scala
+++ b/src/main/scala/leon/solvers/isabelle/IsabelleSolverFactory.scala
@@ -12,6 +12,8 @@ import leon.solvers._
final class IsabelleSolverFactory(context: LeonContext, program: Program) extends SolverFactory[TimeoutSolver] {
+ val name = "isabelle"
+
private val env = IsabelleEnvironment(context, program)
override def shutdown() =
diff --git a/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala b/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
index 85382cfcdf39a7d1cd77c78a4a76b7ed32a02689..e4fabf2daf1bb200d95e272188223efc9a8c105b 100644
--- a/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
@@ -446,7 +446,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
(qarg, arg) <- (qargs zip args)
_ = strictnessCnstr(qarg, arg)
} qarg match {
- case Left(quant) if subst.isDefinedAt(quant) =>
+ case Left(quant) if !quantified(quant) || subst.isDefinedAt(quant) =>
eqConstraints += (quant -> arg.encoded)
case Left(quant) if quantified(quant) =>
subst += quant -> arg
diff --git a/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala b/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala
index bd477c54a30bbd3dbeb938db0566d166ad498f5a..c95b75e3ea3603ff773e9621498c30095c16e033 100644
--- a/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala
+++ b/src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala
@@ -25,7 +25,7 @@ class SimplifyPathsSuite extends LeonTestSuite {
val l2 = InfiniteIntegerLiteral(2)
def simplifyPaths(ctx: LeonContext, expr: Expr): Expr = {
- val uninterpretedZ3 = SolverFactory(() => new UninterpretedZ3Solver(ctx, Program.empty))
+ val uninterpretedZ3 = SolverFactory.getFromName(ctx, Program.empty)("nativez3-u")
try {
ExprOps.simplifyPaths(uninterpretedZ3)(expr)
} finally {
diff --git a/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala b/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala
index e491737cdc12adcfd9331396e7cde874ee4c8c55..9714c5678c7490fa415f11149c7b2640af123183 100644
--- a/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala
+++ b/src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala
@@ -45,7 +45,7 @@ class TimeoutSolverSuite extends LeonTestSuite {
}
private def getTOSolver(ctx: LeonContext): SolverFactory[Solver] = {
- SolverFactory(() => (new IdioticSolver(ctx, Program.empty) with TimeoutSolver).setTimeout(200L))
+ SolverFactory("idiotic", () => (new IdioticSolver(ctx, Program.empty) with TimeoutSolver).setTimeout(200L))
}
private def check(sf: SolverFactory[Solver], e: Expr): Option[Boolean] = {
diff --git a/src/test/scala/leon/unit/solvers/SolverPoolSuite.scala b/src/test/scala/leon/unit/solvers/SolverPoolSuite.scala
index eba92b1f00039287753a1db5a3e5b3bb660fd718..ad781b577e27414638686b78940ece46f288ba7d 100644
--- a/src/test/scala/leon/unit/solvers/SolverPoolSuite.scala
+++ b/src/test/scala/leon/unit/solvers/SolverPoolSuite.scala
@@ -28,7 +28,7 @@ class SolverPoolSuite extends LeonTestSuite {
}
def sfactory(implicit ctx: LeonContext): SolverFactory[Solver] = {
- SolverFactory(() => new DummySolver(ctx, Program.empty))
+ SolverFactory("dummy", () => new DummySolver(ctx, Program.empty))
}
val poolSize = 5;