fixed bug for getting model from Z3; added regression test for it
fixed updating the empty map