Consider supporting assert (expression) by (spinoff)

[utaal]

Suggested by @jaybosamiya as a prover performance management tool.

We have discussed offline what context would be auto-imported, and @jaybosamiya suggests we may want to implicitly import anything that had been explicitly asserted and the post-conditions of function calls in the preceding code. Importing all the learned facts from the outer context isn't technically possible, as those are part of prover state for a specific query. That is (as @tjhance says), we wouldn't import "things that Z3 deduces while proving earlier asserts, but which it wouldn't have in context if it just assumes them".

@jaybosamiya:

That (i.e., not having implicitly-learnt facts) is the behavior I would expect from a context-imported spinoff anyways (I would only expect explicitly-asserted facts, and program encoding to be part of the spinoff’d query). In particular, I would believe by (context-imported-spinoff) is not meant to be a magic “this will always work” anyways, but more of an expert’s hammer for someone who wants to chop down that context.

@utaal is a little worried from a user experience perspective that the imported context would be implicitly anything that's been asserted and the postconditions of function calls. This would not be spelled out in one place. Changing the preceding program would break the spunoff assert, and it wouldn't be clear what you missed. But that may still be okay in practice for the advanced users that would need this tool.