; SMT 2
(set-info :source "Generated by CBMC 5.6")
(set-option :produce-models true)
(set-logic QF_AUFBV)

; set_to true (equal)
(define-fun |__CPROVER_dead_object#1| () (_ BitVec 64) (_ bv0 64))

; set_to true (equal)
(define-fun |__CPROVER_deallocated#1| () (_ BitVec 64) (_ bv0 64))

; set_to true (equal)
(define-fun |__CPROVER_malloc_is_new_array#1| () Bool false)

; set_to true (equal)
(define-fun |__CPROVER_malloc_object#1| () (_ BitVec 64) (_ bv0 64))

; set_to true (equal)
(define-fun |__CPROVER_malloc_size#1| () (_ BitVec 64) (_ bv0 64))

; set_to true (equal)
(define-fun |__CPROVER_memory_leak#1| () (_ BitVec 64) (_ bv0 64))

; set_to true (equal)
(define-fun |__CPROVER_next_thread_id#1| () (_ BitVec 64) (_ bv0 64))

; set_to true (equal)
(define-fun |__CPROVER_pipe_count#1| () (_ BitVec 32) (_ bv0 32))

; set_to true (equal)
(define-fun |__CPROVER_rounding_mode!0#1| () (_ BitVec 32) (_ bv0 32))

; set_to true (equal)
(define-fun |__CPROVER_thread_id!0#1| () (_ BitVec 64) (_ bv0 64))

; the following is a substitute for lambda i. x
(declare-fun array_of.0 () (Array (_ BitVec 64) (_ BitVec 1)))
; set_to true (equal)
(define-fun |__CPROVER_threads_exited#1| () (Array (_ BitVec 64) (_ BitVec 1)) array_of.0)

; find_symbols
(declare-fun |main::1::r!0@1#1| () (_ BitVec 8))
; find_symbols
(declare-fun |main::1::a!0@1#1| () (_ BitVec 8))
; set_to true (equal)
(define-fun |main::1::r!0@1#2| () (_ BitVec 8) (let ((?withop |main::1::r!0@1#1|)) ?withop))

; convert
(define-fun |B0| () Bool (= |main::1::a!0@1#1| |main::1::a!0@1#1|))

; convert
(define-fun |B1| () Bool (= |main::1::r!0@1#1| |main::1::r!0@1#1|))

; set_to false
(assert (not (= ((_ extract 7 0) |main::1::r!0@1#2|) |main::1::a!0@1#1|)))

(check-sat)

(get-value (|B0|))
(get-value (|B1|))
(get-value (|__CPROVER_dead_object#1|))
(get-value (|__CPROVER_deallocated#1|))
(get-value (|__CPROVER_malloc_is_new_array#1|))
(get-value (|__CPROVER_malloc_object#1|))
(get-value (|__CPROVER_malloc_size#1|))
(get-value (|__CPROVER_memory_leak#1|))
(get-value (|__CPROVER_next_thread_id#1|))
(get-value (|__CPROVER_pipe_count#1|))
(get-value (|__CPROVER_rounding_mode!0#1|))
(get-value (|__CPROVER_thread_id!0#1|))
(get-value (|__CPROVER_threads_exited#1|))
(get-value (|main::1::a!0@1#1|))
(get-value (|main::1::r!0@1#1|))
(get-value (|main::1::r!0@1#2|))

(exit)
; end of SMT2 file