Trivial goals are not user-friendly
When doing split_vc
on the weakest precondition of bar
let foo () requires { true } = ()
let bar () = foo (); foo ()
we get two subgoals true
marked as unknown. At this point, the user can either apply split_vc
or launch a prover, on each subgoal. In both cases, this is a waste of user time and processor cycles. This becomes especially noticeable after !207 (merged), as the number of trivial goals greatly increases.
Two possible solutions:
- Automatically mark
true
goals as proved. - Prevent
split_vc
from generating them.