Skip to content

Commit

Permalink
Don't copy ids when creating trivial assumptions
Browse files Browse the repository at this point in the history
When creating an assumption from an assertion, don't copy the id if the
resulting assumption is trivial (such as when subsumption is turned
off).
  • Loading branch information
atomb committed Dec 6, 2023
1 parent 9cc6140 commit 9a0bb7c
Showing 1 changed file with 6 additions and 3 deletions.
9 changes: 6 additions & 3 deletions Source/VCGeneration/VCGen.cs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down

0 comments on commit 9a0bb7c

Please sign in to comment.