[SMT backend] ESBMC is not printing the SMT formula with Z3

[lucasccordeiro]

For some reason, ESBMC is not printing the SMT formula with Z3 when we use the options: --smt-formula-only and --smt-formula-too.

[mikhailramalho]

have you tried using "--verbosity 10"?

[lucasccordeiro]

It works! Thanks, Mikhail.

We should update our documentation. I'll leave this issue open while I update it.

Em ter., 14 de mar. de 2023 às 14:29, Mikhail R. Gadelha < @.***> escreveu:

have you tried using "--verbosity 10"?

— Reply to this email directly, view it on GitHub https://github.com/esbmc/esbmc/issues/929#issuecomment-1468207454, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA4F4HMSEOPHY2ZHVTTPVWDW4B6GNANCNFSM6AAAAAAV2QJ5VQ . You are receiving this because you authored the thread.Message ID: @.***>

-- Lucas C. Cordeiro​

https://ssvlab.github.io/lucasccordeiro/

[mikhailramalho]

Maybe we should "fix" it: since we are asking esbmc to print the formula, it should work without having to specify the verbosity, just like it works for goto and ssa.

Em ter., 14 de mar. de 2023 às 11:56, Lucas Cordeiro < @.***> escreveu:

It works! Thanks, Mikhail.

We should update our documentation. I'll leave this issue open while I update it.

Em ter., 14 de mar. de 2023 às 14:29, Mikhail R. Gadelha < @.***> escreveu:

have you tried using "--verbosity 10"?

— Reply to this email directly, view it on GitHub https://github.com/esbmc/esbmc/issues/929#issuecomment-1468207454, or unsubscribe < https://github.com/notifications/unsubscribe-auth/AA4F4HMSEOPHY2ZHVTTPVWDW4B6GNANCNFSM6AAAAAAV2QJ5VQ

. You are receiving this because you authored the thread.Message ID: @.***>

-- Lucas C. Cordeiro​

https://ssvlab.github.io/lucasccordeiro/

— Reply to this email directly, view it on GitHub https://github.com/esbmc/esbmc/issues/929#issuecomment-1468256529, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKEJH7RXFTPHYBC4WWRHVDW4CBLHANCNFSM6AAAAAAV2QJ5VQ . You are receiving this because you commented.Message ID: @.***>

--

Mikhail Ramalho.

[lucasccordeiro]

I agree.

Em ter., 14 de mar. de 2023 às 15:02, Mikhail R. Gadelha < @.***> escreveu:

Maybe we should "fix" it: since we are asking esbmc to print the formula, it should work without having to specify the verbosity, just like it works for goto and ssa.

Em ter., 14 de mar. de 2023 às 11:56, Lucas Cordeiro < @.***> escreveu:

It works! Thanks, Mikhail.

We should update our documentation. I'll leave this issue open while I update it.

Em ter., 14 de mar. de 2023 às 14:29, Mikhail R. Gadelha < @.***> escreveu:

have you tried using "--verbosity 10"?

— Reply to this email directly, view it on GitHub https://github.com/esbmc/esbmc/issues/929#issuecomment-1468207454, or unsubscribe <

https://github.com/notifications/unsubscribe-auth/AA4F4HMSEOPHY2ZHVTTPVWDW4B6GNANCNFSM6AAAAAAV2QJ5VQ

. You are receiving this because you authored the thread.Message ID: @.***>

-- Lucas C. Cordeiro​

https://ssvlab.github.io/lucasccordeiro/

— Reply to this email directly, view it on GitHub https://github.com/esbmc/esbmc/issues/929#issuecomment-1468256529, or unsubscribe < https://github.com/notifications/unsubscribe-auth/AAKEJH7RXFTPHYBC4WWRHVDW4CBLHANCNFSM6AAAAAAV2QJ5VQ

. You are receiving this because you commented.Message ID: @.***>

--

Mikhail Ramalho.

— Reply to this email directly, view it on GitHub https://github.com/esbmc/esbmc/issues/929#issuecomment-1468271539, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA4F4HOBZXVLQBK3ABZE6KTW4CB7FANCNFSM6AAAAAAV2QJ5VQ . You are receiving this because you authored the thread.Message ID: @.***>

-- Lucas C. Cordeiro​

https://ssvlab.github.io/lucasccordeiro/

[fbrausse]

I agree and proposed something like this in https://github.com/esbmc/esbmc/discussions/678, maybe we can decide on that here.

[luamfb]

I have run into the same issue with --smt-formula-too in the Z3 backend, however changing verbosity did not solve it.

Running in gdb, it appears the relevant code is in the call to dump_smt in the bmct::run_decision_procedure method. The string returned by dump_smt is never used. With the Z3 backend, the method z3_convt::dump_smt is called, and the returned string seems to be what contains the SMT formula, as all printing is done to a ostringstream instance. Meanwhile, with the Bitwuzla backend, the method bitwuzla_convt::dump_smt actually prints the string through the call to the external function bitwuzla_print_formula.