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
Right now, we're doing conditional derivability checks by looking at our predicate bank, and hoping that there exists some environment from vars --> values which satisfies the condition.
Instead of looking into randomly generated environments, we should actually just ask Z3 to synthesize a model from vars -> values.
The text was updated successfully, but these errors were encountered:
Right now, we're doing conditional derivability checks by looking at our predicate bank, and hoping that there exists some environment from vars --> values which satisfies the condition.
Instead of looking into randomly generated environments, we should actually just ask Z3 to synthesize a model from vars -> values.
The text was updated successfully, but these errors were encountered: