Good day!
Z3 says the following smt is SAT
(benchmark xx:logic QF_BV:extrafuns ((x Int)):assumption(and (> x 0) (< x 1) ))
with model "x -> val!0"
Yes, this code has an error: the correct logic is QF_LIA but not QF_BV (Z3 says UNSAT with QF_LIA and it is correct, of course). So, my question is what means "val!0" ? some unknown 0'th value ?