diff --git a/src/main/scala/viper/gobra/Gobra.scala b/src/main/scala/viper/gobra/Gobra.scala
index 3b1e71757..3f87f865e 100644
--- a/src/main/scala/viper/gobra/Gobra.scala
+++ b/src/main/scala/viper/gobra/Gobra.scala
@@ -17,6 +17,7 @@ import scalaz.Scalaz.futureInstance
 import viper.gobra.ast.internal.Program
 import viper.gobra.ast.internal.transform.{CGEdgesTerminationTransform, ConstantPropagation, InternalTransform, OverflowChecksTransform}
 import viper.gobra.backend.BackendVerifier
+import viper.gobra.backend.ViperBackends.{CarbonBackend, SiliconBackend}
 import viper.gobra.frontend.PackageResolver.{AbstractPackage, RegularPackage}
 import viper.gobra.frontend.Parser.ParseResult
 import viper.gobra.frontend.info.{Info, TypeInfo}
@@ -26,7 +27,11 @@ import viper.gobra.translator.Translator
 import viper.gobra.util.Violation.{KnownZ3BugException, LogicException, UglyErrorMessage}
 import viper.gobra.util.{DefaultGobraExecutionContext, GobraExecutionContext}
 import viper.silicon.BuildInfo
+import viper.silver.ast.pretty.FastPrettyPrinter
+import viper.silver.utility.ManualProgramSubmitter
 import viper.silver.{ast => vpr}
+import viper.silver.ast.pretty.FastPrettyPrinter
+import viper.silver.utility.ManualProgramSubmitter
 
 import java.time.format.DateTimeFormatter
 import java.time.LocalTime
@@ -51,6 +56,8 @@ object GoVerifier {
 
 trait GoVerifier extends StrictLogging {
 
+  protected var submitters: Map[String, ManualProgramSubmitter] = Map()
+
   def name: String = {
     this.getClass.getSimpleName
   }
@@ -82,9 +89,18 @@ trait GoVerifier extends StrictLogging {
       }
     })
 
