From 9d96c290cfaada26843cda8f8d415b7129a01a91 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 7 Dec 2023 16:44:49 -0800 Subject: [PATCH] Don't create trivial labeled assumptions (#823) Previously, `{:id ...}` attributes were copied from `assert` statements to `assume` statements unconditionally, even when subsumption was disabled. This led to `{:id ...}` attributes on `assume true` statements, which will never be necessary for a proof, so there's no reason to track them. --- Source/VCGeneration/VCGen.cs | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/Source/VCGeneration/VCGen.cs b/Source/VCGeneration/VCGen.cs index 1cc591207..ed3393daa 100644 --- a/Source/VCGeneration/VCGen.cs +++ b/Source/VCGeneration/VCGen.cs @@ -58,9 +58,12 @@ public static AssumeCmd AssertTurnedIntoAssume(VCGenOptions options, AssertCmd a } var assume = new AssumeCmd(assrt.tok, expr); - // Copy any {:id ...} from the assertion to the assumption, so - // we can track it while analyzing verification coverage. - (assume as ICarriesAttributes).CopyIdFrom(assrt.tok, assrt); + if (expr != Expr.True) { + // Copy any {:id ...} from the assertion to the assumption, so + // we can track it while analyzing verification coverage. But + // skip it if it's `true` because that's never useful to track. + (assume as ICarriesAttributes).CopyIdFrom(assrt.tok, assrt); + } return assume; }