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

Use Error-Unable to query solver: Connection timed out #882

Open
16061054 opened this issue Sep 6, 2024 · 1 comment
Open

Use Error-Unable to query solver: Connection timed out #882

16061054 opened this issue Sep 6, 2024 · 1 comment

Comments

@16061054
Copy link

16061054 commented Sep 6, 2024

As described in title, I build and use souper according to README.md, but it doesn't work.

Actually, it works in usage like '/path/to/souper-build path/to/example.bc' with static profile count. However, when I use it like '/path/to/souper-build path/to/example.bc -souper-use-cegis', meaning that I want it to perform optimization, I get output like this :

; Listing valid replacements.
; Using solver: Z3 + internal cache
Unable to query solver: Connection timed out

I try to use '-solver-timeout=60' and '--souper-internal-cache=false', and it still gets 'Unable to query solver'.

I even recover the command line param support of '-z3-path' according to commit for passing it the absolute path of z3, and it still gets 'Unable to query solver'.

May you help me to find out the problem indeed and the solution to it?

@16061054
Copy link
Author

16061054 commented Sep 6, 2024

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