Alex Gryzlov

icon indicating a website link https://software.imdea.org/~aliaksandr.hryzlou/

icon company IMDEA Software icon location Madrid icon location Logic, languages and systems

Results 113 comments of Alex Gryzlov

CVC5 failing to terminate on some tests

It seems that the problem with both tests is the inclusion of BitVector theory. If `set-logic` is changed from `ALL` to `UFLIRA` (`QF_UFLIRA` works for `Permutations` but not `ByteString.Lazy`) in...

No decreasing parameter even though constructor is unwrapped

Proving termination for functions defined on nested types is indeed often tricky in type theory, the typical advice in such a case is to have a specialized version of the...

Z3 required

I think at this point we should aim to support CVC5. The theory of strings should be quite similar in both Z3 and CVC5, so this is probably just some...