Skip to content
Snippets Groups Projects
Commit 8a8ec3ff authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Fix solver names for real this time

parent 9f30d3ef
Branches
Tags
No related merge requests found
......@@ -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",
......
......@@ -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",
......
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment