Miss some model

[SimpleXiaohu]

Variables without constraints do not generate model. Like the example below, the model of len_x and y will not be generated:

; sat
(declare-fun x ()String)
(declare-fun y ()String)

(declare-const len_x Int)
(declare-const len_y Int)

(assert (= len_x (str.len x)))
(assert (< 1 len_x))


(check-sat)
(get-model)

The result is:

Running backward propagation
   ... sat
(model
  (define-fun len_x () Int 2)
  (define-fun x () String "\u{0}\u{0}")
)

[SimpleXiaohu]

@pruemmer

[pruemmer]

This is a known problem, but usually not much of an issue. In the example, I get satisfying assignments for x and len_x. The variables y and len_y are not included in the model, because their value is irrelevant for satisfying the formula. You can use the command "get-value" to query assignments of y, len_y.

[SimpleXiaohu]

I have try to use z3 and cvc4 to solve this instance. And they will generate them all. May be we can support this feature?