Fix solver names

epfl-lara · Sep 17, 2024 · 96a02ab · 96a02ab
1 parent 6b862c5
commit 96a02ab
Showing 1 changed file with 6 additions and 3 deletions.
diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala
@@ -270,7 +270,7 @@ object SolverFactory {
         () => new SMTZ3OptImpl(p)
       })
 
-      case "horn-z3" => create(p)(finalName, {
+      case "inv-z3" => create(p)(finalName, {
         val emptyEnc = ProgramEncoder.empty(enc.targetProgram)
         val chooses = ChooseEncoder(enc.targetProgram)(emptyEnc)
         class SMTZ3Impl(override val program: enc.targetProgram.type)
@@ -279,6 +279,8 @@ object SolverFactory {
             with TimeoutSolver
             with tip.TipDebugger {
 
+          override val name = "inv-z3" 
+
           class Underlying(override val program: targetProgram.type)
             extends smtlib.SMTLIBSolver(program, context)
               with smtlib.Z3Solver {
@@ -308,7 +310,6 @@ object SolverFactory {
               parser.parseGenResponse
 
               override def eval(cmd: Terms.SExpr): Terms.SExpr = 
-                // println(s"{SENDING} $cmd")
                 super.eval(cmd)
 
             override protected val interpreter = {
@@ -333,7 +334,7 @@ object SolverFactory {
         () => new EncodedImpl(p, enc, SMTZ3Impl(enc.targetProgram))
       })
 
-      case "horn-eld" => create(p)(finalName, {
+      case "inv-eld" => create(p)(finalName, {
         val emptyEnc = ProgramEncoder.empty(enc.targetProgram)
         val chooses = ChooseEncoder(enc.targetProgram)(emptyEnc)
         class SMTEldaricaImpl(override val program: enc.targetProgram.type)
@@ -342,6 +343,8 @@ object SolverFactory {
             with TimeoutSolver
             with tip.TipDebugger {
 
+          override val name = "inv-eld" 
+
           class Underlying(override val program: targetProgram.type)
             extends smtlib.SMTLIBSolver(program, context)
               with smtlib.CVC5Solver {