(set-logic QF_BV)
(declare-fun __ESBMC_ptr_obj_start_0 () (_ BitVec 64))
(declare-fun __ESBMC_ptr_obj_end_0 () (_ BitVec 64))
(declare-fun __ESBMC_ptr_obj_start_1 () (_ BitVec 64))
(declare-fun __ESBMC_ptr_obj_end_1 () (_ BitVec 64))
(declare-fun |smt_conv::__ESBMC_ptr_addr_range_0..start0| () (_ BitVec 64))
(declare-fun |smt_conv::__ESBMC_ptr_addr_range_0..end0| () (_ BitVec 64))
(declare-fun |smt_conv::__ESBMC_ptr_addr_range_1..start0| () (_ BitVec 64))
(declare-fun |smt_conv::__ESBMC_ptr_addr_range_1..end0| () (_ BitVec 64))
(declare-fun |smt_conv::smt_conv::collate_array_vals::3..start0| () (_ BitVec 64))
(declare-fun |smt_conv::smt_conv::collate_array_vals::3..end0| () (_ BitVec 64))
(declare-fun |smt_conv::smt_conv::collate_array_vals::4..start0| () (_ BitVec 64))
(declare-fun |smt_conv::smt_conv::collate_array_vals::4..end0| () (_ BitVec 64))
(declare-fun |smt_conv::smt_conv::collate_array_vals::7..start0| () (_ BitVec 64))
(declare-fun |smt_conv::smt_conv::collate_array_vals::7..end0| () (_ BitVec 64))
(declare-fun |c:@u&0#11| () (_ BitVec 800032))
(declare-fun |nondet$symex::nondet8| () (_ BitVec 800032))
(declare-fun |execution_statet::\guard_exec?0!0| () (_ BitVec 1))
(assert 
 (= __ESBMC_ptr_obj_start_0 #b0000000000000000000000000000000000000000000000000000000000000000))
(assert 
 (= #b0000000000000000000000000000000000000000000000000000000000000000 __ESBMC_ptr_obj_end_0))
(assert 
 (= __ESBMC_ptr_obj_start_1 #b0000000000000000000000000000000000000000000000000000000000000001))
(assert 
 (= #b1111111111111111111111111111111111111111111111111111111111111111 __ESBMC_ptr_obj_end_1))
(assert 
 (= __ESBMC_ptr_obj_end_0 |smt_conv::__ESBMC_ptr_addr_range_0..end0|))
(assert 
 (= __ESBMC_ptr_obj_start_0 |smt_conv::__ESBMC_ptr_addr_range_0..start0|))
(assert 
 (= __ESBMC_ptr_obj_end_1 |smt_conv::__ESBMC_ptr_addr_range_1..end0|))
(assert 
 (= __ESBMC_ptr_obj_start_1 |smt_conv::__ESBMC_ptr_addr_range_1..start0|))
(assert 
 (= |smt_conv::smt_conv::collate_array_vals::3..end0| |smt_conv::smt_conv::collate_array_vals::4..end0|))
(assert 
 (= |smt_conv::smt_conv::collate_array_vals::3..start0| |smt_conv::smt_conv::collate_array_vals::4..start0|))
(assert 
 (= __ESBMC_ptr_obj_end_0 |smt_conv::smt_conv::collate_array_vals::7..end0|))
(assert 
 (= __ESBMC_ptr_obj_start_0 |smt_conv::smt_conv::collate_array_vals::7..start0|))
(assert 
 (= |c:@u&0#11| |nondet$symex::nondet8|))
(assert (distinct 
 (bvnot 
  (bvand 
   (bvnot 
    ((_ extract 80007 80007) |c:@u&0#11|)) 
   (ite 
    (= 
     ((_ extract 80007 80000) |c:@u&0#11|) #b00000011) #b1 #b0))) #b0))
(assert (distinct |execution_statet::\guard_exec?0!0| #b0))
(check-sat)
(exit)