splnitelnost, SMT, bit-vektory, Q3B, modely