[xsmith-dev] XSmith questions

[William G Hatch]

And it doesn't have global variables that you could lift to?

I ask mostly because I don't have a great answer for the other question.

(The answer should be “oh, you can specify types that a variable can't
be, and just use that when you make a decision that precludes certain
types without having to fully commit to a type”, as we've discussed,
but I still haven't implemented that.)

On Fri, Aug 27, 2021 at 04:03:30PM -0700, Sorawee Porncharoenwase wrote:
>Oh, and about this question:
>
>> In Dafny do function expressions not generate closures?
>>
>
>It does, but an important part of the language is top-level function
>expression definition, which would not have a lifting target.
>
>So yes, choice-filters-to-apply seems like a solution, but see my above
>question about how to use it properly.
>
>Thanks!