Inconsistent behavior in `dump_smt` across solvers

The behavior in `::dump_smt` is not consistent across solvers:
 
Z3 dumps the smt formula to the file defined in `output`. If there is no file defined, it just swallows everything.
https://github.com/esbmc/esbmc/blob/9a2bd1847c5a8c68f255981abb5471bec123a1f4/src/solvers/z3/z3_conv.cpp#L1306-L1317

Note that this wasn't always the case; previously it would output to stdout when no `output` was defined:

https://github.com/esbmc/esbmc/pull/1342/commits/a2ff1a8dcc0ab1ec98d047e91655caee1565a169#diff-0489271635db802271e51ff12caa04e85c9fe16e8a38361d69256b0afbc802dfL1305-L1321

Bitwuzla always prints to stdout

https://github.com/esbmc/esbmc/blob/9a2bd1847c5a8c68f255981abb5471bec123a1f4/src/solvers/bitwuzla/bitwuzla_conv.cpp#L828-L832

Smtlib observes `output`

https://github.com/esbmc/esbmc/blob/9a2bd1847c5a8c68f255981abb5471bec123a1f4/src/solvers/smtlib/smtlib_conv.cpp#L163-L175

while Boolector again just prints to stdout:

https://github.com/esbmc/esbmc/blob/9a2bd1847c5a8c68f255981abb5471bec123a1f4/src/solvers/boolector/boolector_conv.cpp#L790-L793

This is annoying when you're wondering why `--z3 --smt-formula-only` doesn't print anything on stdout.
The `output` parameter is also overused:
it is used in smt-formula printing, vcc printing, goto2c printing and maybe somewhere else.

	void z3_convt::dump_smt()
	{
	const std::string &path = options.get_option("output");
	/* the iostream API is just unusable */
	if (path == "-")
	print_smt_formulae(std::cout);
	else
	{
	std::ofstream out(path);
	print_smt_formulae(out);
	}
	}

	void smtlib_convt::dump_smt()
	{
	auto path = config.options.get_option("output");
	if (path != "")
	{
	assert(emit_opt_output);
	emit_opt_output.emit("%s\n", "(check-sat)");
	if (path == "-")
	log_status("SMT formula written to standard output");
	else
	log_status("SMT formula written to output file {}", path);
	}
	}

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Inconsistent behavior in `dump_smt` across solvers #2167

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

	void bitwuzla_convt::dump_smt()
	{
	// Print formulas using binary bit-vector output format
	bitwuzla_print_formula(bitw, "smt2", messaget::state.out, 2);
	}

	void boolector_convt::dump_smt()
	{
	boolector_dump_smt2(btor, messaget::state.out);
	}

Inconsistent behavior in dump_smt across solvers #2167

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Inconsistent behavior in `dump_smt` across solvers #2167