[QUESTION] Get SMT formula about esbmc

[MJJ-Shuai]

@fbrausse Oh, I see. I will give it a try. Thank you again.

[fbrausse]

Hi @MJJ-Shuai. ESBMC can generate SMT formulas instead of solving the safety properties it normally checks with --smtlib --smt-formula-only --output FILE.smt2. There are other ways to generate such formulas, too, specific to each built-in solver. For that, replace --smtlib by, e.g., --z3 and you will notice that the result will be a different, but equi-satisfiable, formula understandable by Z3.

This program however is a bit too simple for ESBMC to regularly invoke an SMT solver for. ESBMC will solve it directly. However, by adding the options --unwind 1 --no-simplify it will generate such a formula. This one for --smtlib: gh-1829.txt Note that the --unwind bound is specific to this program. In general, when a program contains potentially unbounded loops, this bound could be higher or not exist at all without specialized solving strategies, such as k-induction.

You might find that the formula is relatively large compared to the given program. That is because a lot of it relates to setting up symbols required for dealing with lifetime properties of dynamically allocated objects and the address space in general.

[MJJ-Shuai]

@fbrausse Thanks for your quick reply, I will consider your suggestions. Besides, if I need to use cvc5,esbmc can also generate smt formula for it, right？

[fbrausse]

@fbrausse Thanks for your quick reply, I will consider your suggestions. Besides, if I need to use cvc5,esbmc can also generate smt formula for it, right？

ESBMC at the moment doesn't have a cvc5 backend, but it does have a cvc4 one. Unfortunately, the cvc4 backend can't produce SMT output files right now (it talks to the cvc4 API directly). However, the --smtlib output is the most general and should be understood by all SMT-Lib v2 compliant solvers including cvc5.

[lucasccordeiro]

@fbrausse: Can you please submit a PR to update our documentation https://ssvlab.github.io/esbmc/documentation.html#smt-backends with these commands?