Reduce verbosity with model-gen

[sy6sy2]

If you try with the attached file test.smt2.

With CVC4 you get:

 $ cvc4 --lang=smt2.6 --produce-models --incremental /tmp/test.smt2
sat
((esi2 (_ bv8328 32)))

With Z3 you get:

 $ z3 -smt2 pp.bv_literals=false /tmp/test.smt2
sat
((esi2 (_ bv8328 32)))

But with Boolector you get:

$ boolector --model-gen --incremental --smt2 --pretty-print=0 --dec --exit-codes=0 --output-format=smt2 /tmp/test.smt2
sat
((esi2 (_ bv8328 32)))
2[8172] 96 memory0
2[8173] 32 memory0
2[8174] 0 memory0
2[8175] 0 memory0
3 0 eax0
4 0 ebx0
5 0 ecx0
6 0 edx0
7 0 esi0
8 0 edi0
9 65536 ebp0
10 65536 esp0
11 0 OF0
12 0 SF0
13 0 ZF0
14 0 PF0
15 0 CF0
16 0 AF0
17 0 DF0
40[8172] 96 memory1
40[8173] 32 memory1
40[8174] 0 memory1
40[8175] 0 memory1
41 0 eax1
42 0 ebx1
43 0 ecx1
44 0 edx1
45 0 esi1
46 0 edi1
47 65536 ebp1
48 65536 esp1
49 0 OF1
50 0 SF1
51 0 ZF1
52 0 PF1
53 0 CF1
54 0 AF1
55 0 DF1

As expected, the 3 solvers give the same result, BUT Boolector prints some other information on my variables.

1. Is it the expected behavior?
2. Is there an option to disable this extra information?
3. If no option, can you tell me which lines in the source code I have to comment to disable this extra information in order to get the same output as Z3 and CVC4.

Thank you very munch for your help!

test.smt2.zip

[sy6sy2]

So, I finally found the line to comment!
I comment this line

boolector/src/btormain.c

Line 1584 in d46fb7b

boolector_print_model (btor, val ? "smt2" : "btor", g_app->outfile);

and I now have the same behavior as CVC4 and Z3.

I also notice another "issue", when you have an SMT2 file without any (check-sat) (so only declare-fun, define-fun, assert), if you run this file with CVC4 or Z3 then you get nothing on your stdout (for me this is the correct behavior because you did not ask for a check-sat, a get-value or a get-model BUT, with boolector you get a sat or unsat line on your stdout, even without asking for a (check-sat).

[mpreiner]

This is expected behaviour. Boolector by default prints the full model (get-model) if option -m is provided. The default output language for the model is the BTOR format. Since you also query a value via (get-value) you get ((esi2 (_ bv8328 32))) followed by the full model in BTOR. Just use (set-option :produce-models true) in you SMT files and don't specify -m. There is no need to comment out code. Now you also disabled (get-model).

Boolector will still solve the problem even if there is no (check-sat) in the file. We can change this behaviour for SMT2 input files.

[sy6sy2]

(set-option :produce-models true) is perfect!
Thank you very munch for your fast answer!