On Fri, 21 Oct 2022, Ivan Perez wrote:
[...]I might take a look at packaging cvc5, too, if it doesn't seem too difficult.What4 can use cvc4 if available, but it can't use cvc5 AFAIK. It's not one of the supported solvers:What4.Solver.Adapter What4.Solver.Boolector What4.Solver.CVC4 What4.Solver.DReal What4.Solver.ExternalABC What4.Solver.STP What4.Solver.Yices What4.Solver.Z3It might still make sense to package it, but it would not help address this issue, I don't think.
Oh, interesting. I was looking at the README.md in the what4 github repository, and there is some cvc5 code there:
https://github.com/GaloisInc/what4/blob/master/what4/src/What4/Solver/CVC5.hs But it seems that was added since the last what4 release, so you're right. Disabling the tests might be the best option for now. Scott