diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Target.scala index 4e87fa6b914bdd44dedbd7bc2ba9c071e8e49893..a263a30422c7ab27a47e6826ebce03b911499c03 100644 --- a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Target.scala +++ b/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Target.scala @@ -17,6 +17,8 @@ trait SMTLIBCVC4Target extends SMTLIBTarget { import trees._ import symbols._ + def targetName = "cvc4" + override def getNewInterpreter(ctx: InoxContext) = { val opts = interpreterOps(ctx) ctx.reporter.debug("Invoking solver with "+opts.mkString(" ")) diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Target.scala index bf2cf05e2ad68fddec9f068fffbed3b6b6242baf..d0868974106d4334a23e024c2103f56ce8993c17 100644 --- a/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Target.scala +++ b/src/main/scala/inox/solvers/smtlib/SMTLIBZ3Target.scala @@ -4,7 +4,6 @@ package inox package solvers package smtlib -import _root_.smtlib.common._ import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, Let => SMTLet, _} import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _} import _root_.smtlib.interpreters.Z3Interpreter