From ac3fc66f6a0ae5689b017469f2b0cbbcd39aae4a Mon Sep 17 00:00:00 2001 From: Aleksandr Fedchin Date: Thu, 18 Jan 2024 16:21:37 -0800 Subject: [PATCH] Use ExpectingModel flag --- Source/VCGeneration/ConditionGeneration.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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)