You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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?
The text was updated successfully, but these errors were encountered:
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.
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?
The text was updated successfully, but these errors were encountered: