diff --git a/src/main/scala/viper/gobra/reporting/Message.scala b/src/main/scala/viper/gobra/reporting/Message.scala
index 5b9157e6d..61530d91b 100644
--- a/src/main/scala/viper/gobra/reporting/Message.scala
+++ b/src/main/scala/viper/gobra/reporting/Message.scala
@@ -166,7 +166,7 @@ case class GeneratedViperMessage(taskName: String, inputs: Vector[String], vprAs
   override val name: String = s"generated_viper_message"
 
   override def toString: String = s"generated_viper_message(" +
-    s"taskName=$taskName"
+    s"taskName=$taskName" +
     s"files=$inputs, " +
     s"vprFormated=$vprAstFormatted)"
 
diff --git a/src/main/scala/viper/gobra/translator/Translator.scala b/src/main/scala/viper/gobra/translator/Translator.scala
index a142a67d8..8cb2a1fab 100644
--- a/src/main/scala/viper/gobra/translator/Translator.scala
+++ b/src/main/scala/viper/gobra/translator/Translator.scala
@@ -15,6 +15,8 @@ import viper.gobra.translator.context.DfltTranslatorConfig
 import viper.gobra.translator.encodings.programs.ProgramsImpl
 import viper.gobra.translator.transformers.{AssumeTransformer, TerminationTransformer, ViperTransformer}
 import viper.gobra.util.Violation
+import viper.silver.ast.pretty.FastPrettyPrinter
+import viper.silver.{ast => vpr}
 
 object Translator {
 
@@ -37,8 +39,34 @@ object Translator {
       case (t, transformer) => transformer.transform(t)
     }
 
-    config.reporter report GeneratedViperMessage(config.taskName, config.packageInfoInputMap(pkgInfo).map(_.name), () => transformedTask.program, () => transformedTask.backtrack)
+    config.reporter report GeneratedViperMessage(config.taskName, config.packageInfoInputMap(pkgInfo).map(_.name), () => sortAst(transformedTask.program), () => transformedTask.backtrack)
     transformedTask
   }
 
+  /**
+    * sorts AST members alphabetically to ease the comparison of (similar) Viper ASTs
+    */
+  def sortAst(program: vpr.Program): vpr.Program = {
+    lazy val memberOrdering: Ordering[vpr.Member] = Ordering.by(_.name)
+    implicit lazy val domainFnOrdering: Ordering[vpr.DomainFunc] = Ordering.by(_.name)
+    implicit lazy val domainAxOrdering: Ordering[vpr.DomainAxiom] = Ordering.by(FastPrettyPrinter.pretty(_))
+
+    def sortDomain(domain: vpr.Domain): vpr.Domain = {
+      vpr.Domain(
+        domain.name,
+        domain.functions.sorted,
+        domain.axioms.sorted,
+        domain.typVars
+      )(domain.pos, domain.info, domain.errT)
+    }
+
+    vpr.Program(
+      program.domains.map(sortDomain).sorted(memberOrdering),
+      program.fields.sorted(memberOrdering),
+      program.functions.sorted(memberOrdering),
+      program.predicates.sorted(memberOrdering),
+      program.methods.sorted(memberOrdering),
+      program.extensions.sorted(memberOrdering),
+    )(program.pos, program.info, program.errT)
+  }
 }
diff --git a/src/main/scala/viper/gobra/translator/transformers/TerminationTransformer.scala b/src/main/scala/viper/gobra/translator/transformers/TerminationTransformer.scala
index 1809fa0c7..50465895c 100644
--- a/src/main/scala/viper/gobra/translator/transformers/TerminationTransformer.scala
+++ b/src/main/scala/viper/gobra/translator/transformers/TerminationTransformer.scala
@@ -6,13 +6,13 @@
 
 package viper.gobra.translator.transformers
 import java.nio.file.Path
-
 import viper.gobra.backend.BackendVerifier
 import viper.gobra.util.Violation
 import viper.silicon.Silicon
 import viper.silver.{ast => vpr}
 import viper.silver.frontend.{DefaultStates, ViperAstProvider}
-import viper.silver.plugin.standard.termination.TerminationPlugin
+import viper.silver.plugin.standard.predicateinstance.PredicateInstance.PredicateInstanceDomainName
+import viper.silver.plugin.standard.termination.{DecreasesTuple, TerminationPlugin}
 import viper.silver.reporter.{NoopReporter, Reporter}
 import viper.silver.plugin.standard.predicateinstance.PredicateInstancePlugin
 
@@ -26,9 +26,33 @@ class TerminationTransformer extends ViperTransformer {
     // constructs a separate Viper program (as a string) that should be parsed
     // after parsing this separate Viper program, the resulting AST is combined with `task`
 
+    val allImport = "decreases/all.vpr"
+    def type2Import(typ: vpr.Type): String = typ match {
+      case vpr.Bool => "decreases/bool.vpr"
+      case vpr.Int => "decreases/int.vpr"
+      case vpr.MultisetType(_) => "decreases/multiset.vpr"
+      case vpr.Perm => "decreases/rational.vpr"
+      case vpr.Ref => "decreases/ref.vpr"
+      case vpr.SeqType(_) => "decreases/seq.vpr"
+      case vpr.SetType(_) => "decreases/set.vpr"
+      case vpr.DomainType(name, _) if name == PredicateInstanceDomainName => "decreases/predicate_instance.vpr"
+      case _ => allImport // fallback
+    }
+
+    // find the types of all expressions used as decreases measues
+    val measureTypes = task.program.deepCollect {
+      case DecreasesTuple(tupleExpressions, _) => tupleExpressions.map(_.typ)
+    }.flatten.distinct
+    // map these types to the respective files that should be imported
+    val imports = measureTypes
+      .map(type2Import)
+      .distinct
+    // if `allImport` is in the list of files that should be imported, we can ignore all others and instead only import
+    // `allImport`
+    val importsAll = imports.contains(allImport)
     /** list of Viper standard imports that should be parsed */
-    val imports = Seq("decreases/all.vpr")
-    val progWithImports = imports.map(p => s"import <${p}>").mkString("\n")
+    val filteredImports = if (importsAll) Seq(allImport) else imports
+    val progWithImports = filteredImports.map(p => s"import <${p}>").mkString("\n")
     val vprProgram = parseVpr(progWithImports)
     combine(task, vprProgram)
   }