diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 241dbd2e092bd77e40a89a84c51e7d2b3f2ae79a..e9faa425c32880c2b312db677eb5846a7eb82ed9 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -66,7 +66,12 @@ abstract class SMTLIBSolver(val context: LeonContext,
 
     reporter.debug(s"Outputting VC into $fileName" )
 
-    new java.io.FileWriter(fileName, false)
+    val fw = new java.io.FileWriter(fileName, false)
+
+    fw.write("; Solver : "+name+"\n")
+    fw.write("; Options: "+interpreterOps(context).mkString(" ")+"\n")
+
+    fw
   } else None