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

Dynlink error #17

Open
Hakimba opened this issue Nov 30, 2021 · 0 comments
Open

Dynlink error #17

Hakimba opened this issue Nov 30, 2021 · 0 comments

Comments

@Hakimba
Copy link

Hakimba commented Nov 30, 2021

Hi, i just followed the README and when i try cameleer on the example.ml you give, i have this error and a black why3 screen.

/.../..../.opam/4.12.0/lib/why3/plugins/plugin_cameleer cannot be loaded: 
Dynlink error: error loading shared library: Dynlink error: error loading shared library: 

Failure("dlopen(/...../..../.opam/4.12.0/lib/why3/plugins/plugin_cameleer.cmxs, 0x0006): 
symbol not found in flat namespace '_camlSexplib0__Sexp_conv'")

When i run why3 config detect i have this

Found prover Alt-Ergo version 2.4.0, OK.
Found prover Z3 version 4.8.10 (alternative: counterexamples)
Found prover Z3 version 4.8.10, OK.
Found prover Z3 version 4.8.10 (alternative: noBV)
Found prover Coq version 8.14.0, but no Why3 libraries were compiled for it
4 prover(s) added
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant