diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala index fe1149bb0e947088635b6f942c28b3b5c4513a28..da8533fc4daacf85fbdbfd9ccb027fa8de32a427 100644 --- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala +++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala @@ -30,9 +30,19 @@ trait SMTLIBTarget { val interpreter = getNewInterpreter() - val out = new java.io.FileWriter(s"vcs-$targetName.smt2", true) + var out: java.io.FileWriter = _ + reporter.ifDebug { debug => - out.write("; -----------------------------------------------------\n") + val file = context.files.headOption.map(_.getName).getOrElse("NA") + val n = VCNumbers.getNext(targetName+file) + + val dir = new java.io.File("vcs"); + + if (!dir.isDirectory) { + dir.mkdir + } + + out = new java.io.FileWriter(s"vcs/$targetName-$file-$n.smt2", true) } def id2sym(id: Identifier): SSymbol = SSymbol(id.name+"!"+id.globalId) @@ -490,3 +500,12 @@ trait SMTLIBTarget { } } + +object VCNumbers { + private var nexts = Map[String, Int]().withDefaultValue(0) + def getNext(id: String) = { + val n = nexts(id)+1 + nexts += id -> n + n + } +}