Use correct flag when checking if captureState assumptions need to be…

… inserted (#835)

When discharging verification conditions, Boogie optionally inserts
`:captureState` assumptions into the AST. This improves error reporting
in case of a proof failure. Currently, these assumptions are only
inserted if the user wants to print the counterexample model to a file.
However, a counterexample model is sometimes used within Boogie without
being printed to a file, in which case the `:captureState` assumptions
should still be inserted. This PR changes the condition under which
Boogie adds `:captureState` assumptions to account for such scenarios.

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)