Clauses Generated in CBMC

18 views
Skip to first unread message

Ipsita Koley

unread,
Jul 29, 2019, 9:23:14 AM7/29/19
to CProver Support
Is there any way to get the clauses and variables generated by CBMC which is fed to SAT solver

Michael Tautschnig

unread,
Jul 29, 2019, 9:36:03 AM7/29/19
to cprover...@googlegroups.com
Hello,

You can get them printed to your_file by running

cbmc input.c —dimacs —outfile your_file

There is some information on the mapping between symbols and variables at the end of the output.

Best,
Michael

On 29 Jul 2019, at 14:23, Ipsita Koley <ikip...@gmail.com> wrote:

Is there any way to get the clauses and variables generated by CBMC which is fed to SAT solver

--

---
You received this message because you are subscribed to the Google Groups "CProver Support" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cprover-suppo...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/cprover-support/0e4e9322-d476-4652-b750-595409418b9d%40googlegroups.com.

Ipsita Koley

unread,
Jul 30, 2019, 4:13:18 AM7/30/19
to CProver Support
Yeah, I figured that out. Thank you :)
Reply all
Reply to author
Forward
0 new messages