code: def _generic_model(self, z3_model):
          
          model = { }
          for m_f in z3_model:
              n = _z3_decl_name_str(m_f.ctx.ctx, m_f.ast).decode()
              m = m_f()
              me = z3_model.eval(m)
              model[n] = self._abstract_to_primitive(me.ctx.ctx, me.ast)
  
          return model
docs: Converts a Z3 model to a name->primitive dict.