You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We always ask for a witness in the properties and store them. However, in general the witness production is more expensive, and we never used the witness so far. Furthermore, the property types are currently mutable for this reason, and witnesses cannot be stored with Conjunction etc. (see #474).
I propose to instead add an optional argument witness::Bool=false to the check function, and then optionally return the witness immediately to the caller.
The text was updated successfully, but these errors were encountered:
We always ask for a witness in the properties and store them. However, in general the witness production is more expensive, and we never used the witness so far. Furthermore, the property types are currently mutable for this reason, and witnesses cannot be stored with
Conjunction
etc. (see #474).I propose to instead add an optional argument
witness::Bool=false
to thecheck
function, and then optionally return the witness immediately to the caller.The text was updated successfully, but these errors were encountered: