diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala index 60b148c8cfe106f2e7aaa81cd1277ed714f281f3..6549193ea364f6d316fce2948098b11f90aa3e8c 100644 --- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala +++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala @@ -15,6 +15,8 @@ import smtlib.parser.Terms._ trait SMTLIBCVC4CounterExampleTarget extends SMTLIBCVC4QuantifiedTarget { this: SMTLIBSolver => + override val targetName = "cvc4-cex" + override def interpreterOps(ctx: LeonContext) = { Seq( "-q", diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofTarget.scala index 1df96a80d44be45e565f22e8bc8fd59b9fb0cd29..f868e0dfca39adb5226f02b169b119e5180287b2 100644 --- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofTarget.scala +++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofTarget.scala @@ -15,6 +15,8 @@ import smtlib.parser.Terms._ trait SMTLIBCVC4ProofTarget extends SMTLIBCVC4QuantifiedTarget { this: SMTLIBSolver => + override val targetName = "cvc4-proof" + override def interpreterOps(ctx: LeonContext) = { Seq( "-q", diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala index 30545752722c230e7fa214ac2e1d62a80eba25e6..87e4a40a4967c500fd98f4b25b1be946c21b6f65 100644 --- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala +++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala @@ -16,7 +16,7 @@ import smtlib.theories.Core.Equals trait SMTLIBCVC4QuantifiedTarget extends SMTLIBCVC4Target { this: SMTLIBSolver => - override val targetName = "cvc4-proof" + override val targetName = "cvc4-quantified" private val typedFunDefExplorationLimit = 10000