diff --git a/LICENSE b/LICENSE
index 2418ba1b5fb52ae5c981bd3b1378bf601d20a746..bb0f3c2eec8b672b85f77e428d94feb00c2f14da 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2009-2013 EPFL, Lausanne, unless otherwise specified. All rights
+Copyright (c) 2009-2015 EPFL, Lausanne, unless otherwise specified. All rights
reserved.
This software was developed by the Laboratory for Automated Reasoning and
diff --git a/library/instrumentation/package.scala b/library/instrumentation/package.scala
index a724eadd725cae95034354c5bd64990f8ff18ba3..a6e7545c0b4ab2bae468b0cc6556f67784487b17 100644
--- a/library/instrumentation/package.scala
+++ b/library/instrumentation/package.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon
diff --git a/library/invariant/package.scala b/library/invariant/package.scala
index 4382462bdbce3e062d246aefa682db21df557624..0cc7919d0194a5dff25457c38db8cd00c78db8bd 100644
--- a/library/invariant/package.scala
+++ b/library/invariant/package.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon
diff --git a/library/proof/Internal.scala b/library/proof/Internal.scala
index ad395f5326884a34be16eda85a84e01f5bf323d8..0962c371c670d2b08db797a9f24542195c78bac8 100644
--- a/library/proof/Internal.scala
+++ b/library/proof/Internal.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.proof
import leon.lang._
diff --git a/library/proof/package.scala b/library/proof/package.scala
index f298dce2726e29394df38656e695824ed65661a6..3f097864964a8d2d724a8ec1256dd803c5c048c5 100644
--- a/library/proof/package.scala
+++ b/library/proof/package.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon
import leon.annotation._
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 45c62bd0d3a5e82735b98237d2671f485915d13d..9cc0dc9c6af811444024a05dd95b93c518df31eb 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -141,7 +141,7 @@ object Main {
def computePipeline(ctx: LeonContext): Pipeline[List[String], Any] = {
import purescala.Definitions.Program
- import purescala.{FunctionClosure, RestoreMethods}
+ import purescala.RestoreMethods
import utils.FileOutputPhase
import frontends.scalac.{ExtractionPhase, ClassgenPhase}
import synthesis.SynthesisPhase
@@ -164,8 +164,8 @@ object Main {
val terminationF = ctx.findOptionOrDefault(optTermination)
val verifyF = ctx.findOptionOrDefault(optVerify)
val evalF = ctx.findOption(optEval).isDefined
- val inferInvF = ctx.findOptionOrDefault(optInferInv)
- val instrumentF = ctx.findOptionOrDefault(optInstrument)
+ val inferInvF = ctx.findOptionOrDefault(optInferInv)
+ val instrumentF = ctx.findOptionOrDefault(optInstrument)
val analysisF = verifyF && terminationF
if (helpF) {
diff --git a/src/main/scala/leon/evaluators/ScalacEvaluator.scala b/src/main/scala/leon/evaluators/ScalacEvaluator.scala
index 2356bdf33329288907d8d48ccb6f9cdd07c8596a..7c4d8ee92ad2379987c0563e388d9d4fdfb777fc 100644
--- a/src/main/scala/leon/evaluators/ScalacEvaluator.scala
+++ b/src/main/scala/leon/evaluators/ScalacEvaluator.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon
package evaluators
diff --git a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
index eca69f0c0f0246dae7840ae9b6511f841fcc90d2..e79926e62158a095b755b48db43c8f3e46c41590 100644
--- a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
+++ b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
@@ -43,7 +43,7 @@ object InferInvariantsPhase extends SimpleLeonPhase[Program, InferenceReport] {
def apply(ctx: LeonContext, program: Program): InferenceReport = {
val inferctx = new InferenceContext(program, ctx)
val report = (new InferenceEngine(inferctx)).runWithTimeout()
- //println("Final Program: \n" +PrettyPrinter.apply(report.finalProgramWoInstrumentation))
+ //println("Final Program: \n" +PrettyPrinter.apply(InferenceReportUtil.pushResultsToInput(inferctx, report.conditions)))
report
}
}
diff --git a/src/main/scala/leon/invariant/engine/InferenceReport.scala b/src/main/scala/leon/invariant/engine/InferenceReport.scala
index 39af145c31bd5a7253475a5cebe047fca4e932b3..d5f0196278d04489f657940caf74e30009fd02b9 100644
--- a/src/main/scala/leon/invariant/engine/InferenceReport.scala
+++ b/src/main/scala/leon/invariant/engine/InferenceReport.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon
package invariant.engine
@@ -112,142 +112,91 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]], program: Program)(implicit ct
object InferenceReportUtil {
- /* def programWoInstrumentation(ctx: InferenceContext, p: Program, ics: Seq[InferenceCondition]) = {
- val funToUninstFun = p.definedFunctions.foldLeft(Map[FunDef, FunDef]()) {
- case (acc, fd) =>
- val uninstFunName = InstUtil.userFunctionName(fd)
- val uninstFdOpt =
- if (uninstFunName.isEmpty) None
- else functionByName(uninstFunName, ctx.initProgram)
- if (uninstFdOpt.isDefined) {
- acc + (fd -> uninstFdOpt.get)
- } else acc
- }
- val funToPost = ics.collect {
- case cd if cd.prettyInv.isDefined && funToUninstFun.contains(cd.fd) =>
- funToUninstFun(cd.fd) -> cd.prettyInv.get
- }.toMap
- //println("Function to template: " + funToTmpl.map { case (k, v) => s"${k.id.name} --> $v" }.mkString("\n"))
- assignTemplateAndCojoinPost(Map(), ctx.initProgram, funToPost, uniqueIdDisplay = false)
- }*/
-
- def pluginResultInInput(ctx: InferenceContext, ics: Seq[InferenceCondition], p: Program) = {
+ def pushResultsToInput(ctx: InferenceContext, ics: Seq[InferenceCondition]) = {
+ val initFuns = functionsWOFields(ctx.initProgram.definedFunctions).filter { fd =>
+ !fd.isTheoryOperation && !fd.annotations.contains("library")
+ }
val solvedICs = ics.filter { _.prettyInv.isDefined }
+
// mapping from init to output
- val outputFunMap =
- functionsWOFields(ctx.initProgram.definedFunctions).map {
- case fd if fd.isTheoryOperation => (fd -> fd)
- case fd => {
- val freshId = FreshIdentifier(fd.id.name, fd.returnType)
- val newfd = new FunDef(freshId, fd.tparams, fd.params, fd.returnType)
- fd -> newfd
- }
+ val initToOutput =
+ initFuns.map { fd =>
+ val freshId = FreshIdentifier(fd.id.name, fd.returnType)
+ val newfd = new FunDef(freshId, fd.tparams, fd.params, fd.returnType)
+ fd -> newfd
}.toMap
def fullNameWoInst(fd: FunDef) = {
- val splits = DefOps.fullName(fd)(p).split("-")
+ val splits = DefOps.fullName(fd)(ctx.inferProgram).split("-")
if (!splits.isEmpty) splits(0)
else ""
}
- // mapping from p to output
- val progFunMap = (Map[FunDef, FunDef]() /: functionsWOFields(p.definedFunctions)) {
- case (acc, fd) =>
- val inFun = functionByFullName(fullNameWoInst(fd), ctx.initProgram)
- if (inFun.isDefined)
- acc + (fd -> outputFunMap(inFun.get))
- else acc
+ val nameToInitFun = initFuns.map { fd =>
+ DefOps.fullName(fd)(ctx.initProgram) -> fd
}.toMap
// mapping from init to ic
- val initICmap = (Map[FunDef, InferenceCondition]() /: solvedICs) {
+ val initICMap = (Map[FunDef, InferenceCondition]() /: solvedICs) {
case (acc, ic) =>
- val initfd = functionByFullName(fullNameWoInst(ic.fd), ctx.initProgram)
- if (initfd.isDefined) {
- acc + (initfd.get -> ic)
- } else acc
+ nameToInitFun.get(fullNameWoInst(ic.fd)) match {
+ case Some(initfd) =>
+ acc + (initfd -> ic)
+ case _ => acc
+ }
}
- def mapProgram(funMap: Map[FunDef, FunDef]) = {
-
- def mapExpr(ine: Expr): Expr = {
- val replaced = simplePostTransform((e: Expr) => e match {
- case FunctionInvocation(tfd, args) if funMap.contains(tfd.fd) =>
- FunctionInvocation(TypedFunDef(funMap(tfd.fd), tfd.tps), args)
- case _ => e
- })(ine)
- replaced
- }
-
- for ((from, to) <- funMap) {
- to.body = from.body.map(mapExpr)
- to.precondition = from.precondition.map(mapExpr)
- if (initICmap.contains(from)) {
- val ic = initICmap(from)
- val paramMap = (ic.fd.params zip from.params).map {
- case (p1, p2) =>
- (p1.id.toVariable -> p2.id.toVariable)
- }.toMap
- val icres = getResId(ic.fd).get
- val npost =
- if (from.hasPostcondition) {
- val resid = getResId(from).get
- val inv = replace(Map(icres.toVariable -> resid.toVariable) ++ paramMap, ic.prettyInv.get)
- val postBody = from.postWoTemplate.map(post => createAnd(Seq(post, inv))).getOrElse(inv)
- Lambda(Seq(ValDef(resid)), postBody)
- } else {
- val resid = FreshIdentifier(icres.name, icres.getType)
- val inv = replace(Map(icres.toVariable -> resid.toVariable) ++ paramMap, ic.prettyInv.get)
- Lambda(Seq(ValDef(resid)), inv)
+ def mapExpr(ine: Expr): Expr = {
+ val replaced = simplePostTransform((e: Expr) => e match {
+ case FunctionInvocation(TypedFunDef(fd, targs), args) =>
+ if (initToOutput.contains(fd)) {
+ FunctionInvocation(TypedFunDef(initToOutput(fd), targs), args)
+ } else {
+ nameToInitFun.get(fullNameWoInst(fd)) match {
+ case Some(ifun) if initToOutput.contains(ifun) =>
+ FunctionInvocation(TypedFunDef(initToOutput(ifun), targs), args)
+ case _ => e
}
- to.postcondition = Some(mapExpr(npost))
- } else
- to.postcondition = from.postcondition.map(mapExpr)
- //copy annotations
- from.flags.foreach(to.addFlag(_))
- }
+ }
+ case _ => e
+ })(ine)
+ replaced
}
- mapProgram(outputFunMap ++ progFunMap)
+ // copy bodies and specs
+ for ((from, to) <- initToOutput) {
+ to.body = from.body.map(mapExpr)
+ to.precondition = from.precondition.map(mapExpr)
+ val icOpt = initICMap.get(from)
+ if (icOpt.isDefined) {
+ val ic = icOpt.get
+ val paramMap = (ic.fd.params zip from.params).map {
+ case (p1, p2) =>
+ (p1.id.toVariable -> p2.id.toVariable)
+ }.toMap
+ val icres = getResId(ic.fd).get
+ val npost =
+ if (from.hasPostcondition) {
+ val resid = getResId(from).get
+ val inv = replace(Map(icres.toVariable -> resid.toVariable) ++ paramMap, ic.prettyInv.get)
+ val postBody = from.postWoTemplate.map(post => createAnd(Seq(post, inv))).getOrElse(inv)
+ Lambda(Seq(ValDef(resid)), postBody)
+ } else {
+ val resid = FreshIdentifier(icres.name, icres.getType)
+ val inv = replace(Map(icres.toVariable -> resid.toVariable) ++ paramMap, ic.prettyInv.get)
+ Lambda(Seq(ValDef(resid)), inv)
+ }
+ to.postcondition = Some(mapExpr(npost))
+ } else
+ to.postcondition = from.postcondition.map(mapExpr)
+ //copy annotations
+ from.flags.foreach(to.addFlag(_))
+ }
+
copyProgram(ctx.initProgram, (defs: Seq[Definition]) => defs.map {
- case fd: FunDef if outputFunMap.contains(fd) =>
- outputFunMap(fd)
+ case fd: FunDef if initToOutput.contains(fd) =>
+ initToOutput(fd)
case d => d
})
- /*if (debugSimplify)
- println("After Simplifications: \n" + ScalaPrinter.apply(newprog))*/
- // /newprog
- /*if (ic.prettyInv.isDefined) {
- val uninstFunName = InstUtil.userFunctionName(ic.fd)
- val inputFdOpt =
- if (uninstFunName.isEmpty) None
- else functionByName(uninstFunName, ctx.initProgram)
- inputFdOpt match {
- case None => ctx.initProgram
- case Some(inFd) =>
- ProgramUtil.copyProgram(ctx.initProgram, defs => defs map {
- case fd if fd.id == inFd.id =>
- val newfd = new FunDef(FreshIdentifier(inFd.id.name), inFd.tparams, inFd.params, inFd.returnType)
- newfd.body = inFd.body
- newfd.precondition = inFd.precondition
- val fdres = getResId(ic.fd).get
- val npost =
- if (inFd.hasPostcondition) {
- val resid = getResId(inFd).get
- val inv = replace(Map(fdres.toVariable -> resid.toVariable), ic.prettyInv.get)
- // map also functions here.
- val postBody = inFd.postWoTemplate.map(post => createAnd(Seq(post, inv))).getOrElse(inv)
- Lambda(Seq(ValDef(resid)), postBody)
- } else {
- val resid = FreshIdentifier(fdres.name, fdres.getType)
- val inv = replace(Map(fdres.toVariable -> resid.toVariable), ic.prettyInv.get)
- Lambda(Seq(ValDef(resid)), inv)
- }
- newfd.postcondition = Some(npost)
- newfd
- case d => d
- })
- }
- } else ctx.initProgram*/
}
}
\ No newline at end of file
diff --git a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
index f54eeef6249651ee7d8ab1517a1982f9e69f6694..4bb5bbc3d76a341151ff9478b139f2ad8157485d 100644
--- a/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala
@@ -134,12 +134,16 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, program: Program, rootFd: F
}
def apply() = {
- //create a body and post of the function
- val (bodyExpr, fullPost) = constructVC(rootFd)
- if (fullPost == tru)
- Some(InferResult(true, Some(Model.empty), List()))
- else
- solveParametricVC(And(bodyExpr, Not(fullPost)))
+ if(ctx.abort) {
+ Some(InferResult(false, None, List()))
+ } else {
+ //create a body and post of the function
+ val (bodyExpr, fullPost) = constructVC(rootFd)
+ if (fullPost == tru)
+ Some(InferResult(true, Some(Model.empty), List()))
+ else
+ solveParametricVC(And(bodyExpr, Not(fullPost)))
+ }
}
def instantiateModel(model: Model, funcs: Seq[FunDef]) = {
diff --git a/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala b/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala
index b072ddc67c4a5022854ee4cd772fbe39e685afa4..805f09a941139d817309a3a10df0b07cd57a21aa 100644
--- a/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/ExtendedUFSolver.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon
package invariant.templateSolvers
diff --git a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
index 26710b7111b301748340d738fd35a1465364c9da..19dee9ab4be261cd2378d2146864fb9566912ca3 100644
--- a/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala
@@ -274,7 +274,7 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
}
// solve the resulting constraints using solver
- val solver = if (solveAsBitvectors) {
+ lazy val solver = if (solveAsBitvectors) {
throw new IllegalStateException("Not supported now. Will be in the future!")
//new ExtendedUFSolver(leonctx, program, useBitvectors = true, bitvecSize = bvsize) with TimeoutSolver
} else {
@@ -282,11 +282,11 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() =>
new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver), timeout * 1000))
}
- //val solver = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => innerSolver), ))
if (verbose) reporter.info("solving...")
val t1 = System.currentTimeMillis()
- //solver.solveSAT(simpctrs)
- val (res, model) = solver.solveSAT(simpctrs) //solver.solveSAT(simpctrs, timeout * 1000)
+ val (res, model) =
+ if (ctx.abort) (None, Model.empty)
+ else solver.solveSAT(simpctrs)
val t2 = System.currentTimeMillis()
if (verbose) reporter.info((if (res.isDefined) "solved" else "timed out") + "... in " + (t2 - t1) / 1000.0 + "s")
Stats.updateCounterTime((t2 - t1), "NL-solving-time", "disjuncts")
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
index 0e0e4ef355e116d717a210cb2b587ad76c3b733b..41d672fe5a94861197430a69c9516985e46f2511 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
@@ -79,8 +79,8 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
ctrTracker.getVC(fd).splitParamPart
}
- def initVCSolvers {
- funcVCs.keys.foreach(fd => {
+ def initVCSolvers = {
+ funcVCs.keys.foreach { fd =>
val (paramPart, rest) = if (ctx.usereals) {
val (pp, r) = splitVC(fd)
(IntLiteralToReal(pp), IntLiteralToReal(r))
@@ -90,26 +90,28 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
if (hasReals(rest) && hasInts(rest))
throw new IllegalStateException("Non-param Part has both integers and reals: " + rest)
- val vcSolver =
- if (this.useCVCToCheckVCs)
- new SMTLIBCVC4Solver(leonctx, program) with TimeoutSolver
- else
- new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver
- vcSolver.assertCnstr(rest)
-
- if (debugIncrementalVC) {
- assert(getTemplateVars(rest).isEmpty)
- println("For function: " + fd.id)
- println("Param part: " + paramPart)
- /*vcSolver.check match {
+ if (!ctx.abort) { // this is required to ensure that solvers are not created after interrupts
+ val vcSolver =
+ if (this.useCVCToCheckVCs)
+ new SMTLIBCVC4Solver(leonctx, program) with TimeoutSolver
+ else
+ new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver
+ vcSolver.assertCnstr(rest)
+
+ if (debugIncrementalVC) {
+ assert(getTemplateVars(rest).isEmpty)
+ println("For function: " + fd.id)
+ println("Param part: " + paramPart)
+ /*vcSolver.check match {
case Some(false) => throw new IllegalStateException("Non param-part is unsat "+rest)
case _ => ;
}*/
+ }
+ vcSolvers += (fd -> vcSolver)
+ paramParts += (fd -> paramPart)
+ simpleParts += (fd -> rest)
}
- vcSolvers += (fd -> vcSolver)
- paramParts += (fd -> paramPart)
- simpleParts += (fd -> rest)
- })
+ }
}
def freeVCSolvers {
@@ -254,24 +256,26 @@ class NLTemplateSolver(ctx: InferenceContext, program: Program,
blockedCEs = true
Not(createOr(seenPaths(fd)))
} else tru
- getUNSATConstraints(fd, model, disableCounterExs) match {
- case None =>
- None
- case Some(((disjunct, callsInPath), ctrsForFun)) =>
- if (ctrsForFun == tru) Some(acc)
- else {
- confFunctions += fd
- confDisjuncts :+= disjunct
- callsInPaths ++= callsInPath
- //instantiate the disjunct
- val cePath = simplifyArithmetic(TemplateInstantiator.instantiate(disjunct, tempVarMap))
- //some sanity checks
- if (variablesOf(cePath).exists(TemplateIdFactory.IsTemplateIdentifier _))
- throw new IllegalStateException("Found template identifier in counter-example disjunct: " + cePath)
- updateSeenPaths(fd, cePath)
- Some(acc :+ ctrsForFun)
- }
- }
+ if (ctx.abort) None
+ else
+ getUNSATConstraints(fd, model, disableCounterExs) match {
+ case None =>
+ None
+ case Some(((disjunct, callsInPath), ctrsForFun)) =>
+ if (ctrsForFun == tru) Some(acc)
+ else {
+ confFunctions += fd
+ confDisjuncts :+= disjunct
+ callsInPaths ++= callsInPath
+ //instantiate the disjunct
+ val cePath = simplifyArithmetic(TemplateInstantiator.instantiate(disjunct, tempVarMap))
+ //some sanity checks
+ if (variablesOf(cePath).exists(TemplateIdFactory.IsTemplateIdentifier _))
+ throw new IllegalStateException("Found template identifier in counter-example disjunct: " + cePath)
+ updateSeenPaths(fd, cePath)
+ Some(acc :+ ctrsForFun)
+ }
+ }
}
newctrsOpt match {
case None =>
diff --git a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
index b373c5e7045aab99264c5403648c2ac968b48ef5..dceed68279e089122875d19c86664425df49aa22 100644
--- a/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/TemplateSolver.scala
@@ -88,7 +88,6 @@ abstract class TemplateSolver(ctx: InferenceContext, val rootFun: FunDef,
wr.close()
}
}
-
if (ctx.dumpStats) {
Stats.updateCounterStats(atomNum(vc), "VC-size", "VC-refinement")
Stats.updateCounterStats(numUIFADT(vc), "UIF+ADT", "VC-refinement")
@@ -103,9 +102,10 @@ abstract class TemplateSolver(ctx: InferenceContext, val rootFun: FunDef,
//else
acc ++ getTemplateIds(vc)
}
-
Stats.updateCounterStats(tempIds.size, "TemplateIds", "VC-refinement")
- val solution = solve(tempIds, funcExprs)
+ val solution =
+ if (ctx.abort) (None, None)
+ else solve(tempIds, funcExprs)
solution
}
diff --git a/src/main/scala/leon/invariant/util/Minimizer.scala b/src/main/scala/leon/invariant/util/Minimizer.scala
index f9ee65b007147b245330ede807e959a25411e3c0..e39378f267c0970d85797d19eef468c3a35f1db4 100644
--- a/src/main/scala/leon/invariant/util/Minimizer.scala
+++ b/src/main/scala/leon/invariant/util/Minimizer.scala
@@ -55,7 +55,7 @@ class Minimizer(ctx: InferenceContext, program: Program) {
val orderedTempVars = nestMap.toSeq.sortWith((a, b) => a._2 >= b._2).map(_._1)
//do a binary search sequentially on each of these tempvars
// note: use smtlib solvers so that they can be timedout
- val solver = new SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() =>
+ lazy val solver = new SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() =>
new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver), ctx.vcTimeout * 1000))
reporter.info("minimizing...")
@@ -97,7 +97,9 @@ class Minimizer(ctx: InferenceContext, program: Program) {
else {
val boundCtr = And(LessEquals(tvar, currval), GreaterEquals(tvar, lowerBound))
//val t1 = System.currentTimeMillis()
- val (res, newModel) = solver.solveSAT(And(acc, boundCtr))
+ val (res, newModel) =
+ if (ctx.abort) (None, Model.empty)
+ else solver.solveSAT(And(acc, boundCtr))
//val t2 = System.currentTimeMillis()
//println((if (res.isDefined) "solved" else "timed out") + "... in " + (t2 - t1) / 1000.0 + "s")
res match {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 99b4d9d1727144c5d1080dc192d2e6a5e4063f45..f13ed21a2929a0b845e9c0138092bb36b5fc6428 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -4,7 +4,6 @@ package leon
package solvers
package smtlib
-import verification.VC
import purescala.Common._
import purescala.Expressions._
import purescala.ExprOps._
@@ -21,9 +20,6 @@ abstract class SMTLIBSolver(val context: LeonContext, val program: Program)
def targetName: String
override def name: String = "smt-"+targetName
- /* Reporter */
- protected val reporter = context.reporter
-
override def dbg(msg: => Any) = {
debugOut foreach { o =>
o.write(msg.toString)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 01b35d9dec65e1002af734f50eddfd4f5cda5b8b..33b3a26d88a660fe737b144766c8dfdfa48ff685 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -16,10 +16,15 @@ import purescala.Definitions._
import _root_.smtlib.common._
import _root_.smtlib.printer.{ RecursivePrinter => SMTPrinter }
-import _root_.smtlib.parser.Commands.{ Constructor => SMTConstructor, FunDef => _, Assert => SMTAssert, _ }
+import _root_.smtlib.parser.Commands.{
+ Constructor => SMTConstructor,
+ FunDef => _,
+ Assert => _,
+ _
+}
import _root_.smtlib.parser.Terms.{
Forall => SMTForall,
- Exists => SMTExists,
+ Exists => _,
Identifier => SMTIdentifier,
Let => SMTLet,
_
@@ -31,7 +36,7 @@ import _root_.smtlib.interpreters.ProcessInterpreter
trait SMTLIBTarget extends Interruptible {
val context: LeonContext
val program: Program
- protected val reporter: Reporter
+ protected def reporter = context.reporter
def targetName: String
diff --git a/src/main/scala/leon/solvers/sygus/SygusSolver.scala b/src/main/scala/leon/solvers/sygus/SygusSolver.scala
index b0a7f0aab8fdf8f49d5639a5cfc94154a489948f..6d2c7678947c07fb6c53da2beac902e1fb25dbd5 100644
--- a/src/main/scala/leon/solvers/sygus/SygusSolver.scala
+++ b/src/main/scala/leon/solvers/sygus/SygusSolver.scala
@@ -4,24 +4,16 @@ package leon
package solvers
package sygus
-import utils._
-import grammars._
-
import purescala.Common._
import purescala.Definitions._
-import purescala.Types._
import purescala.ExprOps._
-import purescala.Extractors._
import purescala.Constructors._
import purescala.Expressions._
-import scala.collection.mutable.ArrayBuffer
-
import synthesis.Problem
import leon.solvers.smtlib._
-import _root_.smtlib.common._
import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
import _root_.smtlib.parser.Commands.{FunDef => SMTFunDef, _}
import _root_.smtlib.parser.CommandsResponses.{Error => _, _}
@@ -31,8 +23,6 @@ abstract class SygusSolver(val context: LeonContext, val program: Program, val p
implicit val ctx = context
implicit val debugSection = leon.utils.DebugSectionSynthesis
- val reporter = context.reporter
-
protected def unsupported(t: Tree, str: String): Nothing = {
throw new Unsupported(t, str)
}
diff --git a/src/main/scala/leon/synthesis/rules/SygusCVC4.scala b/src/main/scala/leon/synthesis/rules/SygusCVC4.scala
index 7a0e7edf495ef20597e4c9cde1939b5778ebcbbb..7760b8c0d50f0f12958de870311ccba7daa85b22 100644
--- a/src/main/scala/leon/synthesis/rules/SygusCVC4.scala
+++ b/src/main/scala/leon/synthesis/rules/SygusCVC4.scala
@@ -4,11 +4,9 @@ package leon
package synthesis
package rules
-import purescala.Types._
import solvers.sygus._
import grammars._
-import utils._
case object SygusCVC4 extends Rule("SygusCVC4") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
diff --git a/src/main/scala/leon/utils/InterruptManager.scala b/src/main/scala/leon/utils/InterruptManager.scala
index 29a79bafbfab37caebe74ae62d4410f97af72f20..40d8dd1836a8eacecadbc823c68e29fa4b232ca7 100644
--- a/src/main/scala/leon/utils/InterruptManager.scala
+++ b/src/main/scala/leon/utils/InterruptManager.scala
@@ -5,36 +5,32 @@ package utils
import scala.collection.JavaConversions._
-import java.util.concurrent.atomic.AtomicBoolean
+import java.util.concurrent.atomic.{AtomicLong, AtomicBoolean}
import sun.misc.{Signal, SignalHandler}
import java.util.WeakHashMap
class InterruptManager(reporter: Reporter) extends Interruptible {
private[this] val interruptibles = new WeakHashMap[Interruptible, Boolean]()
private[this] val sigINT = new Signal("INT")
- private[this] val withinTimeout: AtomicBoolean = new AtomicBoolean(false)
+
+ private[this] val lastTimestamp = new AtomicLong(0L)
+ private val exitWindow = 1000L
+
private[this] val handler = new SignalHandler {
def handle(sig: Signal) {
- println()
- if (withinTimeout.get()) {
+ def now(): Long = System.currentTimeMillis()
+ reporter.info("")
+ if (now() - lastTimestamp.get < exitWindow) {
reporter.warning("Aborting Leon...")
System.exit(1)
}
else {
reporter.warning("Interrupted...")
- setTimeout()
+ lastTimestamp.set(now())
interrupt()
}
}
}
- private val exitWindow = 1000
- private[this] def setTimeout() = {
- import scala.concurrent.Future
- import scala.concurrent.ExecutionContext.Implicits.global
- withinTimeout.set(true)
- Future { Thread.sleep(exitWindow) } onComplete { _ => withinTimeout.set(false) }
- ()
- }
val interrupted: AtomicBoolean = new AtomicBoolean(false)
diff --git a/src/test/resources/regression/verification/newsolvers/valid/AddingPositiveNumbers.scala b/src/test/resources/regression/verification/newsolvers/valid/AddingPositiveNumbers.scala
index ad5efa8794a974e620fe5c0ea936380a36dd562b..0b269ededa2e7bf3eb21203c4e1455d8fae9351f 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/AddingPositiveNumbers.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/AddingPositiveNumbers.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
object AddingPositiveNumbers {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala b/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala
index b5f30a7e10f59d917ff75ea2e3a63113f6dcc737..d3ad0237a88c6592702f1479397997f0324dd108 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
import leon.annotation._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/ArrayLiterals.scala b/src/test/resources/regression/verification/newsolvers/valid/ArrayLiterals.scala
index 01fb395fdb232536c2de589fdb3cac3a56c489fa..c3496b157e339725d823ff9f9d6fb586401d1e1d 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/ArrayLiterals.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/ArrayLiterals.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
object ArrayLiterals {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/ArrayUpdated.scala b/src/test/resources/regression/verification/newsolvers/valid/ArrayUpdated.scala
index 046745504078ebbf0b83ee4bb967d87fc5a751f1..e60918b6437d8a13d50fed7c793967d46aebd7aa 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/ArrayUpdated.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/ArrayUpdated.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/AssociativeList.scala b/src/test/resources/regression/verification/newsolvers/valid/AssociativeList.scala
index ad22edcd88daeb11f1b1d41f35dc48e5766ad0ad..39cc5b7326c3d1aa964055f6335336943b2afcf7 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/AssociativeList.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/AssociativeList.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
import leon.annotation._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/BestRealTypes.scala b/src/test/resources/regression/verification/newsolvers/valid/BestRealTypes.scala
index 9b1002f7f68f8594f65afd7dfebec9f9920e5f1c..6da51350f5bbf2abb6322393d96c4f3b3756ef6b 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/BestRealTypes.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/BestRealTypes.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/CaseObject1.scala b/src/test/resources/regression/verification/newsolvers/valid/CaseObject1.scala
index e46c15305d243b5a07b328813b40eb41964585e7..4a71c913afbde28a0e7cff3081cbeb68cecfa391 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/CaseObject1.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/CaseObject1.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
object CaseObject1 {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Field1.scala b/src/test/resources/regression/verification/newsolvers/valid/Field1.scala
index 7865db5e17b7c7a68acff16c1a4f5dee466f9833..be10c683da7f6bb8c940964ddf26f0ae3e3bec06 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/Field1.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/Field1.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
object Field1 {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Field2.scala b/src/test/resources/regression/verification/newsolvers/valid/Field2.scala
index 659b64815d6e068b17734670bfb65359205218d4..6b52ca258823af46754f7156a8cc78b2a741c3fd 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/Field2.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/Field2.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
object Field2 {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/FiniteSort.scala b/src/test/resources/regression/verification/newsolvers/valid/FiniteSort.scala
index 149dd4ac5ab4d70919a72b1e5d6f9d779e1e6d3b..a9b5ff6b656a48675723dca9fc07dcd07f1d05cb 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/FiniteSort.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/FiniteSort.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Generics.scala b/src/test/resources/regression/verification/newsolvers/valid/Generics.scala
index f4c5c1b20bf0b6183e94d34d7c51de8eac7aa499..14045bf32057cc50955acc0118d845b0afbab95b 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/Generics.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/Generics.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Generics1.scala b/src/test/resources/regression/verification/newsolvers/valid/Generics1.scala
index 3ad9b7df9a5090a1abfa268f3bdbcbd7a57f2119..d269f21785a401991a0bc077e3fc53ae2e42bf20 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/Generics1.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/Generics1.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Heaps.scala b/src/test/resources/regression/verification/newsolvers/valid/Heaps.scala
index 11f577ea10ff699fa0d849ed21120f5124758bbb..876fb5a2ac6467c9679a86e0a27effa532c5d622 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/Heaps.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/Heaps.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala b/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
index 0a922e2a478401c44aee156d968bdd0b97986008..05889fcb726ff88728959172f2127128831802c2 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/InstanceOf1.scala b/src/test/resources/regression/verification/newsolvers/valid/InstanceOf1.scala
index 14dab69bcd3df6e4030542d333e41b6f3ce7c56a..6543f94e5c66df0a073fe88770885e3bd408c0ac 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/InstanceOf1.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/InstanceOf1.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
object InstanceOf1 {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala b/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala
index 5b162a58b3d2b5d600e2cb8321d17b538bceef82..d54b5b86ecf6137d084df96a45fe3852ae486c23 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/LiteralMaps.scala b/src/test/resources/regression/verification/newsolvers/valid/LiteralMaps.scala
index 0acd6c81e2bbfb14a9bad85ba5d4ed891366822e..eea0009f2576c8a74b2a319b92bb768cb9a7870c 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/LiteralMaps.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/LiteralMaps.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
object LiteralMaps {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MergeSort.scala b/src/test/resources/regression/verification/newsolvers/valid/MergeSort.scala
index 133c19bcacc59e53955a214cd3a46c1b0109b4fd..2776a86c21baafc8b73112baaad01eab1357974f 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/MergeSort.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/MergeSort.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MyMap.scala b/src/test/resources/regression/verification/newsolvers/valid/MyMap.scala
index 84e9c4967c53609caf9aaeb5584e727a48c788e3..4f656c5960aff42f2c28dd32f7765d22af6261e5 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/MyMap.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/MyMap.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MySet.scala b/src/test/resources/regression/verification/newsolvers/valid/MySet.scala
index 19b83a93d6e57d33c7dfd9d763b35d51782d2129..b19be90e73d5b7981baefc3e8908c69719722de4 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/MySet.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/MySet.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MyTuple1.scala b/src/test/resources/regression/verification/newsolvers/valid/MyTuple1.scala
index b7fa2e8c3a0ad1470b568beb399be42995c231f3..9aa42ce056da6a877f59f99f4abbacd55060d65a 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/MyTuple1.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/MyTuple1.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
object MyTuple1 {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MyTuple2.scala b/src/test/resources/regression/verification/newsolvers/valid/MyTuple2.scala
index 9117fab370cc56957aba2e3a8587551377f8cb47..05124ffbe0d2cbd1edb448d2925d9762c767e443 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/MyTuple2.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/MyTuple2.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
object MyTuple2 {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MyTuple3.scala b/src/test/resources/regression/verification/newsolvers/valid/MyTuple3.scala
index 7bae15f427d498f3ab402536db720682a8f26f06..20bb0eec9be4c735d6ef92abfd33e1d059fb8983 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/MyTuple3.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/MyTuple3.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
object MyTuple3 {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MyTuple4.scala b/src/test/resources/regression/verification/newsolvers/valid/MyTuple4.scala
index 77ba6dc1b141f310eddd1e05d0728b1577950f86..8b2ede8f299cc13fe70ee5bcf41fabca7b853e6c 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/MyTuple4.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/MyTuple4.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
object MyTuple4 {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MyTuple5.scala b/src/test/resources/regression/verification/newsolvers/valid/MyTuple5.scala
index a427c410debc8c87f89377bf404ac3d43d8b1a92..78c93bc2a0f8e5bfcd4e58126d1ad8d5ec4bf695 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/MyTuple5.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/MyTuple5.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
object MyTuple5 {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MyTuple6.scala b/src/test/resources/regression/verification/newsolvers/valid/MyTuple6.scala
index 85287265240ccd8d383912eb2f70d43ad16d4aa7..e6cff3917d077ef83c11b5c3965204ccbe15da55 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/MyTuple6.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/MyTuple6.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
object MyTuple6 {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Nat.scala b/src/test/resources/regression/verification/newsolvers/valid/Nat.scala
index eb7fe27c56595bfb442644e8f258305fafbc4bf2..498373c4ac3cb0c95948ac6d0b6e0831f74352f0 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/Nat.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/Nat.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/PropositionalLogic.scala b/src/test/resources/regression/verification/newsolvers/valid/PropositionalLogic.scala
index 4c2beb4c78bbcbe3177249b9866d6df73fa65bb6..66e3f84ecfa11a460c6e721f69cb44d51def285e 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/PropositionalLogic.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
import leon.annotation._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/RedBlackTree.scala b/src/test/resources/regression/verification/newsolvers/valid/RedBlackTree.scala
index edaee5e92a4d10eb089e6e9a91e3e27678d4f84a..e24935bbedb8f87e0778f29f44f3a4758560fc11 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/RedBlackTree.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/RedBlackTree.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.annotation._
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala b/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala
index f0fd1c13fae74b01176424d250df3aa5a3084f16..ba2380c6a4fc1518a77281d4521840b5159bfbc2 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
import leon.annotation._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Subtyping1.scala b/src/test/resources/regression/verification/newsolvers/valid/Subtyping1.scala
index e84f5bafab6ff4305fbc7a270189ad8f8bf665ff..e31801436891f05afd9e04cd01ef1274a6ef18f6 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/Subtyping1.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/Subtyping1.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Subtyping2.scala b/src/test/resources/regression/verification/newsolvers/valid/Subtyping2.scala
index bc96d0617a8bf2361e16c35316a15c8895eb71a2..eef9c65da55c0b4d0ed76802a82c720f79fd44e7 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/Subtyping2.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/Subtyping2.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon.lang._
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Unit1.scala b/src/test/resources/regression/verification/newsolvers/valid/Unit1.scala
index e1456aaa651ac72ce9211948880a56c170ac151c..a0683d303545f782004fda587e520c5abf676c02 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/Unit1.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/Unit1.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
object Unit1 {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Unit2.scala b/src/test/resources/regression/verification/newsolvers/valid/Unit2.scala
index f71ea0ff5e80be50f001d3ff41f9ddfccbd4f147..8a285ff23af02ff1ae907fd714da0ae46141db50 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/Unit2.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/Unit2.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
object Unit2 {
diff --git a/src/test/scala/leon/regression/verification/NewSolversSuite.scala b/src/test/scala/leon/regression/verification/NewSolversSuite.scala
index 6065d8232341060f0f0eeae735961ae8c5e73da3..15e02a693988e44be555c5e954be65cab4203086 100644
--- a/src/test/scala/leon/regression/verification/NewSolversSuite.scala
+++ b/src/test/scala/leon/regression/verification/NewSolversSuite.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.regression.verification
diff --git a/testcases/repair/Heap/Heap.scala b/testcases/repair/Heap/Heap.scala
index a3c064376563d4584aa76367b1da9faf72592489..7b70693c77dcee60b8998b7b76ab9d3c3acddc26 100644
--- a/testcases/repair/Heap/Heap.scala
+++ b/testcases/repair/Heap/Heap.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013
diff --git a/testcases/repair/Heap/Heap1.scala b/testcases/repair/Heap/Heap1.scala
index 7cd8659614e40551538866c6f929159864344244..9a4e074bb20f560c4dc6dc71750acccc545a942e 100644
--- a/testcases/repair/Heap/Heap1.scala
+++ b/testcases/repair/Heap/Heap1.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013
diff --git a/testcases/repair/Heap/Heap10.scala b/testcases/repair/Heap/Heap10.scala
index de5ae51d1796aa2e01101207f63fad657bfe02af..c27bc93507b847bb6af22200fc2b3cf3e13f0511 100644
--- a/testcases/repair/Heap/Heap10.scala
+++ b/testcases/repair/Heap/Heap10.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013
diff --git a/testcases/repair/Heap/Heap2.scala b/testcases/repair/Heap/Heap2.scala
index 175f55d194e3379cb3120d7da3cc507c6ce6b923..a975f5c65e73c44c69adfa00348ee6b5c775e30e 100644
--- a/testcases/repair/Heap/Heap2.scala
+++ b/testcases/repair/Heap/Heap2.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013
diff --git a/testcases/repair/Heap/Heap3.scala b/testcases/repair/Heap/Heap3.scala
index 5b9fadeeb819a9704aa173a9b8b1bf8b0d956d61..3305b5d15a0731bd3aeaa1269c2404807f49a266 100644
--- a/testcases/repair/Heap/Heap3.scala
+++ b/testcases/repair/Heap/Heap3.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013
diff --git a/testcases/repair/Heap/Heap4.scala b/testcases/repair/Heap/Heap4.scala
index f6176a56ae67e927c2f38d333de253b84bb25b4a..46c78c8fd25dc5519aa6d8bddba257eb1e7c39e2 100644
--- a/testcases/repair/Heap/Heap4.scala
+++ b/testcases/repair/Heap/Heap4.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013
diff --git a/testcases/repair/Heap/Heap5.scala b/testcases/repair/Heap/Heap5.scala
index 5bbccada58e538033e6a12fc51ffc2683f9a1392..4e963e3bd63b913bb960dc0640f52aa2d9150723 100644
--- a/testcases/repair/Heap/Heap5.scala
+++ b/testcases/repair/Heap/Heap5.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013
diff --git a/testcases/repair/Heap/Heap6.scala b/testcases/repair/Heap/Heap6.scala
index 2760af2fa849bf642908661a0d5c0dba276776da..d284bb3804496fddadd8edced8c8fd98ddf5217c 100644
--- a/testcases/repair/Heap/Heap6.scala
+++ b/testcases/repair/Heap/Heap6.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013
diff --git a/testcases/repair/Heap/Heap7.scala b/testcases/repair/Heap/Heap7.scala
index b2232fa7b2f59ef9af0b1cddb3d461b7f04ca91f..ed4d189ce0f4c8dd78327f707627c1e9319b9187 100644
--- a/testcases/repair/Heap/Heap7.scala
+++ b/testcases/repair/Heap/Heap7.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013
diff --git a/testcases/repair/Heap/Heap8.scala b/testcases/repair/Heap/Heap8.scala
index 3debf1630a31dbcc3d36ba5c98f22f21a3551647..2564dceb8678e25dafabdc81b2dee125f63928ea 100644
--- a/testcases/repair/Heap/Heap8.scala
+++ b/testcases/repair/Heap/Heap8.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013
diff --git a/testcases/repair/Heap/Heap9.scala b/testcases/repair/Heap/Heap9.scala
index 4ed28b8677a40779d9ea586d274808723f1e4d08..4f5f4f3986d1daabb3ce3e9e94440ebe9235f7b8 100644
--- a/testcases/repair/Heap/Heap9.scala
+++ b/testcases/repair/Heap/Heap9.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013
diff --git a/testcases/repair/List/List.scala b/testcases/repair/List/List.scala
index 5f95f7595299a2f2c479efdb26a1b358218f55a0..043cd86ad8e600434adb9933d984d8e7a679fa43 100644
--- a/testcases/repair/List/List.scala
+++ b/testcases/repair/List/List.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.custom
diff --git a/testcases/repair/List/List1.scala b/testcases/repair/List/List1.scala
index 86910a60424ee14176bf3f467798cfe90e01856c..b2802d5f5135b8aadecaad999b1d7e00b97ae2c4 100644
--- a/testcases/repair/List/List1.scala
+++ b/testcases/repair/List/List1.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.custom
diff --git a/testcases/repair/List/List10.scala b/testcases/repair/List/List10.scala
index 61751947dc5e8c149f9c7d756af7d8458bb09655..81cf37c6b32b5b70c095c81efe6d94d14da7c8b4 100644
--- a/testcases/repair/List/List10.scala
+++ b/testcases/repair/List/List10.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.custom
diff --git a/testcases/repair/List/List11.scala b/testcases/repair/List/List11.scala
index 01ea114501a40dc5f9d01740cedfca1d4198cd3e..73c76fecc8acfb2d0719e73e694474a8158f0b9c 100644
--- a/testcases/repair/List/List11.scala
+++ b/testcases/repair/List/List11.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.custom
diff --git a/testcases/repair/List/List12.scala b/testcases/repair/List/List12.scala
index eeada312b1a4cd9e80ad4e735696e3e214ac6612..2f8afafd14d3665a51747ab5742c1821183c5823 100644
--- a/testcases/repair/List/List12.scala
+++ b/testcases/repair/List/List12.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.custom
diff --git a/testcases/repair/List/List13.scala b/testcases/repair/List/List13.scala
index dec461f0add16ceccd63f78d7401fef0c84b9057..914f0caacd49b42448ec428df24af6ea155c53d2 100644
--- a/testcases/repair/List/List13.scala
+++ b/testcases/repair/List/List13.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.custom
diff --git a/testcases/repair/List/List2.scala b/testcases/repair/List/List2.scala
index 77fa7f0f99aecc37a5405d91186d63b2965ed3be..d035e3933b6d509cf6535e850997daa166260b60 100644
--- a/testcases/repair/List/List2.scala
+++ b/testcases/repair/List/List2.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.custom
diff --git a/testcases/repair/List/List3.scala b/testcases/repair/List/List3.scala
index 5624d7db964356214dfc2ad6166f3334a7ecc4ca..7ab14a218574d20a17379ac6cfb4aa60f48dbda3 100644
--- a/testcases/repair/List/List3.scala
+++ b/testcases/repair/List/List3.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.custom
diff --git a/testcases/repair/List/List4.scala b/testcases/repair/List/List4.scala
index 0e0aad1eec0d83a16d12f8e8e8b09ad6d7bdce99..b6cb5e276741be29d86da86b7c43cbe7e1639c62 100644
--- a/testcases/repair/List/List4.scala
+++ b/testcases/repair/List/List4.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.custom
diff --git a/testcases/repair/List/List5.scala b/testcases/repair/List/List5.scala
index 2e8099bce966a6911c44adc77c5f33291c06b24d..743cced6533536eac8c03bbc3f2381378b8190b8 100644
--- a/testcases/repair/List/List5.scala
+++ b/testcases/repair/List/List5.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.custom
diff --git a/testcases/repair/List/List6.scala b/testcases/repair/List/List6.scala
index 1cf527cfa280387e49d64384210238a38c2e12cc..7ccf9ef721afe93f8276f9dc9cea65b1971d5a35 100644
--- a/testcases/repair/List/List6.scala
+++ b/testcases/repair/List/List6.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.custom
diff --git a/testcases/repair/List/List7.scala b/testcases/repair/List/List7.scala
index 4a2d34262d383c70e929d3df04f00cb7b2b711d6..7eef0585e9cb467f75da05fdb7957db4f9838afa 100644
--- a/testcases/repair/List/List7.scala
+++ b/testcases/repair/List/List7.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.custom
diff --git a/testcases/repair/List/List8.scala b/testcases/repair/List/List8.scala
index 3d79f043401117032505980ea6ee2b7f6d501d40..faf7571e9582f652e3ba494b11eb34c5923d4dac 100644
--- a/testcases/repair/List/List8.scala
+++ b/testcases/repair/List/List8.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.custom
diff --git a/testcases/repair/List/List9.scala b/testcases/repair/List/List9.scala
index c9d528a945c07080469d2591563f3d6a61a4c319..12a8152b1701fe993f36c33392eebda724ec4aad 100644
--- a/testcases/repair/List/List9.scala
+++ b/testcases/repair/List/List9.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
package leon.custom
diff --git a/testcases/repair/Numerical/Numerical.scala b/testcases/repair/Numerical/Numerical.scala
index 06d0516abbf5beb1bcad8ec8c9a994bb5a16ce06..bad9160654675694afd68519089fcf1d0d5b35a3 100644
--- a/testcases/repair/Numerical/Numerical.scala
+++ b/testcases/repair/Numerical/Numerical.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon._
import leon.lang._
diff --git a/testcases/repair/Numerical/Numerical1.scala b/testcases/repair/Numerical/Numerical1.scala
index 0818b015677e02be9661db68d8d0b8bb4a2d6e2d..6223cc54703f5377047695ea21420701098e5f8d 100644
--- a/testcases/repair/Numerical/Numerical1.scala
+++ b/testcases/repair/Numerical/Numerical1.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon._
import leon.lang._
diff --git a/testcases/repair/Numerical/Numerical2.scala b/testcases/repair/Numerical/Numerical2.scala
index a5eb3595f311e96d8a3d40bd36e66f6a46c60947..4315c8a07f7f56a7598a9425c911e807825e428d 100644
--- a/testcases/repair/Numerical/Numerical2.scala
+++ b/testcases/repair/Numerical/Numerical2.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon._
import leon.lang._
diff --git a/testcases/repair/Numerical/Numerical3.scala b/testcases/repair/Numerical/Numerical3.scala
index 5e0dbee5950b00fa99395f7aaf0c6db7c0d361e1..593bbd604d0aa1d2c8080cba1c2cd4fafb28132a 100644
--- a/testcases/repair/Numerical/Numerical3.scala
+++ b/testcases/repair/Numerical/Numerical3.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
import leon._
import leon.lang._
diff --git a/testcases/repair/inria/HeapSort.scala b/testcases/repair/inria/HeapSort.scala
index 46be0f31a1a0855d31ed4b0ec929aa3d7cb5a49a..01d2616894cea1f97629afa2359c0a1e6ebe2f92 100644
--- a/testcases/repair/inria/HeapSort.scala
+++ b/testcases/repair/inria/HeapSort.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013
diff --git a/testcases/verification/datastructures/AVLTree.scala b/testcases/verification/datastructures/AVLTree.scala
index d94d2da3aa86435867956846a60d9fe1053b3231..02eed85a3d1a223fe926308eca78052ba0f9335a 100644
--- a/testcases/verification/datastructures/AVLTree.scala
+++ b/testcases/verification/datastructures/AVLTree.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Manos (modified by Ravi)
* Date: 20.11.2013
diff --git a/testcases/verification/datastructures/BinaryTrie.scala b/testcases/verification/datastructures/BinaryTrie.scala
index 97871e87113f7393a27f2279a121c9faa4c6ae8d..bf064f9366fbec6d6029d0b01107e2eca3fda02e 100644
--- a/testcases/verification/datastructures/BinaryTrie.scala
+++ b/testcases/verification/datastructures/BinaryTrie.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013
diff --git a/testcases/verification/datastructures/HeapSort.scala b/testcases/verification/datastructures/HeapSort.scala
index 96e11022bed451f4224bad7b01028efd6e703d6f..935bf9efc1933ba7ae067c4b122120de09bbb2d3 100644
--- a/testcases/verification/datastructures/HeapSort.scala
+++ b/testcases/verification/datastructures/HeapSort.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013
diff --git a/testcases/verification/datastructures/LeftistHeap.scala b/testcases/verification/datastructures/LeftistHeap.scala
index 629c1013969132416be8e32b598049d9e9f5a69c..7617b981672829ec8d1940897f5ecbead0e57946 100644
--- a/testcases/verification/datastructures/LeftistHeap.scala
+++ b/testcases/verification/datastructures/LeftistHeap.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2013 EPFL, Lausanne
+/* Copyright 2009-2015 EPFL, Lausanne
*
* Author: Ravi
* Date: 20.11.2013