new option to disable checking for loop maintained invariants - this leads to an underapproximation that helps to speedup houdini refutation of candidates

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);