-
Notifications
You must be signed in to change notification settings - Fork 250
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
Generate SMT-LIB #8279
Comments
Given "Generated 1 VCC(s), 1 remaining after simplification" I am very much surprised that the above is all the output you got. Would you mind sharing |
Thanks for your reply, this is my cpp code, which is very simple. My purpose is to generate the SMT model corresponding to C++, so I consider using CBMC, hoping that it can meet my needs:
|
@MJJ-Shuai, on running the above program, I got the following output:
The program is simple enough and there is no non determinism here. The output you are getting on |
@ArpitaDutta Thanks for your reply, but my purpose is to generate the SMT formula corresponding to C++, so I wonder if CBMC can generate SMT formulas for C++? |
Hello, my question is:
When I use the above command below to convert my C++ code to SMT-LIB code, I find that I cannot find the assert I defined in the generated SMT2 file. It seems that cbmc has hidden it. If I want to see the details of SMT-LIB (with assert, declare, etc.), I will be able to use this command.
What instructions should I use?
SMT-LIB:
The text was updated successfully, but these errors were encountered: