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