We are not compatible with the development release of Dolmen due to the implicit field added in Gbury/dolmen#199. Further, we currently require that Dolmen move trigger annotations in SMT-LIB format from the body of the formula to the quantifier itself, but this was removed in Gbury/dolmen#207.
Since both of these will be part of the next release of dolmen, let us pre-emptively ensure that release won't break Alt-Ergo.
Note: this PR only makes sense for the v2.5.x branch. For the next branch, we already support Gbury/dolmen#199, and will adapt our code to support Gbury/dolmen#207 instead.
Halbaroth
commented
7 months ago
We are not compatible with the development release of Dolmen due to the
implicitfield added in Gbury/dolmen#199. Further, we currently require that Dolmen move trigger annotations in SMT-LIB format from the body of the formula to the quantifier itself, but this was removed in Gbury/dolmen#207.Since both of these will be part of the next release of dolmen, let us pre-emptively ensure that release won't break Alt-Ergo.
Note: this PR only makes sense for the
v2.5.xbranch. For thenextbranch, we already support Gbury/dolmen#199, and will adapt our code to support Gbury/dolmen#207 instead.