Boolector: formula printing is broken

[daniel-raffler]

Hello,

formula printing in Boolector does not appear to be working right now. It's fine for some simple cases, like just printing a variable:

BooleanFormula f = bfmgr.makeVariable(name);
String s = mgr.dumpFormula(f).toString();

Here the output is (declare-fun a () (_ BitVec 1)), which is fine as Boolector encodes Booleans as Bitvectors. However, when printing terms the output only contains Smtlib for the term, without any surrounding (assert ...) or declarations for the symbols that were used. For instance, the following

BooleanFormula fa = bfmgr.makeVariable("a");
BooleanFormula fb = bfmgr.makeVariable("b");
BooleanFormula fc = bfmgr.makeVariable("c");
BooleanFormula f1 = bfmgr.or(fa, bfmgr.and(fb, fc));
String s1 = mgr.dumpFormula(f1).toString();

will only print

(bvnot (bvand (bvnot a) (bvnot (bvand b c))))

which is not valid Smtlib as the term would have to be surrounded by an (assert ...) and we're missing declarations for the variables

Also note, that when push was used, symbols appear to be prefixed with the current level of the assertion stack:

prover.push(bfmgr.makeVariable("x"));
BooleanFormula f = bfmgr.makeVariable("a");
String s = mgr.dumpFormula(f).toString();

This will print as (declare-fun BTOR_2@a () (_ BitVec 1)), and we'd have to remove the prefix manually to get the actual variable name

All of these examples are taken from BoolectorNativeApiTest, so this appears to be an old issue. I did look it up, and internally it appears like we're using boolector_dump_smt2_node to print the formulas. We may want to try switching to boolector_dump_smt2 instead to at least get the symbol declarations included in the dump

However, since Boolector is no longer being developed, we might as well just disable formula printing for it