You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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 c137ef7.
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")
The text was updated successfully, but these errors were encountered:
We tried using
model.completion=true
on 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 c137ef7.I minimized the input to the following:
The text was updated successfully, but these errors were encountered: