We tried using model.completion=true on inputs that use datatypes and found that (get-value ...) takes a minute or so and then errors with Overflow encountered when expanding vector. The oldest version I tested is 4.12.1, and I still see it on current master c137ef7fbaf847025ef0b4e47bb8e853c224fb34.
I minimized the input to the following:
$ cat min.smt2
(declare-datatypes ((s 0)) (((b (b Int)))))
(declare-fun t (Int) s)
(check-sat)
(get-value (t))
$ ./z3 model.completion=true min.smt
sat
*wait for a minute*
((error "line 4 column 14: Overflow encountered when expanding vector")
We tried using
model.completion=trueon inputs that use datatypes and found that(get-value ...)takes a minute or so and then errors withOverflow encountered when expanding vector. The oldest version I tested is 4.12.1, and I still see it on current master c137ef7fbaf847025ef0b4e47bb8e853c224fb34. I minimized the input to the following: