From 8e5ad90c042c54d4cd9d25b818038e0c3a2ded07 Mon Sep 17 00:00:00 2001 From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch> Date: Mon, 8 Aug 2016 14:02:39 +0200 Subject: [PATCH] Update targets --- src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Target.scala | 2 ++ src/main/scala/inox/solvers/smtlib/SMTLIBZ3Target.scala | 1 - 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBCVC4Target.scala index 4e87fa6b9..a263a3042 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 bf2cf05e2..d08689741 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 -- GitLab