stanford-centaur / smt-switch

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

Linker for CVC5 requires x86-64 #358

Open iblumenfeld opened 2 days ago

iblumenfeld commented 2 days ago

I'm getting an error trying to run the setup script on Apple silicon because the CVC5 build seems to require x86-64. I have CVC5 already installed fine as a standalone executable, but there seems to be some issue with the smt-switch version of the config that doesn't permit this.

cvc5::internal::prop::CadicalSolver::isFixed(unsigned long long) const in libcvc5.a[110](cadical.cpp.o) ld: symbol(s) not found for architecture x86_64 c++: error: linker command failed with exit code 1 (use -v to see invocation)

CyanoKobalamyne commented 1 day ago

Thanks for the report. I am not able to reproduce this. See this run for an example: https://github.com/stanford-centaur/smt-switch/actions/runs/11601894545/job/32305661197.

Could you give some more details about your setup? What commands are you running exactly?

iblumenfeld commented 10 hours ago

I was running the setup-smt-switch.sh shell script from the pono install. I'll try to track down exactly where the failure occurs and update.

CyanoKobalamyne commented 10 hours ago

Oh I see. Are you passing any arguments to the script? Just so that I can try to run the exact same thing.