diff --git a/src/main/scala/gvc/main.scala b/src/main/scala/gvc/main.scala
index cfb082f..ab586a1 100644
--- a/src/main/scala/gvc/main.scala
+++ b/src/main/scala/gvc/main.scala
@@ -391,13 +391,13 @@ object Main extends App {
         fileNames.irFileName,
         IRPrinter.print(ir, includeSpecs = true)
       )
-    if (config.dump.contains(Config.DumpSilver)) dump(silver.program.toString())
+    if (config.dump.contains(Config.DumpSilver)) dump(silver.toString())
     else if (config.saveFiles)
-      writeFile(fileNames.silverFileName, silver.program.toString())
+      writeFile(fileNames.silverFileName, silver.toString())
 
     val verificationStart = System.nanoTime()
     silicon.start()
-    silicon.verify(silver.program) match {
+    silicon.verify(silver) match {
       case verifier.Success => if (stopImmediately) silicon.stop()
       case verifier.Failure(errors) =>
         val message = errors.map(_.readableMessage).mkString("\n")
@@ -423,7 +423,7 @@ object Main extends App {
     if (config.dump.contains(Config.DumpC0))
       dumpC0(c0Source)
     VerifiedOutput(
-      silver.program,
+      silver,
       c0Source,
       ProfilingInfo(
         profilingInfo.getTotalConjuncts,
diff --git a/src/main/scala/gvc/transformer/IRSilver.scala b/src/main/scala/gvc/transformer/IRSilver.scala
index 73b4b79..20e2f43 100644
--- a/src/main/scala/gvc/transformer/IRSilver.scala
+++ b/src/main/scala/gvc/transformer/IRSilver.scala
@@ -4,14 +4,6 @@ import scala.collection.mutable
 
 case class SilverVarId(methodName: String, varName: String)
 
-class SilverProgram(
-  val program: vpr.Program,
-
-  // Map of (methodName, varName) Silver variables that represent the result
-  // of the invoke
-  val temporaryVars: Map[SilverVarId, IR.Invoke]
-)
-
 object IRSilver {
   def toSilver(program: IR.Program) = new Converter(program).convert()
 
@@ -22,22 +14,6 @@ object IRSilver {
     val RenamedResult = "_result$"
   }
 
-  private class TempVars(methodName: String, index: mutable.Map[SilverVarId, IR.Invoke]) {
-    private var counter = -1
-    val declarations = mutable.ListBuffer[vpr.LocalVarDecl]()
-
-    def next(invoke: IR.Invoke, t: vpr.Type): vpr.LocalVar = {
-      counter += 1
-      val name = Names.TempResultPrefix + counter
-
-      index += SilverVarId(methodName, name) -> invoke
-
-      val decl = vpr.LocalVarDecl(name, t)()
-      declarations += decl
-      decl.localVar
-    }
-  }
-
   class Converter(ir: IR.Program) {
     val fields = mutable.ListBuffer[vpr.Field]()
     val structFields = mutable.Map[IR.StructField, vpr.Field]()
@@ -48,11 +24,10 @@ object IRSilver {
       field
     }
 
-    def convert(): SilverProgram = {
+    def convert(): vpr.Program = {
       val predicates = ir.predicates.map(convertPredicate).toList
-      val tempVarIndex = mutable.Map[SilverVarId, IR.Invoke]()
       val methods = (
-        ir.methods.map(convertMethod(_, tempVarIndex)) ++
+        ir.methods.map(convertMethod) ++
         ir.dependencies.flatMap(_.methods.map(convertLibraryMethod))
       ).toList
       val fields = this.fields.toSeq.sortBy(_.name).toList
@@ -66,7 +41,7 @@ object IRSilver {
         Seq.empty
       )()
 
-      new SilverProgram(program, tempVarIndex.toMap)
+      program
     }
 
     private def returnVarDecl(t: Option[IR.Type]): List[vpr.LocalVarDecl] = {
@@ -92,17 +67,14 @@ object IRSilver {
       )()
     }
 
-    private def convertMethod(method: IR.Method, tempVarIndex: mutable.Map[SilverVarId, IR.Invoke]): vpr.Method = {
-      var tempCount = 0
+    private def convertMethod(method: IR.Method): vpr.Method = {
 
       val params = method.parameters.map(convertDecl).toList
-      val vars = method.variables.map(convertDecl).toList
+      val decls = method.variables.map(convertDecl).toList
       val ret = returnVarDecl(method.returnType)
       val pre = method.precondition.map(convertExpr).toSeq
       val post = method.postcondition.map(convertExpr).toSeq
-      val tempVars = new TempVars(method.name, tempVarIndex)
-      val body = method.body.flatMap(convertOp(_, tempVars)).toList
-      val decls = vars ++ tempVars.declarations.toList
+      val body = method.body.flatMap(convertOp).toList
 
       vpr.Method(
         method.name,
@@ -139,10 +111,10 @@ object IRSilver {
     def getReturnVar(method: IR.Method): vpr.LocalVar =
       vpr.LocalVar(Names.ReturnVar, convertType(method.returnType.get))()
 
-    private def convertOp(op: IR.Op, tempVars: TempVars): Seq[vpr.Stmt] = op match {
+    private def convertOp(op: IR.Op): Seq[vpr.Stmt] = op match {
       case iff: IR.If => {
-        val ifTrue = iff.ifTrue.flatMap(convertOp(_, tempVars)).toList
-        val ifFalse = iff.ifFalse.flatMap(convertOp(_, tempVars)).toList
+        val ifTrue = iff.ifTrue.flatMap(convertOp).toList
+        val ifFalse = iff.ifFalse.flatMap(convertOp).toList
         Seq(
           vpr.If(
             convertExpr(iff.condition),
@@ -157,7 +129,7 @@ object IRSilver {
           vpr.While(
             convertExpr(loop.condition),
             List(convertExpr(loop.invariant)),
-            vpr.Seqn(loop.body.flatMap(convertOp(_, tempVars)).toList, Seq.empty)()
+            vpr.Seqn(loop.body.flatMap(convertOp).toList, Seq.empty)()
           )()
         )
       }
@@ -172,7 +144,7 @@ object IRSilver {
           
           case None => invoke.callee.returnType match {
             case Some(retType) =>
-              Some(tempVars.next(invoke, convertType(retType)))
+              throw new IRException("Cannot convert invoke of non-void method with no target")
             case None =>
               None
           }
diff --git a/src/main/scala/gvc/transformer/IRTransformer.scala b/src/main/scala/gvc/transformer/IRTransformer.scala
index a3fd836..7fb5d6d 100644
--- a/src/main/scala/gvc/transformer/IRTransformer.scala
+++ b/src/main/scala/gvc/transformer/IRTransformer.scala
@@ -668,10 +668,13 @@ object IRTransformer {
       scope += new IR.Invoke(method, args, Some(target))
     }
 
-    def invokeVoid(input: ResolvedInvoke, scope: Scope): Unit = {
+    def invokeVoid(input: ResolvedInvoke, scope: MethodScope): Unit = {
       val method = resolveMethod(input)
       val args = input.arguments.map(arg => transformExpr(arg, scope))
-      scope += new IR.Invoke(method, args, None)
+      // Add a variable to capture the result, even when it is not used. (The
+      // [conditions of] Viper run-time checks may reference it.)
+      val target = method.returnType.map(t => scope.method.addVar(t))
+      scope += new IR.Invoke(method, args, target)
     }
 
     def resolveMethod(invoke: ResolvedInvoke): IR.MethodDefinition =
diff --git a/src/main/scala/gvc/weaver/Checker.scala b/src/main/scala/gvc/weaver/Checker.scala
index 53f9768..fa01901 100644
--- a/src/main/scala/gvc/weaver/Checker.scala
+++ b/src/main/scala/gvc/weaver/Checker.scala
@@ -1,6 +1,6 @@
 package gvc.weaver
 
-import gvc.transformer.{IR, SilverVarId}
+import gvc.transformer.IR
 import Collector._
 import scala.collection.mutable
 import scala.annotation.tailrec
@@ -8,33 +8,6 @@ import scala.annotation.tailrec
 object Checker {
   type StructIDTracker = Map[String, IR.StructField]
 
-  class CheckerMethod(
-      val method: IR.Method,
-      tempVars: Map[SilverVarId, IR.Invoke]
-  ) extends CheckMethod {
-    val resultVars = mutable.Map[String, IR.Expression]()
-    def resultVar(name: String): IR.Expression = {
-      resultVars.getOrElseUpdate(
-        name, {
-          val invoke = tempVars.getOrElse(
-            SilverVarId(method.name, name),
-            throw new WeaverException(s"Missing temporary variable '$name'")
-          )
-          invoke.target.getOrElse {
-            val retType = invoke.method.returnType.getOrElse(
-              throw new WeaverException(
-                s"Invalid temporary variable '$name' for void '${invoke.callee.name}'"
-              )
-            )
-            val tempVar = method.addVar(retType)
-            invoke.target = Some(tempVar)
-            tempVar
-          }
-        }
-      )
-    }
-  }
-
   def insert(program: Collector.CollectedProgram): Unit = {
     val runtime = CheckRuntime.addToIR(program.program)
 
@@ -61,7 +34,6 @@ object Checker {
   ): Unit = {
     val program = programData.program
     val method = methodData.method
-    val checkMethod = new CheckerMethod(method, programData.temporaryVars)
 
     val callsImprecise: Boolean = methodData.calls.exists(c =>
       programData.methods.get(c.ir.callee.name) match {
@@ -106,7 +78,7 @@ object Checker {
     }
 
     def getCondition(cond: Condition): IR.Expression = cond match {
-      case ImmediateCondition(expr) => expr.toIR(program, checkMethod, None)
+      case ImmediateCondition(expr) => expr.toIR(program, method, None)
       case cond: TrackedCondition   => conditionVars(cond)
       case NotCondition(value) =>
         new IR.Unary(IR.UnaryOp.Not, getCondition(value))
@@ -193,7 +165,7 @@ object Checker {
     // Insert the runtime checks
     // Group them by location and condition, so that multiple checks can be contained in a single
     // if block.
-    val context = CheckContext(program, checkMethod, implementation, runtime)
+    val context = CheckContext(program, method, implementation, runtime)
     for ((loc, checkData) <- groupChecks(methodData.checks)) {
       insertAt(
         loc,
@@ -205,7 +177,7 @@ object Checker {
 
           def getTemporaryOwnedFields(): IR.Var =
             temporaryOwnedFields.getOrElse {
-              val tempVar = context.method.method.addVar(
+              val tempVar = context.method.addVar(
                 context.runtime.ownedFieldsRef,
                 CheckRuntime.Names.temporaryOwnedFields
               )
@@ -394,7 +366,7 @@ object Checker {
             conds.map(
               c =>
                 new IR.Assign(conditionVars(c),
-                              c.value.toIR(program, checkMethod, retVal)))
+                              c.value.toIR(program, method, retVal)))
           })
       }
 
@@ -474,7 +446,7 @@ object Checker {
 
   case class CheckContext(
       program: IR.Program,
-      method: CheckMethod,
+      method: IR.Method,
       implementation: CheckImplementation,
       runtime: CheckRuntime
   )
@@ -604,7 +576,7 @@ object Checker {
     case u: CheckExpression.Unary =>
       nesting(u.operand) + 1
     case _: CheckExpression.Literal | _: CheckExpression.Var |
-        CheckExpression.Result | _: CheckExpression.ResultVar =>
+        CheckExpression.Result =>
       1
   }
 }
diff --git a/src/main/scala/gvc/weaver/Checks.scala b/src/main/scala/gvc/weaver/Checks.scala
index 35f82d2..1a37c36 100644
--- a/src/main/scala/gvc/weaver/Checks.scala
+++ b/src/main/scala/gvc/weaver/Checks.scala
@@ -4,11 +4,6 @@ import gvc.transformer.{IR, IRSilver}
 
 sealed trait Check
 
-trait CheckMethod {
-  def method: IR.Method
-  def resultVar(name: String): IR.Expression
-}
-
 object Check {
   def fromViper(
       check: vpr.Exp,
@@ -75,7 +70,7 @@ case class PredicateAccessibilityCheck(
 sealed trait CheckExpression extends Check {
   def toIR(
       p: IR.Program,
-      m: CheckMethod,
+      m: IR.Method,
       returnValue: Option[IR.Expression]
   ): IR.Expression
 
@@ -103,7 +98,7 @@ object CheckExpression {
     def op: IR.BinaryOp
     def toIR(
         p: IR.Program,
-        m: CheckMethod,
+        m: IR.Method,
         r: Option[IR.Expression]
     ): IR.Binary =
       new IR.Binary(op, left.toIR(p, m, r), right.toIR(p, m, r))
@@ -154,7 +149,7 @@ object CheckExpression {
     def op: IR.UnaryOp
     def toIR(
         p: IR.Program,
-        m: CheckMethod,
+        m: IR.Method,
         r: Option[IR.Expression]
     ): IR.Unary =
       new IR.Unary(op, operand.toIR(p, m, r))
@@ -168,15 +163,8 @@ object CheckExpression {
   }
 
   case class Var(name: String) extends Expr {
-    def toIR(p: IR.Program, m: CheckMethod, r: Option[IR.Expression]) = {
-      m.method.variable(name)
-    }
-    def guard = None
-  }
-
-  case class ResultVar(name: String) extends Expr {
-    def toIR(p: IR.Program, m: CheckMethod, r: Option[IR.Expression]) = {
-      m.resultVar(name)
+    def toIR(p: IR.Program, m: IR.Method, r: Option[IR.Expression]) = {
+      m.variable(name)
     }
     def guard = None
   }
@@ -191,14 +179,14 @@ object CheckExpression {
           throw new WeaverException(s"Field '$fieldName' does not exist")
         )
 
-    def toIR(p: IR.Program, m: CheckMethod, r: Option[IR.Expression]) =
+    def toIR(p: IR.Program, m: IR.Method, r: Option[IR.Expression]) =
       new IR.FieldMember(root.toIR(p, m, r), getIRField(p))
     
     def guard = Some(and(root.guard, Not(Eq(root, NullLit))))
   }
 
   case class Deref(operand: Expr) extends Expr {
-    def toIR(p: IR.Program, m: CheckMethod, r: Option[IR.Expression]) =
+    def toIR(p: IR.Program, m: IR.Method, r: Option[IR.Expression]) =
       new IR.DereferenceMember(operand.toIR(p, m, r))
     def guard = Some(and(operand.guard, Not(Eq(operand, NullLit))))
   }
@@ -208,24 +196,24 @@ object CheckExpression {
   }
 
   case class IntLit(value: Int) extends Literal {
-    def toIR(p: IR.Program, m: CheckMethod, r: Option[IR.Expression]) =
+    def toIR(p: IR.Program, m: IR.Method, r: Option[IR.Expression]) =
       new IR.IntLit(value)
   }
   case class CharLit(value: Char) extends Literal {
-    def toIR(p: IR.Program, m: CheckMethod, r: Option[IR.Expression]) =
+    def toIR(p: IR.Program, m: IR.Method, r: Option[IR.Expression]) =
       new IR.CharLit(value)
   }
   case class StrLit(value: String) extends Literal {
-    def toIR(p: IR.Program, m: CheckMethod, r: Option[IR.Expression]) =
+    def toIR(p: IR.Program, m: IR.Method, r: Option[IR.Expression]) =
       new IR.StringLit(value)
   }
   case object NullLit extends Literal {
-    def toIR(p: IR.Program, m: CheckMethod, r: Option[IR.Expression]) =
+    def toIR(p: IR.Program, m: IR.Method, r: Option[IR.Expression]) =
       new IR.NullLit()
   }
   sealed trait BoolLit extends Literal {
     def value: Boolean
-    def toIR(p: IR.Program, m: CheckMethod, r: Option[IR.Expression]) =
+    def toIR(p: IR.Program, m: IR.Method, r: Option[IR.Expression]) =
       new IR.BoolLit(value)
   }
   object BoolLit {
@@ -239,7 +227,7 @@ object CheckExpression {
   }
 
   case class Cond(cond: Expr, ifTrue: Expr, ifFalse: Expr) extends Expr {
-    def toIR(p: IR.Program, m: CheckMethod, r: Option[IR.Expression]) =
+    def toIR(p: IR.Program, m: IR.Method, r: Option[IR.Expression]) =
       new IR.Conditional(
         cond.toIR(p, m, r),
         ifTrue.toIR(p, m, r),
@@ -266,7 +254,7 @@ object CheckExpression {
   case object Result extends Expr {
     def toIR(
         p: IR.Program,
-        m: CheckMethod,
+        m: IR.Method,
         returnValue: Option[IR.Expression]
     ): IR.Expression =
       returnValue.getOrElse(
@@ -373,7 +361,6 @@ object CheckExpression {
         v.name match {
           case IRSilver.Names.ReturnVar => Result
           case IRSilver.Names.RenamedResult => Var(IRSilver.Names.ReservedResult)
-          case temp if temp.startsWith(IRSilver.Names.TempResultPrefix) => ResultVar(temp)
           case id => Var(id)
         }
 
diff --git a/src/main/scala/gvc/weaver/Collector.scala b/src/main/scala/gvc/weaver/Collector.scala
index ed4feb5..c3043ec 100644
--- a/src/main/scala/gvc/weaver/Collector.scala
+++ b/src/main/scala/gvc/weaver/Collector.scala
@@ -3,7 +3,7 @@ package gvc.weaver
 import gvc.transformer.IR.Predicate
 
 import scala.collection.mutable
-import gvc.transformer.{IR, SilverProgram, SilverVarId}
+import gvc.transformer.IR
 import viper.silver.ast.MethodCall
 import viper.silver.{ast => vpr}
 import viper.silicon.state.CheckPosition
@@ -61,7 +61,6 @@ object Collector {
 
   class CollectedProgram(
       val program: IR.Program,
-      val temporaryVars: Map[SilverVarId, IR.Invoke],
       val methods: Map[String, CollectedMethod]
   )
 
@@ -69,9 +68,9 @@ object Collector {
 
   def collect(
       irProgram: IR.Program,
-      vprProgram: SilverProgram
+      vprProgram: vpr.Program
   ): CollectedProgram = {
-    val checks = collectChecks(vprProgram.program)
+    val checks = collectChecks(vprProgram)
 
     val methods = irProgram.methods
       .map(
@@ -80,9 +79,9 @@ object Collector {
             m.name,
             collect(
               irProgram,
-              vprProgram.program,
+              vprProgram,
               m,
-              vprProgram.program.findMethod(m.name),
+              vprProgram.findMethod(m.name),
               checks
             )
         ))
@@ -90,7 +89,6 @@ object Collector {
 
     new CollectedProgram(
       program = irProgram,
-      temporaryVars = vprProgram.temporaryVars,
       methods = methods
     )
   }
diff --git a/src/main/scala/gvc/weaver/Weaver.scala b/src/main/scala/gvc/weaver/Weaver.scala
index 85ab0e7..4394381 100644
--- a/src/main/scala/gvc/weaver/Weaver.scala
+++ b/src/main/scala/gvc/weaver/Weaver.scala
@@ -1,11 +1,11 @@
 package gvc.weaver
 import gvc.transformer.IR
-import gvc.transformer.SilverProgram
+import viper.silver.{ast => vpr}
 
 class WeaverException(message: String) extends Exception(message)
 
 object Weaver {
-  def weave(ir: IR.Program, silver: SilverProgram): Unit = {
+  def weave(ir: IR.Program, silver: vpr.Program): Unit = {
     Checker.insert(Collector.collect(ir, silver))
   }
 }
diff --git a/src/test/resources/baseline/postcondition.baseline.c0 b/src/test/resources/baseline/postcondition.baseline.c0
index 4f7f10f..d7649c9 100644
--- a/src/test/resources/baseline/postcondition.baseline.c0
+++ b/src/test/resources/baseline/postcondition.baseline.c0
@@ -4,13 +4,14 @@ int test(int x, struct OwnedFields* _ownedFields);
 
 int main()
 {
+  int _ = 0;
   struct OwnedFields* _ownedFields = NULL;
   struct OwnedFields* _tempFields = NULL;
   int* _instanceCounter = NULL;
   _instanceCounter = alloc(int);
   _ownedFields = initOwnedFields(_instanceCounter);
   assert(true);
-  test(2, _ownedFields);
+  _ = test(2, _ownedFields);
   assert(true);
   return 0;
 }
diff --git a/src/test/resources/verifier/missing_result.output.c0 b/src/test/resources/verifier/missing_result.output.c0
index edac230..620b1b7 100644
--- a/src/test/resources/verifier/missing_result.output.c0
+++ b/src/test/resources/verifier/missing_result.output.c0
@@ -11,21 +11,21 @@ int doSomething(int x, int* _instanceCounter)
 int main()
 {
   int x = 0;
+  int _ = 0;
+  int _1 = 0;
   bool _cond_1 = false;
   int* _instanceCounter = NULL;
-  int _ = 0;
   struct OwnedFields* _ownedFields = NULL;
-  int _1 = 0;
   struct OwnedFields* _tempFields = NULL;
   _instanceCounter = alloc(int);
   _ownedFields = initOwnedFields(_instanceCounter);
-  _1 = doSomething(0, _instanceCounter);
+  _ = doSomething(0, _instanceCounter);
   _tempFields = initOwnedFields(_instanceCounter);
-  _cond_1 = _1 == 0;
+  _cond_1 = _ == 0;
   x = random(_tempFields);
   join(_ownedFields, _tempFields);
-  _ = doSomething(x, _instanceCounter);
-  if (!_cond_1 && !(_ == 0) || _cond_1 && !(_ == 0))
+  _1 = doSomething(x, _instanceCounter);
+  if (!_cond_1 && !(_1 == 0) || _cond_1 && !(_1 == 0))
   {
     assert(x == 0);
   }
diff --git a/src/test/resources/verifier/missing_result.vpr b/src/test/resources/verifier/missing_result.vpr
index 736a0cf..b116ad4 100644
--- a/src/test/resources/verifier/missing_result.vpr
+++ b/src/test/resources/verifier/missing_result.vpr
@@ -10,11 +10,11 @@ method main() returns ($result: Int)
   ensures true
 {
   var x: Int
-  var $result_0: Int
-  var $result_1: Int
-  $result_0 := doSomething(0)
+  var _: Int
+  var _1: Int
+  _ := doSomething(0)
   x := random()
-  $result_1 := doSomething(x)
+  _1 := doSomething(x)
   assert x == 0
   $result := 0
 }
diff --git a/src/test/scala/TestUtils.scala b/src/test/scala/TestUtils.scala
index 6c71d1d..966ce15 100644
--- a/src/test/scala/TestUtils.scala
+++ b/src/test/scala/TestUtils.scala
@@ -8,16 +8,17 @@ import fastparse.Parsed
 import gvc.analyzer._
 import gvc.transformer._
 import gvc.weaver.Weaver
+import viper.silver.{ast => vpr}
 
 case class TestProgram(
     ir: IR.Program,
-    silverProgram: SilverProgram
+    silverProgram: vpr.Program
 ) {
   def weave = Weaver.weave(ir, silverProgram)
 
   def irSource = IRPrinter.print(ir, true)
 
-  def silverSource = silverProgram.program.toString()
+  def silverSource = silverProgram.toString()
 }
 
 case class TestResource(file: Path) {
diff --git a/src/test/scala/permutation/PermutationSpec.scala b/src/test/scala/permutation/PermutationSpec.scala
index c0eb84b..71e87b0 100644
--- a/src/test/scala/permutation/PermutationSpec.scala
+++ b/src/test/scala/permutation/PermutationSpec.scala
@@ -8,7 +8,6 @@ import gvc.transformer.IR.{Method, Predicate}
 import org.scalatest.Outcome
 import org.scalatest.funsuite.FixtureAnyFunSuite
 
-import java.io.{File, FileWriter}
 import java.nio.file.Files
 import scala.collection.mutable