generate model for all expressions BTOR_OPT_MODEL_GEN not working

[sy6sy2]

In betortypes.h we can read:

* **BTOR_OPT_MODEL_GEN**
      | Enable (``value``: 1 or 2) or disable (``value``: 0) generation of a
        model for satisfiable instances.
      | There are two modes for model generation:
      * generate model for asserted expressions only (``value``: 1)
      * generate model for all expressions (``value``: 2)

But even with the value 2 the boolector_print_model function only gives model for declare-fun variables but not for define-fun variables.

Is it a bug?

Thank you.

PS: My define-fun variables come from an SMTLIB file parsed with boolector_parse_smt2.

To reproduce, parse this file:

(set-logic QF_ABV)
(declare-fun memory0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun eax0 () (_ BitVec 32))
(declare-fun ebx0 () (_ BitVec 32))
(declare-fun ecx0 () (_ BitVec 32))
(declare-fun edx0 () (_ BitVec 32))
(declare-fun esi0 () (_ BitVec 32))
(declare-fun edi0 () (_ BitVec 32))
(declare-fun ebp0 () (_ BitVec 32))
(declare-fun esp0 () (_ BitVec 32))
(assert (= esp0 (_ bv65536 32)))
(assert (= ebp0 (_ bv65536 32)))
(define-fun res321 () (_ BitVec 32) (_ bv0 32))
(define-fun OF1 () (_ BitVec 1) (_ bv0 1))
(define-fun SF1 () (_ BitVec 1) (ite (bvslt res321 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))
(define-fun ZF1 () (_ BitVec 1) (bvcomp res321 (_ bv0 32)))
(define-fun AF1 () (_ BitVec 1) (_ bv0 1))
(define-fun PF1 () (_ BitVec 1) (bvnot (bvxor (bvxor (bvxor (bvxor (bvxor (bvxor (bvxor ((_ extract 0 0) res321) ((_ extract 1 1) res321)) ((_ extract 2 2) res321)) ((_ extract 3 3) res321)) ((_ extract 4 4) res321)) ((_ extract 5 5) res321)) ((_ extract 6 6) res321)) ((_ extract 7 7) res321))))
(define-fun CF1 () (_ BitVec 1) (_ bv0 1))
(define-fun eax1 () (_ BitVec 32) res321)
(define-fun res322 () (_ BitVec 32) eax1)
(define-fun OF2 () (_ BitVec 1) (_ bv0 1))
(define-fun SF2 () (_ BitVec 1) (ite (bvslt res322 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))
(define-fun PF2 () (_ BitVec 1) (bvnot (bvxor (bvxor (bvxor (bvxor (bvxor (bvxor (bvxor ((_ extract 0 0) res322) ((_ extract 1 1) res322)) ((_ extract 2 2) res322)) ((_ extract 3 3) res322)) ((_ extract 4 4) res322)) ((_ extract 5 5) res322)) ((_ extract 6 6) res322)) ((_ extract 7 7) res322))))
(define-fun ZF2 () (_ BitVec 1) (bvcomp res322 (_ bv0 32)))
(define-fun CF2 () (_ BitVec 1) (_ bv0 1))
(define-fun cond_expr1 () (_ BitVec 1) ZF2)

and call boolector_print_model.

I only obtain:

(model
  (define-fun eax0 () (_ BitVec 32) (_ bv0 32))
  (define-fun ebx0 () (_ BitVec 32) (_ bv0 32))
  (define-fun ecx0 () (_ BitVec 32) (_ bv0 32))
  (define-fun edx0 () (_ BitVec 32) (_ bv0 32))
  (define-fun esi0 () (_ BitVec 32) (_ bv0 32))
  (define-fun edi0 () (_ BitVec 32) (_ bv0 32))
  (define-fun ebp0 () (_ BitVec 32) (_ bv65536 32))
  (define-fun esp0 () (_ BitVec 32) (_ bv65536 32))
)

But I would like also see cons_expr1, CF2, etc ...

Or even better, I would like to get model of only one variable (see https://github.com/Boolector/boolector/issues/50)

Thank

[mpreiner]

This is not a bug, but intended behaviour. Value 2 of the option internally builds a model for all expressions so that you can query all assignments via boolector_{array,bv}_assignment, but it does not change the way Boolector prints models.

[mpreiner]

@SylvainCecchetto let me know if you have more questions. I'll close the issue for now.