; find_symbols
(declare-fun |main::1::circle!0@1#1| () (_ BitVec 32))
; set_to true
(assert (= |goto_symex::&92;guard#1| (not (= (bvadd |main::1::circle!0@1#1| |main::1::circle!0@1#1|) (_ bv10 32)))))

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

; find_symbols
(declare-fun |main::1::square!0@1#1| () (_ BitVec 32))
; set_to true
(assert (= |goto_symex::&92;guard#2| (not (= (bvadd (bvmul |main::1::circle!0@1#1| |main::1::square!0@1#1|) |main::1::square!0@1#1|) (_ bv12 32)))))

; set_to true (equal)
(define-fun |main#return_value!0#2| () (_ BitVec 32) (_ bv0 32))

; find_symbols
(declare-fun |main::1::triangle!0@1#1| () (_ BitVec 32))
; set_to true
(assert (= |goto_symex::&92;guard#3| (not (= (bvadd (bvmul |main::1::circle!0@1#1| |main::1::square!0@1#1|) (bvneg (bvmul |main::1::circle!0@1#1| |main::1::triangle!0@1#1|))) |main::1::circle!0@1#1|))))

; set_to true (equal)
(define-fun |main#return_value!0#3| () (_ BitVec 32) (_ bv0 32))

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

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

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

; convert
(define-fun |B12| () Bool (= (bvadd |main::1::circle!0@1#1| |main::1::circle!0@1#1|) (_ bv10 32)))

; convert
(define-fun |B13| () Bool (= (bvadd (bvmul |main::1::circle!0@1#1| |main::1::square!0@1#1|) |main::1::square!0@1#1|) (_ bv12 32)))

; convert
(define-fun |B14| () Bool (= (bvadd (bvmul |main::1::circle!0@1#1| |main::1::square!0@1#1|) (bvneg (bvmul |main::1::circle!0@1#1| |main::1::triangle!0@1#1|))) |main::1::circle!0@1#1|))