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

Error regarding std::bad_alloc #265

Open
natureangel opened this issue Mar 7, 2024 · 1 comment
Open

Error regarding std::bad_alloc #265

natureangel opened this issue Mar 7, 2024 · 1 comment

Comments

@natureangel
Copy link

I encountered the following issue while using symbolosis to formal verification my module:
Unexpected response from solver: terminate called after throwing an instance of 'std::bad_alloc';
The running results are as follows:
engine_0 (smtbmc boolector) returned pass for basecase
engine_0 (smtbmc boolector) returned ERROR for induction
engine_0 did not produce any traces
Sometimes there is another issue that causes the program to interrupt:
Unexpected EOF response from solver.
May I ask what caused this problem and how to solve it?

@nakengelhardt
Copy link
Member

This means that the boolector process crashed. We've been able to trigger a similar bug by having an extremely large number of properties in a design, so it may be that your design is too large or has too many asserts.

You can try using a different solver by changing the line smtbmc boolector in [engines] to something else, e.g. smtbmc yices or btor btormc.

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

2 participants