Change order of solvers to avoid smt-z3-opt being recognized as a custom z3 executable

Author: jad-hamza

src/main/scala/inox/solvers/SolverFactory.scala

@@ -191,20 +191,19 @@ object SolverFactory {
         }
       })
 
-      case _ if finalName.startsWith("smt-z3") => create(p)(finalName, {
+      case "smt-z3-opt" => create(p)(finalName, {
         val chooseEnc = ChooseEncoder(p)(enc)
         val fullEnc = enc andThen chooseEnc
         val theoryEnc = theories.Z3(fullEnc.targetProgram)
         val progEnc = fullEnc andThen theoryEnc
         val targetProg = progEnc.targetProgram
         val targetSem = targetProg.getSemantics
-        val executableName = if (finalName == "smt-z3") "z3" else finalName.drop(7)
 
         () => new {
           val program: p.type = p
           val context = ctx
           val encoder: enc.type = enc
-        } with UnrollingSolver with TimeoutSolver with tip.TipDebugger {
+        } with UnrollingOptimizer with TimeoutSolver {
           override protected val semantics = sem
           override protected val chooses: chooseEnc.type = chooseEnc
           override protected val theories: theoryEnc.type = theoryEnc
@@ -216,26 +215,26 @@ object SolverFactory {
           protected val underlying = new {
             val program: progEnc.targetProgram.type = progEnc.targetProgram
             val context = ctx
-          } with smtlib.Z3Solver {
+          } with smtlib.optimization.Z3Optimizer {
             val semantics: program.Semantics = targetSem
-            override def targetName = executableName
           }
         }
       })
 
-      case "smt-z3-opt" => create(p)(finalName, {
+      case _ if finalName.startsWith("smt-z3") => create(p)(finalName, {
         val chooseEnc = ChooseEncoder(p)(enc)
         val fullEnc = enc andThen chooseEnc
         val theoryEnc = theories.Z3(fullEnc.targetProgram)
         val progEnc = fullEnc andThen theoryEnc
         val targetProg = progEnc.targetProgram
         val targetSem = targetProg.getSemantics
+        val executableName = if (finalName == "smt-z3") "z3" else finalName.drop(7)
 
         () => new {
           val program: p.type = p
           val context = ctx
           val encoder: enc.type = enc
-        } with UnrollingOptimizer with TimeoutSolver {
+        } with UnrollingSolver with TimeoutSolver with tip.TipDebugger {
           override protected val semantics = sem
           override protected val chooses: chooseEnc.type = chooseEnc
           override protected val theories: theoryEnc.type = theoryEnc
@@ -247,8 +246,9 @@ object SolverFactory {
           protected val underlying = new {
             val program: progEnc.targetProgram.type = progEnc.targetProgram
             val context = ctx
-          } with smtlib.optimization.Z3Optimizer {
+          } with smtlib.Z3Solver {
             val semantics: program.Semantics = targetSem
+            override def targetName = executableName
           }
         }
       })