/* Copyright 2009-2015 EPFL, Lausanne */ package leon package solvers.smtlib import purescala.Definitions.Program class SMTLIBCVC4CounterExampleSolver(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedSolver(context, program) { override def targetName = "cvc4-cex" override def interpreterOps(ctx: LeonContext) = { Seq( "-q", "--rewrite-divk", "--produce-models", "--print-success", "--lang", "smt", "--fmf-fun" ) ++ userDefinedOps(ctx) } protected val allowQuantifiedAssertions: Boolean = false }