nakengelhardt
commented
3 months ago 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？