Peter Nightingale

Savile Row can't parse those question marks.

OK, that should be documented I suppose.

Which SR files should I be using? I need a param file to go with 395a and 395b above.

Well that was easy to diagnose. Indexing a matrix with a matrix is only (currently) implemented when the inner matrix is the only index. I'll see what I can do.

Are the two eprime files attached here out of date? I have done some work on matrices-indexed-by-matrices to implement this case, but actually it seems the error is in the...

Savile Row is doing what it's told, even though that doesn't make sense. It is told to produce the BV (nested) encoding, and run yices-smt2 and that combination does not...

That could be a savile row issue, i.e. the second SR to start is overwriting the files of the first one -- what are the filenames of the param files...

Hi Oz, do you think this would be an easy fix or lots of work? @ozgurakgun

Thanks Oz The constraint that uses Valid just says something like "s in Valid -> ...." where s is a sequence decision variable. imagine s is the sequence of digits...

Maybe I can avoid making Valid and just check the prefix condition some other way.