Current status: Trying to come up with sensible SMT2 encodings for circuit-based incremental ∃∀-problems (without throwing out all the code I already have for dealing with ordinary ∃-problems).pic.twitter.com/f5nDtDSZHi
Show this thread
I need this to encode concurrent SVA properties of the form assume property (regex1 |-> regex2); with arbitrary complex regex2. (Assert of the same thing is trivial, so is assume with a linear regex2.)