From 8a8ec3fffdb7626af23191b60b0aad24a64db9df Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 7 May 2015 17:23:23 +0200
Subject: [PATCH] Fix solver names for real this time
---
.../leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala | 2 ++
src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofTarget.scala | 2 ++
.../scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala | 2 +-
3 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4CounterExampleTarget.scala
index 60b148c8c..6549193ea 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 1df96a80d..f868e0dfc 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 305457527..87e4a40a4 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
--
GitLab