How to use smt solver in CBMC(C Bounded Model Checking)?

77 views Asked by At

I want to know how to use SMT Solver in CBMC. Generally we use minisat solver (SAT Solver) for constraint Solving in cbmc. But I want to use SMT Solvers for constraint solving in CBMC. I have gone through some references regarding the same, but didn't get a clear picture on the same. Is there any command to use SMT solver in CBMC ? Please help me with this.

1

There are 1 answers

0
alias On

Let’s say you want to use z3. Should simply be a matter of:

$ cbmc --z3 prog.c

assuming you already installed z3 beforehand. What have you tried?