Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

undefined reference to CaDiCaL::Solver::flush_proof_trace(bool) #19

Open
filipeom opened this issue May 27, 2024 · 1 comment
Open

undefined reference to CaDiCaL::Solver::flush_proof_trace(bool) #19

filipeom opened this issue May 27, 2024 · 1 comment
Labels
help wanted Extra attention is needed type: bug

Comments

@filipeom
Copy link
Member

Getting:

File "bin/dune", line 11, characters 7-12:
11 |  (name main2)
            ^^^^^
/usr/bin/ld: /home/filipe/.local/share/opam/wasp/lib/cvc5/libcvc5.a(cadical.cpp.o): in function `cvc5::internal::prop::CadicalSolver::getProofSketch()':
cadical.cpp:(.text+0x56e): undefined reference to `CaDiCaL::Solver::flush_proof_trace(bool)'
collect2: error: ld returned 1 exit status
File "caml_startup", line 1:
Error: Error during linking (exit code 1)

On ubuntu server:

Description:    Ubuntu 23.10
Release:        23.10
Codename:       mantic

Need to investigate further

@filipeom filipeom added the bug label May 27, 2024
filipeom added a commit to filipeom/smtml that referenced this issue May 27, 2024
filipeom added a commit to formalsec/smtml that referenced this issue May 27, 2024
@filipeom filipeom added type: bug help wanted Extra attention is needed and removed bug labels Aug 20, 2024
@filipeom
Copy link
Member Author

filipeom commented Aug 21, 2024

Seems to only happen on ocaml 5.2

Seems to actually be problem with dynamic linking? We can have cvc5 on its only and its fine, when we have z3 or bitwuzla it prints out this error

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
help wanted Extra attention is needed type: bug
Projects
None yet
Development

No branches or pull requests

1 participant