void *__VERIFIER_nondet_pointer(void) ;
void __VERIFIER_error(void) ;
void __VERIFIER_assume(int expression) ;
int __VERIFIER_nondet_int(void) ;

void panic(const char *fmt, ...);
void int main(void);

void
panic(const char *fmt, ...)
{
        __VERIFIER_error();
}

int main() {                                                                    
        struct mbuf *m;                                                         
        int len, off;                                                           
                                                                                
        ip_init();                                                              
        ip6_init();                                                             
        m = m_gethdr(0, MT_HEADER);                                             
        m_tag_init(m);                                                          
                                                                                
        len = __VERIFIER_nondet_int();                                          
        __VERIFIER_assume(len > 0);                                             
        __VERIFIER_assume(len <= MHLEN);                                         
        off = __VERIFIER_nondet_int();                                          
        __VERIFIER_assume(off > 0);                                             
        __VERIFIER_assume(off <= len);                                          
                                                                                
        m->m_hdr.mh_len = m->M_dat.MH.MH_pkthdr.len = len;                      
        ip_deliver(&m, &off, IPPROTO_IP, AF_INET6);                             
}