SMT2 interface - Githubissues

esbmc / esbmc

The efficient SMT-based context-bounded model checker (ESBMC)

http://esbmc.org/

Other

278 stars 91 forks source link

SMT2 interface #1021

Open rafaelsamenezes opened 1 year ago

rafaelsamenezes commented 1 year ago

What is the current status of our SMT2 output? It would be great if we could produce formulas that could be sent directly to other solvers via FILE or STDIN. In that way we don't rely on the solvers being compiled with ESBMC which would improve supporting solvers with restricted licenses, no Windows support, or no API.

AFAIK we rely on the solvers to produce the formulas... however, it would be great if we could be solver agnostic here.

rafaelsamenezes commented 1 year ago

There is also an issue that we are producing large files. Comparing the output of the same category has issues:

AWS: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/aws-c-common/aws_add_size_saturating_harness_negated.i (ok) / https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/aws-c-common/aws_hash_iter_begin_harness_negated.i (crashes)
ECA generates huge files: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/eca-rers2012/Problem03_label08.c (generated a 200MB file)

I have used the flags --smtlib --output file.smt2 --unwind 20 --smt-formula-only in the smt-dump branch.

ibnyusuf commented 1 year ago

You mention "smt-dump" branch. Does this mean that the ability to output smtlib (directly, not via Z3) is not available on master?

rafaelsamenezes commented 1 year ago

You mention "smt-dump" branch. Does this mean that the ability to output smtlib (directly, not via Z3) is not available on master?

It is available. However, it will crash if you don't give a supported solver. The smt-dump branch allows to use the interface to just generate the formula and stop.