diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 9222a381e..d9d900377 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1146,7 +1146,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing
         }
 
         Expr copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);
-        if (Options.ModelViewFile != null && pc is AssumeCmd captureStateAssumeCmd)
+        if (Options.ExpectingModel && pc is AssumeCmd captureStateAssumeCmd)
         {
           string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");
           if (description != null)