search

stanford-centaur / smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.
Other
103 stars 40 forks source link

Trying to fix ci on macOS #313

Closed yoni206 closed 1 year ago

yoni206 commented 1 year ago

This is based on https://github.com/cvc5/cvc5/commit/d49b7fc1d1fbe54748b49f1a4923554dd8f6bc1e which seemes to work for cvc5.

yoni206 commented 1 year ago

Does not seem to work in our case... still doesn't find Cython.

yoni206 commented 1 year ago

@makaimann this seems to solve the cython problem. I suggest we merge it and then continue to work on the failed regression separaetly.

yoni206 commented 1 year ago

@makaimann also, regarding the failed regression: I did some binary search on CI runs and discovered that the failed line is this: https://github.com/stanford-centaur/smt-switch/blob/9155864b8e4cfbdb5a2bcbfca4c716772ba01cea/tests/test-disjointset.cpp#L65

Looking at it, I am not sure I understand -- why would we expect t == y? Maybe t == z?

makaimann commented 1 year ago

Thanks for working on this @yoni206! The first expect true makes sense to me, but you’re right about the others. @ahmed-irfan, do you have any input on that? We might just be misunderstanding the disjoint set. Very strange that it doesn’t fail locally though.

CyanoKobalamyne commented 1 year ago

Very strange that it doesn’t fail locally though.

That test (disjointset) did fail for me locally recently when running make test, for what it's worth. I can't reproduce it right now, but I recompiled smt-switch with many different sets of options, so the issue probably only gets triggered in some configurations.

yoni206 commented 1 year ago

Thanks for checking and for the help with this! Finally CI is passing...