@whitequark@mastodon.social @unlambda@hachyderm.io @regehr@mastodon.social @lenary@types.pl I don't know how the loops in your language work, but if you can feasibly enumerate all the states the loop will pass through (e.g. it is independent of the actual values in the vector and the length of the vector), then you won't need an inductive invariant. If the loop count is dependent on the length of the vector, then you will need one, though you could usually run the equivalence check for some limited vector lengths. But it's easy to start and check with direct SMT-LIB if it will work.