1 files changed, 6 insertions, 1 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index fd7a4f72..1aed2cba 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1944,7 +1944,12 @@ namespace VC {
               b.Attributes = c.Attributes;
               b.ErrorData = c.ErrorData;
               prefixOfPredicateCmdsInit.Add(b);
-              b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);
+
+              if (CommandLineOptions.Clo.DisableLoopInvMaintainedAssert)
+                b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, Expr.True);
+              else
+                b = new Bpl.LoopInvMaintainedAssertCmd(c.tok, c.Expr);
+
               b.Attributes = c.Attributes; 
               b.ErrorData = c.ErrorData;
               prefixOfPredicateCmdsMaintained.Add(b);