+    val viperBackendName: String = config.backend match {
+      case CarbonBackend => "Carbon"
+      case SiliconBackend => "Silicon"
+    }
+
     val timeFormatter = DateTimeFormatter.ofPattern("HH:mm:ss");
     config.packageInfoInputMap.keys.foreach(pkgInfo => {
       val pkgId = pkgInfo.id
+
+      //adds a submitter for this package to submitters if config.submitForEvaluation is set, key is pkgId
+      createSubmitter(config.submitForEvaluation, pkgId, viperBackendName)
+
       logger.info(s"Verifying package $pkgId [${LocalTime.now().format(timeFormatter)}]")
       val future = verify(pkgInfo, config.copy(reporter = statsCollector, taskName = pkgId))(executor)
         .map(result => {
@@ -95,6 +111,12 @@ trait GoVerifier extends StrictLogging {
           warningCount += warnings.size
           warnings.foreach(w => logger.debug(w))
 
+          submitters.get(pkgId).foreach(s => {
+            s.setSuccess(result == VerifierResult.Success)
+            s.submit()}
+          )
+          submitters = submitters.removed(pkgId)
+
           result match {
             case VerifierResult.Success => logger.info(s"$name found no errors")
             case VerifierResult.Failure(errors) =>
@@ -143,6 +165,13 @@ trait GoVerifier extends StrictLogging {
     if (allErrors.isEmpty) VerifierResult.Success else VerifierResult.Failure(allErrors)
   }
 
+  private def createSubmitter(allowSubmission: Boolean, id: String, verifier: String): Unit = {
+    if (allowSubmission) {
+      val submitter = new ManualProgramSubmitter(true, "", "Gobra", verifier, Array())
+      submitters = submitters + (id -> submitter)
+    }
+  }
+
   protected[this] def verify(pkgInfo: PackageInfo, config: Config)(implicit executor: GobraExecutionContext): Future[VerifierResult]
 }
 
@@ -163,6 +192,10 @@ class Gobra extends GoVerifier with GoIdeVerifier {
       viperTask <- performViperEncoding(finalConfig, pkgInfo, program)
     } yield (viperTask, finalConfig)
 
+    submitters.get(pkgInfo.id).foreach(s => task.bimap(
+      _ => s.setAllowSubmission(false), //don't submit since no viper program could be produced
+      { case (job, _) => s.setProgram(FastPrettyPrinter.pretty(job.program)) }))
+
     task.foldM({
       case Vector() => Future(VerifierResult.Success)
       case errors => Future(VerifierResult.Failure(errors))
diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala
index 95d12bdc2..87e9dbea1 100644
--- a/src/main/scala/viper/gobra/frontend/Config.scala
+++ b/src/main/scala/viper/gobra/frontend/Config.scala
@@ -77,6 +77,7 @@ object ConfigDefaults {
   val DefaultDisableCheckTerminationPureFns: Boolean = false
   val DefaultUnsafeWildcardOptimization: Boolean = false
   val DefaultEnableMoreJoins: Boolean = false
+  val DefaultSubmitForEvaluation = false
 }
 
 // More-complete exhale modes
@@ -145,6 +146,7 @@ case class Config(
                    requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers,
                    disableSetAxiomatization: Boolean = ConfigDefaults.DefaultDisableSetAxiomatization,
                    disableCheckTerminationPureFns: Boolean = ConfigDefaults.DefaultDisableCheckTerminationPureFns,
+                   submitForEvaluation: Boolean = ConfigDefaults.DefaultSubmitForEvaluation,
                    unsafeWildcardOptimization: Boolean = ConfigDefaults.DefaultUnsafeWildcardOptimization,
                    enableMoreJoins: Boolean = ConfigDefaults.DefaultEnableMoreJoins,
 
@@ -200,6 +202,7 @@ case class Config(
       requireTriggers = requireTriggers || other.requireTriggers,
       disableSetAxiomatization = disableSetAxiomatization || other.disableSetAxiomatization,
       disableCheckTerminationPureFns = disableCheckTerminationPureFns || other.disableCheckTerminationPureFns,
+      submitForEvaluation = submitForEvaluation || other.submitForEvaluation,
       unsafeWildcardOptimization = unsafeWildcardOptimization && other.unsafeWildcardOptimization,
       enableMoreJoins = enableMoreJoins || other.enableMoreJoins,
     )
@@ -258,6 +261,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
                       requireTriggers: Boolean = ConfigDefaults.DefaultRequireTriggers,
                       disableSetAxiomatization: Boolean = ConfigDefaults.DefaultDisableSetAxiomatization,
                       disableCheckTerminationPureFns: Boolean = ConfigDefaults.DefaultDisableCheckTerminationPureFns,
+                      submitForEvaluation: Boolean = ConfigDefaults.DefaultSubmitForEvaluation,
                       unsafeWildcardOptimization: Boolean = ConfigDefaults.DefaultUnsafeWildcardOptimization,
                       enableMoreJoins: Boolean = ConfigDefaults.DefaultEnableMoreJoins,
                      ) {
@@ -275,6 +279,7 @@ case class BaseConfig(gobraDirectory: Path = ConfigDefaults.DefaultGobraDirector
       case _ => Some(positions.toVector)
     }
   }
+  def allowSubmission: Boolean = submitForEvaluation && !shouldChop
 }
 
 trait RawConfig {
@@ -320,6 +325,7 @@ trait RawConfig {
     requireTriggers = baseConfig.requireTriggers,
     disableSetAxiomatization = baseConfig.disableSetAxiomatization,
     disableCheckTerminationPureFns = baseConfig.disableCheckTerminationPureFns,
+    submitForEvaluation = baseConfig.allowSubmission,
     unsafeWildcardOptimization = baseConfig.unsafeWildcardOptimization,
     enableMoreJoins = baseConfig.enableMoreJoins,
   )
@@ -765,6 +771,13 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     default = Some(ConfigDefaults.DefaultDisableSetAxiomatization),
     noshort = true,
   )
+
+  val submitForEvaluation = opt[Boolean](name = "submitForEvaluation",
+    descr = "Whether to allow storing the current program for future evaluation.",
+    default = Some(false),
+    noshort = true
+  )
+
   /**
     * Exception handling
     */
@@ -964,6 +977,7 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals
     requireTriggers = requireTriggers(),
     disableSetAxiomatization = disableSetAxiomatization(),
     disableCheckTerminationPureFns = disableCheckTerminationPureFns(),
+    submitForEvaluation = submitForEvaluation(),
     unsafeWildcardOptimization = unsafeWildcardOptimization(),
     enableMoreJoins = enableMoreJoins(),
   )