;;Initial declarations
(declare-const two-to-p Real)
(assert (= two-to-p 8388608.0))

(declare-const a1 Real)
(declare-const abs-a1 Real)
(declare-const two-to-exp-a1 Real)
(declare-const two-to-exp-p-minus-e-a1 Real)
(assert (=> (>= a1 0.0) (= abs-a1 a1)));added
(assert (=> (< a1 0.0) (= abs-a1 (- a1))));added
(assert (or (and (<= 1.0  a1) (< a1 1073741824.0)) (and (>= -1.0  a1) (> a1 -1073741824.0))))

(assert (=> (and (<= 1.0 abs-a1) (< abs-a1 2.0)) (and (= two-to-exp-a1 1.0) (= two-to-exp-p-minus-e-a1 8388608.0))))
(assert (=> (and (<= 2.0 abs-a1) (< abs-a1 4.0)) (and (= two-to-exp-a1 2.0) (= two-to-exp-p-minus-e-a1 4194304.0))))
(assert (=> (and (<= 4.0 abs-a1) (< abs-a1 8.0)) (and (= two-to-exp-a1 4.0) (= two-to-exp-p-minus-e-a1 2097152.0))))
(assert (=> (and (<= 8.0 abs-a1) (< abs-a1 16.0)) (and (= two-to-exp-a1 8.0) (= two-to-exp-p-minus-e-a1 1048576.0))))
(assert (=> (and (<= 16.0 abs-a1) (< abs-a1 32.0)) (and (= two-to-exp-a1 16.0) (= two-to-exp-p-minus-e-a1 524288.0))))
(assert (=> (and (<= 32.0 abs-a1) (< abs-a1 64.0)) (and (= two-to-exp-a1 32.0) (= two-to-exp-p-minus-e-a1 262144.0))))
(assert (=> (and (<= 64.0 abs-a1) (< abs-a1 128.0)) (and (= two-to-exp-a1 64.0) (= two-to-exp-p-minus-e-a1 131072.0))))
(assert (=> (and (<= 128.0 abs-a1) (< abs-a1 256.0)) (and (= two-to-exp-a1 128.0) (= two-to-exp-p-minus-e-a1 65536.0))))
(assert (=> (and (<= 256.0 abs-a1) (< abs-a1 512.0)) (and (= two-to-exp-a1 256.0) (= two-to-exp-p-minus-e-a1 32768.0))))
(assert (=> (and (<= 512.0 abs-a1) (< abs-a1 1024.0)) (and (= two-to-exp-a1 512.0) (= two-to-exp-p-minus-e-a1 16384.0))))
(assert (=> (and (<= 1024.0 abs-a1) (< abs-a1 2048.0)) (and (= two-to-exp-a1 1024.0) (= two-to-exp-p-minus-e-a1 8192.0))))
(assert (=> (and (<= 2048.0 abs-a1) (< abs-a1 4096.0)) (and (= two-to-exp-a1 2048.0) (= two-to-exp-p-minus-e-a1 4096.0))))
(assert (=> (and (<= 4096.0 abs-a1) (< abs-a1 8192.0)) (and (= two-to-exp-a1 4096.0) (= two-to-exp-p-minus-e-a1 2048.0))))
(assert (=> (and (<= 8192.0 abs-a1) (< abs-a1 16384.0)) (and (= two-to-exp-a1 8192.0) (= two-to-exp-p-minus-e-a1 1024.0))))
(assert (=> (and (<= 16384.0 abs-a1) (< abs-a1 32768.0)) (and (= two-to-exp-a1 16384.0) (= two-to-exp-p-minus-e-a1 512.0))))
(assert (=> (and (<= 32768.0 abs-a1) (< abs-a1 65536.0)) (and (= two-to-exp-a1 32768.0) (= two-to-exp-p-minus-e-a1 256.0))))
(assert (=> (and (<= 65536.0 abs-a1) (< abs-a1 131072.0)) (and (= two-to-exp-a1 65536.0) (= two-to-exp-p-minus-e-a1 128.0))))
(assert (=> (and (<= 131072.0 abs-a1) (< abs-a1 262144.0)) (and (= two-to-exp-a1 131072.0) (= two-to-exp-p-minus-e-a1 64.0))))
(assert (=> (and (<= 262144.0 abs-a1) (< abs-a1 524288.0)) (and (= two-to-exp-a1 262144.0) (= two-to-exp-p-minus-e-a1 32.0))))
(assert (=> (and (<= 524288.0 abs-a1) (< abs-a1 1048576.0)) (and (= two-to-exp-a1 524288.0) (= two-to-exp-p-minus-e-a1 16.0))))
(assert (=> (and (<= 1048576.0 abs-a1) (< abs-a1 2097152.0)) (and (= two-to-exp-a1 1048576.0) (= two-to-exp-p-minus-e-a1 8.0))))
(assert (=> (and (<= 2097152.0 abs-a1) (< abs-a1 4194304.0)) (and (= two-to-exp-a1 2097152.0) (= two-to-exp-p-minus-e-a1 4.0))))
(assert (=> (and (<= 4194304.0 abs-a1) (< abs-a1 8388608.0)) (and (= two-to-exp-a1 4194304.0) (= two-to-exp-p-minus-e-a1 2.0))))
(assert (=> (and (<= 8388608.0 abs-a1) (< abs-a1 16777216.0)) (and (= two-to-exp-a1 8388608.0) (= two-to-exp-p-minus-e-a1 1.0))))
(assert (=> (and (<= 16777216.0 abs-a1) (< abs-a1 33554432.0)) (and (= two-to-exp-a1 16777216.0) (= two-to-exp-p-minus-e-a1 0.5))))
(assert (=> (and (<= 33554432.0 abs-a1) (< abs-a1 67108864.0)) (and (= two-to-exp-a1 33554432.0) (= two-to-exp-p-minus-e-a1 0.25))))
(assert (=> (and (<= 67108864.0 abs-a1) (< abs-a1 134217728.0)) (and (= two-to-exp-a1 67108864.0) (= two-to-exp-p-minus-e-a1 0.125))))
(assert (=> (and (<= 134217728.0 abs-a1) (< abs-a1 268435456.0)) (and (= two-to-exp-a1 134217728.0) (= two-to-exp-p-minus-e-a1 0.0625))))
(assert (=> (and (<= 268435456.0 abs-a1) (< abs-a1 536870912.0)) (and (= two-to-exp-a1 268435456.0) (= two-to-exp-p-minus-e-a1 0.03125))))
(assert (=> (and (<= 536870912.0 abs-a1) (< abs-a1 1073741824.0)) (and (= two-to-exp-a1 536870912.0) (= two-to-exp-p-minus-e-a1 0.015625))))

(declare-const temp-a1 Real)
(assert (= temp-a1 (* a1 two-to-exp-p-minus-e-a1)))
(assert (= temp-a1 (to_real (to_int temp-a1))))
(declare-const a2 Real)
(declare-const abs-a2 Real)
(declare-const two-to-exp-a2 Real)
(declare-const two-to-exp-p-minus-e-a2 Real)
(assert (=> (>= a2 0.0) (= abs-a2 a2)));added
(assert (=> (< a2 0.0) (= abs-a2 (- a2))));added
(assert (or (and (<= 1.0  a2) (< a2 1073741824.0)) (and (>= -1.0  a2) (> a2 -1073741824.0))))

(assert (=> (and (<= 1.0 abs-a2) (< abs-a2 2.0)) (and (= two-to-exp-a2 1.0) (= two-to-exp-p-minus-e-a2 8388608.0))))
(assert (=> (and (<= 2.0 abs-a2) (< abs-a2 4.0)) (and (= two-to-exp-a2 2.0) (= two-to-exp-p-minus-e-a2 4194304.0))))
(assert (=> (and (<= 4.0 abs-a2) (< abs-a2 8.0)) (and (= two-to-exp-a2 4.0) (= two-to-exp-p-minus-e-a2 2097152.0))))
(assert (=> (and (<= 8.0 abs-a2) (< abs-a2 16.0)) (and (= two-to-exp-a2 8.0) (= two-to-exp-p-minus-e-a2 1048576.0))))
(assert (=> (and (<= 16.0 abs-a2) (< abs-a2 32.0)) (and (= two-to-exp-a2 16.0) (= two-to-exp-p-minus-e-a2 524288.0))))
(assert (=> (and (<= 32.0 abs-a2) (< abs-a2 64.0)) (and (= two-to-exp-a2 32.0) (= two-to-exp-p-minus-e-a2 262144.0))))
(assert (=> (and (<= 64.0 abs-a2) (< abs-a2 128.0)) (and (= two-to-exp-a2 64.0) (= two-to-exp-p-minus-e-a2 131072.0))))
(assert (=> (and (<= 128.0 abs-a2) (< abs-a2 256.0)) (and (= two-to-exp-a2 128.0) (= two-to-exp-p-minus-e-a2 65536.0))))
(assert (=> (and (<= 256.0 abs-a2) (< abs-a2 512.0)) (and (= two-to-exp-a2 256.0) (= two-to-exp-p-minus-e-a2 32768.0))))
(assert (=> (and (<= 512.0 abs-a2) (< abs-a2 1024.0)) (and (= two-to-exp-a2 512.0) (= two-to-exp-p-minus-e-a2 16384.0))))
(assert (=> (and (<= 1024.0 abs-a2) (< abs-a2 2048.0)) (and (= two-to-exp-a2 1024.0) (= two-to-exp-p-minus-e-a2 8192.0))))
(assert (=> (and (<= 2048.0 abs-a2) (< abs-a2 4096.0)) (and (= two-to-exp-a2 2048.0) (= two-to-exp-p-minus-e-a2 4096.0))))
(assert (=> (and (<= 4096.0 abs-a2) (< abs-a2 8192.0)) (and (= two-to-exp-a2 4096.0) (= two-to-exp-p-minus-e-a2 2048.0))))
(assert (=> (and (<= 8192.0 abs-a2) (< abs-a2 16384.0)) (and (= two-to-exp-a2 8192.0) (= two-to-exp-p-minus-e-a2 1024.0))))
(assert (=> (and (<= 16384.0 abs-a2) (< abs-a2 32768.0)) (and (= two-to-exp-a2 16384.0) (= two-to-exp-p-minus-e-a2 512.0))))
(assert (=> (and (<= 32768.0 abs-a2) (< abs-a2 65536.0)) (and (= two-to-exp-a2 32768.0) (= two-to-exp-p-minus-e-a2 256.0))))
(assert (=> (and (<= 65536.0 abs-a2) (< abs-a2 131072.0)) (and (= two-to-exp-a2 65536.0) (= two-to-exp-p-minus-e-a2 128.0))))
(assert (=> (and (<= 131072.0 abs-a2) (< abs-a2 262144.0)) (and (= two-to-exp-a2 131072.0) (= two-to-exp-p-minus-e-a2 64.0))))
(assert (=> (and (<= 262144.0 abs-a2) (< abs-a2 524288.0)) (and (= two-to-exp-a2 262144.0) (= two-to-exp-p-minus-e-a2 32.0))))
(assert (=> (and (<= 524288.0 abs-a2) (< abs-a2 1048576.0)) (and (= two-to-exp-a2 524288.0) (= two-to-exp-p-minus-e-a2 16.0))))
(assert (=> (and (<= 1048576.0 abs-a2) (< abs-a2 2097152.0)) (and (= two-to-exp-a2 1048576.0) (= two-to-exp-p-minus-e-a2 8.0))))
(assert (=> (and (<= 2097152.0 abs-a2) (< abs-a2 4194304.0)) (and (= two-to-exp-a2 2097152.0) (= two-to-exp-p-minus-e-a2 4.0))))
(assert (=> (and (<= 4194304.0 abs-a2) (< abs-a2 8388608.0)) (and (= two-to-exp-a2 4194304.0) (= two-to-exp-p-minus-e-a2 2.0))))
(assert (=> (and (<= 8388608.0 abs-a2) (< abs-a2 16777216.0)) (and (= two-to-exp-a2 8388608.0) (= two-to-exp-p-minus-e-a2 1.0))))
(assert (=> (and (<= 16777216.0 abs-a2) (< abs-a2 33554432.0)) (and (= two-to-exp-a2 16777216.0) (= two-to-exp-p-minus-e-a2 0.5))))
(assert (=> (and (<= 33554432.0 abs-a2) (< abs-a2 67108864.0)) (and (= two-to-exp-a2 33554432.0) (= two-to-exp-p-minus-e-a2 0.25))))
(assert (=> (and (<= 67108864.0 abs-a2) (< abs-a2 134217728.0)) (and (= two-to-exp-a2 67108864.0) (= two-to-exp-p-minus-e-a2 0.125))))
(assert (=> (and (<= 134217728.0 abs-a2) (< abs-a2 268435456.0)) (and (= two-to-exp-a2 134217728.0) (= two-to-exp-p-minus-e-a2 0.0625))))
(assert (=> (and (<= 268435456.0 abs-a2) (< abs-a2 536870912.0)) (and (= two-to-exp-a2 268435456.0) (= two-to-exp-p-minus-e-a2 0.03125))))
(assert (=> (and (<= 536870912.0 abs-a2) (< abs-a2 1073741824.0)) (and (= two-to-exp-a2 536870912.0) (= two-to-exp-p-minus-e-a2 0.015625))))

(declare-const temp-a2 Real)
(assert (= temp-a2 (* a2 two-to-exp-p-minus-e-a2)))
(assert (= temp-a2 (to_real (to_int temp-a2))))
(declare-const a3 Real)
(declare-const abs-a3 Real)
(declare-const two-to-exp-a3 Real)
(declare-const two-to-exp-p-minus-e-a3 Real)
(assert (=> (>= a3 0.0) (= abs-a3 a3)));added
(assert (=> (< a3 0.0) (= abs-a3 (- a3))));added
(assert (or (and (<= 1.0  a3) (< a3 1073741824.0)) (and (>= -1.0  a3) (> a3 -1073741824.0))))

(assert (=> (and (<= 1.0 abs-a3) (< abs-a3 2.0)) (and (= two-to-exp-a3 1.0) (= two-to-exp-p-minus-e-a3 8388608.0))))
(assert (=> (and (<= 2.0 abs-a3) (< abs-a3 4.0)) (and (= two-to-exp-a3 2.0) (= two-to-exp-p-minus-e-a3 4194304.0))))
(assert (=> (and (<= 4.0 abs-a3) (< abs-a3 8.0)) (and (= two-to-exp-a3 4.0) (= two-to-exp-p-minus-e-a3 2097152.0))))
(assert (=> (and (<= 8.0 abs-a3) (< abs-a3 16.0)) (and (= two-to-exp-a3 8.0) (= two-to-exp-p-minus-e-a3 1048576.0))))
(assert (=> (and (<= 16.0 abs-a3) (< abs-a3 32.0)) (and (= two-to-exp-a3 16.0) (= two-to-exp-p-minus-e-a3 524288.0))))
(assert (=> (and (<= 32.0 abs-a3) (< abs-a3 64.0)) (and (= two-to-exp-a3 32.0) (= two-to-exp-p-minus-e-a3 262144.0))))
(assert (=> (and (<= 64.0 abs-a3) (< abs-a3 128.0)) (and (= two-to-exp-a3 64.0) (= two-to-exp-p-minus-e-a3 131072.0))))
(assert (=> (and (<= 128.0 abs-a3) (< abs-a3 256.0)) (and (= two-to-exp-a3 128.0) (= two-to-exp-p-minus-e-a3 65536.0))))
(assert (=> (and (<= 256.0 abs-a3) (< abs-a3 512.0)) (and (= two-to-exp-a3 256.0) (= two-to-exp-p-minus-e-a3 32768.0))))
(assert (=> (and (<= 512.0 abs-a3) (< abs-a3 1024.0)) (and (= two-to-exp-a3 512.0) (= two-to-exp-p-minus-e-a3 16384.0))))
(assert (=> (and (<= 1024.0 abs-a3) (< abs-a3 2048.0)) (and (= two-to-exp-a3 1024.0) (= two-to-exp-p-minus-e-a3 8192.0))))
(assert (=> (and (<= 2048.0 abs-a3) (< abs-a3 4096.0)) (and (= two-to-exp-a3 2048.0) (= two-to-exp-p-minus-e-a3 4096.0))))
(assert (=> (and (<= 4096.0 abs-a3) (< abs-a3 8192.0)) (and (= two-to-exp-a3 4096.0) (= two-to-exp-p-minus-e-a3 2048.0))))
(assert (=> (and (<= 8192.0 abs-a3) (< abs-a3 16384.0)) (and (= two-to-exp-a3 8192.0) (= two-to-exp-p-minus-e-a3 1024.0))))
(assert (=> (and (<= 16384.0 abs-a3) (< abs-a3 32768.0)) (and (= two-to-exp-a3 16384.0) (= two-to-exp-p-minus-e-a3 512.0))))
(assert (=> (and (<= 32768.0 abs-a3) (< abs-a3 65536.0)) (and (= two-to-exp-a3 32768.0) (= two-to-exp-p-minus-e-a3 256.0))))
(assert (=> (and (<= 65536.0 abs-a3) (< abs-a3 131072.0)) (and (= two-to-exp-a3 65536.0) (= two-to-exp-p-minus-e-a3 128.0))))
(assert (=> (and (<= 131072.0 abs-a3) (< abs-a3 262144.0)) (and (= two-to-exp-a3 131072.0) (= two-to-exp-p-minus-e-a3 64.0))))
(assert (=> (and (<= 262144.0 abs-a3) (< abs-a3 524288.0)) (and (= two-to-exp-a3 262144.0) (= two-to-exp-p-minus-e-a3 32.0))))
(assert (=> (and (<= 524288.0 abs-a3) (< abs-a3 1048576.0)) (and (= two-to-exp-a3 524288.0) (= two-to-exp-p-minus-e-a3 16.0))))
(assert (=> (and (<= 1048576.0 abs-a3) (< abs-a3 2097152.0)) (and (= two-to-exp-a3 1048576.0) (= two-to-exp-p-minus-e-a3 8.0))))
(assert (=> (and (<= 2097152.0 abs-a3) (< abs-a3 4194304.0)) (and (= two-to-exp-a3 2097152.0) (= two-to-exp-p-minus-e-a3 4.0))))
(assert (=> (and (<= 4194304.0 abs-a3) (< abs-a3 8388608.0)) (and (= two-to-exp-a3 4194304.0) (= two-to-exp-p-minus-e-a3 2.0))))
(assert (=> (and (<= 8388608.0 abs-a3) (< abs-a3 16777216.0)) (and (= two-to-exp-a3 8388608.0) (= two-to-exp-p-minus-e-a3 1.0))))
(assert (=> (and (<= 16777216.0 abs-a3) (< abs-a3 33554432.0)) (and (= two-to-exp-a3 16777216.0) (= two-to-exp-p-minus-e-a3 0.5))))
(assert (=> (and (<= 33554432.0 abs-a3) (< abs-a3 67108864.0)) (and (= two-to-exp-a3 33554432.0) (= two-to-exp-p-minus-e-a3 0.25))))
(assert (=> (and (<= 67108864.0 abs-a3) (< abs-a3 134217728.0)) (and (= two-to-exp-a3 67108864.0) (= two-to-exp-p-minus-e-a3 0.125))))
(assert (=> (and (<= 134217728.0 abs-a3) (< abs-a3 268435456.0)) (and (= two-to-exp-a3 134217728.0) (= two-to-exp-p-minus-e-a3 0.0625))))
(assert (=> (and (<= 268435456.0 abs-a3) (< abs-a3 536870912.0)) (and (= two-to-exp-a3 268435456.0) (= two-to-exp-p-minus-e-a3 0.03125))))
(assert (=> (and (<= 536870912.0 abs-a3) (< abs-a3 1073741824.0)) (and (= two-to-exp-a3 536870912.0) (= two-to-exp-p-minus-e-a3 0.015625))))

(declare-const temp-a3 Real)
(assert (= temp-a3 (* a3 two-to-exp-p-minus-e-a3)))
(assert (= temp-a3 (to_real (to_int temp-a3))))
(declare-const a4 Real)
(declare-const abs-a4 Real)
(declare-const two-to-exp-a4 Real)
(declare-const two-to-exp-p-minus-e-a4 Real)
(assert (=> (>= a4 0.0) (= abs-a4 a4)));added
(assert (=> (< a4 0.0) (= abs-a4 (- a4))));added
(assert (or (and (<= 1.0  a4) (< a4 1073741824.0)) (and (>= -1.0  a4) (> a4 -1073741824.0))))

(assert (=> (and (<= 1.0 abs-a4) (< abs-a4 2.0)) (and (= two-to-exp-a4 1.0) (= two-to-exp-p-minus-e-a4 8388608.0))))
(assert (=> (and (<= 2.0 abs-a4) (< abs-a4 4.0)) (and (= two-to-exp-a4 2.0) (= two-to-exp-p-minus-e-a4 4194304.0))))
(assert (=> (and (<= 4.0 abs-a4) (< abs-a4 8.0)) (and (= two-to-exp-a4 4.0) (= two-to-exp-p-minus-e-a4 2097152.0))))
(assert (=> (and (<= 8.0 abs-a4) (< abs-a4 16.0)) (and (= two-to-exp-a4 8.0) (= two-to-exp-p-minus-e-a4 1048576.0))))
(assert (=> (and (<= 16.0 abs-a4) (< abs-a4 32.0)) (and (= two-to-exp-a4 16.0) (= two-to-exp-p-minus-e-a4 524288.0))))
(assert (=> (and (<= 32.0 abs-a4) (< abs-a4 64.0)) (and (= two-to-exp-a4 32.0) (= two-to-exp-p-minus-e-a4 262144.0))))
(assert (=> (and (<= 64.0 abs-a4) (< abs-a4 128.0)) (and (= two-to-exp-a4 64.0) (= two-to-exp-p-minus-e-a4 131072.0))))
(assert (=> (and (<= 128.0 abs-a4) (< abs-a4 256.0)) (and (= two-to-exp-a4 128.0) (= two-to-exp-p-minus-e-a4 65536.0))))
(assert (=> (and (<= 256.0 abs-a4) (< abs-a4 512.0)) (and (= two-to-exp-a4 256.0) (= two-to-exp-p-minus-e-a4 32768.0))))
(assert (=> (and (<= 512.0 abs-a4) (< abs-a4 1024.0)) (and (= two-to-exp-a4 512.0) (= two-to-exp-p-minus-e-a4 16384.0))))
(assert (=> (and (<= 1024.0 abs-a4) (< abs-a4 2048.0)) (and (= two-to-exp-a4 1024.0) (= two-to-exp-p-minus-e-a4 8192.0))))
(assert (=> (and (<= 2048.0 abs-a4) (< abs-a4 4096.0)) (and (= two-to-exp-a4 2048.0) (= two-to-exp-p-minus-e-a4 4096.0))))
(assert (=> (and (<= 4096.0 abs-a4) (< abs-a4 8192.0)) (and (= two-to-exp-a4 4096.0) (= two-to-exp-p-minus-e-a4 2048.0))))
(assert (=> (and (<= 8192.0 abs-a4) (< abs-a4 16384.0)) (and (= two-to-exp-a4 8192.0) (= two-to-exp-p-minus-e-a4 1024.0))))
(assert (=> (and (<= 16384.0 abs-a4) (< abs-a4 32768.0)) (and (= two-to-exp-a4 16384.0) (= two-to-exp-p-minus-e-a4 512.0))))
(assert (=> (and (<= 32768.0 abs-a4) (< abs-a4 65536.0)) (and (= two-to-exp-a4 32768.0) (= two-to-exp-p-minus-e-a4 256.0))))
(assert (=> (and (<= 65536.0 abs-a4) (< abs-a4 131072.0)) (and (= two-to-exp-a4 65536.0) (= two-to-exp-p-minus-e-a4 128.0))))
(assert (=> (and (<= 131072.0 abs-a4) (< abs-a4 262144.0)) (and (= two-to-exp-a4 131072.0) (= two-to-exp-p-minus-e-a4 64.0))))
(assert (=> (and (<= 262144.0 abs-a4) (< abs-a4 524288.0)) (and (= two-to-exp-a4 262144.0) (= two-to-exp-p-minus-e-a4 32.0))))
(assert (=> (and (<= 524288.0 abs-a4) (< abs-a4 1048576.0)) (and (= two-to-exp-a4 524288.0) (= two-to-exp-p-minus-e-a4 16.0))))
(assert (=> (and (<= 1048576.0 abs-a4) (< abs-a4 2097152.0)) (and (= two-to-exp-a4 1048576.0) (= two-to-exp-p-minus-e-a4 8.0))))
(assert (=> (and (<= 2097152.0 abs-a4) (< abs-a4 4194304.0)) (and (= two-to-exp-a4 2097152.0) (= two-to-exp-p-minus-e-a4 4.0))))
(assert (=> (and (<= 4194304.0 abs-a4) (< abs-a4 8388608.0)) (and (= two-to-exp-a4 4194304.0) (= two-to-exp-p-minus-e-a4 2.0))))
(assert (=> (and (<= 8388608.0 abs-a4) (< abs-a4 16777216.0)) (and (= two-to-exp-a4 8388608.0) (= two-to-exp-p-minus-e-a4 1.0))))
(assert (=> (and (<= 16777216.0 abs-a4) (< abs-a4 33554432.0)) (and (= two-to-exp-a4 16777216.0) (= two-to-exp-p-minus-e-a4 0.5))))
(assert (=> (and (<= 33554432.0 abs-a4) (< abs-a4 67108864.0)) (and (= two-to-exp-a4 33554432.0) (= two-to-exp-p-minus-e-a4 0.25))))
(assert (=> (and (<= 67108864.0 abs-a4) (< abs-a4 134217728.0)) (and (= two-to-exp-a4 67108864.0) (= two-to-exp-p-minus-e-a4 0.125))))
(assert (=> (and (<= 134217728.0 abs-a4) (< abs-a4 268435456.0)) (and (= two-to-exp-a4 134217728.0) (= two-to-exp-p-minus-e-a4 0.0625))))
(assert (=> (and (<= 268435456.0 abs-a4) (< abs-a4 536870912.0)) (and (= two-to-exp-a4 268435456.0) (= two-to-exp-p-minus-e-a4 0.03125))))
(assert (=> (and (<= 536870912.0 abs-a4) (< abs-a4 1073741824.0)) (and (= two-to-exp-a4 536870912.0) (= two-to-exp-p-minus-e-a4 0.015625))))

(declare-const temp-a4 Real)
(assert (= temp-a4 (* a4 two-to-exp-p-minus-e-a4)))
(assert (= temp-a4 (to_real (to_int temp-a4))))
(declare-const a5 Real)
(declare-const abs-a5 Real)
(declare-const two-to-exp-a5 Real)
(declare-const two-to-exp-p-minus-e-a5 Real)
(assert (=> (>= a5 0.0) (= abs-a5 a5)));added
(assert (=> (< a5 0.0) (= abs-a5 (- a5))));added
(assert (or (and (<= 1.0  a5) (< a5 1073741824.0)) (and (>= -1.0  a5) (> a5 -1073741824.0))))

(assert (=> (and (<= 1.0 abs-a5) (< abs-a5 2.0)) (and (= two-to-exp-a5 1.0) (= two-to-exp-p-minus-e-a5 8388608.0))))
(assert (=> (and (<= 2.0 abs-a5) (< abs-a5 4.0)) (and (= two-to-exp-a5 2.0) (= two-to-exp-p-minus-e-a5 4194304.0))))
(assert (=> (and (<= 4.0 abs-a5) (< abs-a5 8.0)) (and (= two-to-exp-a5 4.0) (= two-to-exp-p-minus-e-a5 2097152.0))))
(assert (=> (and (<= 8.0 abs-a5) (< abs-a5 16.0)) (and (= two-to-exp-a5 8.0) (= two-to-exp-p-minus-e-a5 1048576.0))))
(assert (=> (and (<= 16.0 abs-a5) (< abs-a5 32.0)) (and (= two-to-exp-a5 16.0) (= two-to-exp-p-minus-e-a5 524288.0))))
(assert (=> (and (<= 32.0 abs-a5) (< abs-a5 64.0)) (and (= two-to-exp-a5 32.0) (= two-to-exp-p-minus-e-a5 262144.0))))
(assert (=> (and (<= 64.0 abs-a5) (< abs-a5 128.0)) (and (= two-to-exp-a5 64.0) (= two-to-exp-p-minus-e-a5 131072.0))))
(assert (=> (and (<= 128.0 abs-a5) (< abs-a5 256.0)) (and (= two-to-exp-a5 128.0) (= two-to-exp-p-minus-e-a5 65536.0))))
(assert (=> (and (<= 256.0 abs-a5) (< abs-a5 512.0)) (and (= two-to-exp-a5 256.0) (= two-to-exp-p-minus-e-a5 32768.0))))
(assert (=> (and (<= 512.0 abs-a5) (< abs-a5 1024.0)) (and (= two-to-exp-a5 512.0) (= two-to-exp-p-minus-e-a5 16384.0))))
(assert (=> (and (<= 1024.0 abs-a5) (< abs-a5 2048.0)) (and (= two-to-exp-a5 1024.0) (= two-to-exp-p-minus-e-a5 8192.0))))
(assert (=> (and (<= 2048.0 abs-a5) (< abs-a5 4096.0)) (and (= two-to-exp-a5 2048.0) (= two-to-exp-p-minus-e-a5 4096.0))))
(assert (=> (and (<= 4096.0 abs-a5) (< abs-a5 8192.0)) (and (= two-to-exp-a5 4096.0) (= two-to-exp-p-minus-e-a5 2048.0))))
(assert (=> (and (<= 8192.0 abs-a5) (< abs-a5 16384.0)) (and (= two-to-exp-a5 8192.0) (= two-to-exp-p-minus-e-a5 1024.0))))
(assert (=> (and (<= 16384.0 abs-a5) (< abs-a5 32768.0)) (and (= two-to-exp-a5 16384.0) (= two-to-exp-p-minus-e-a5 512.0))))
(assert (=> (and (<= 32768.0 abs-a5) (< abs-a5 65536.0)) (and (= two-to-exp-a5 32768.0) (= two-to-exp-p-minus-e-a5 256.0))))
(assert (=> (and (<= 65536.0 abs-a5) (< abs-a5 131072.0)) (and (= two-to-exp-a5 65536.0) (= two-to-exp-p-minus-e-a5 128.0))))
(assert (=> (and (<= 131072.0 abs-a5) (< abs-a5 262144.0)) (and (= two-to-exp-a5 131072.0) (= two-to-exp-p-minus-e-a5 64.0))))
(assert (=> (and (<= 262144.0 abs-a5) (< abs-a5 524288.0)) (and (= two-to-exp-a5 262144.0) (= two-to-exp-p-minus-e-a5 32.0))))
(assert (=> (and (<= 524288.0 abs-a5) (< abs-a5 1048576.0)) (and (= two-to-exp-a5 524288.0) (= two-to-exp-p-minus-e-a5 16.0))))
(assert (=> (and (<= 1048576.0 abs-a5) (< abs-a5 2097152.0)) (and (= two-to-exp-a5 1048576.0) (= two-to-exp-p-minus-e-a5 8.0))))
(assert (=> (and (<= 2097152.0 abs-a5) (< abs-a5 4194304.0)) (and (= two-to-exp-a5 2097152.0) (= two-to-exp-p-minus-e-a5 4.0))))
(assert (=> (and (<= 4194304.0 abs-a5) (< abs-a5 8388608.0)) (and (= two-to-exp-a5 4194304.0) (= two-to-exp-p-minus-e-a5 2.0))))
(assert (=> (and (<= 8388608.0 abs-a5) (< abs-a5 16777216.0)) (and (= two-to-exp-a5 8388608.0) (= two-to-exp-p-minus-e-a5 1.0))))
(assert (=> (and (<= 16777216.0 abs-a5) (< abs-a5 33554432.0)) (and (= two-to-exp-a5 16777216.0) (= two-to-exp-p-minus-e-a5 0.5))))
(assert (=> (and (<= 33554432.0 abs-a5) (< abs-a5 67108864.0)) (and (= two-to-exp-a5 33554432.0) (= two-to-exp-p-minus-e-a5 0.25))))
(assert (=> (and (<= 67108864.0 abs-a5) (< abs-a5 134217728.0)) (and (= two-to-exp-a5 67108864.0) (= two-to-exp-p-minus-e-a5 0.125))))
(assert (=> (and (<= 134217728.0 abs-a5) (< abs-a5 268435456.0)) (and (= two-to-exp-a5 134217728.0) (= two-to-exp-p-minus-e-a5 0.0625))))
(assert (=> (and (<= 268435456.0 abs-a5) (< abs-a5 536870912.0)) (and (= two-to-exp-a5 268435456.0) (= two-to-exp-p-minus-e-a5 0.03125))))
(assert (=> (and (<= 536870912.0 abs-a5) (< abs-a5 1073741824.0)) (and (= two-to-exp-a5 536870912.0) (= two-to-exp-p-minus-e-a5 0.015625))))

(declare-const temp-a5 Real)
(assert (= temp-a5 (* a5 two-to-exp-p-minus-e-a5)))
(assert (= temp-a5 (to_real (to_int temp-a5))))
(declare-const a6 Real)
(declare-const abs-a6 Real)
(declare-const two-to-exp-a6 Real)
(declare-const two-to-exp-p-minus-e-a6 Real)
(assert (=> (>= a6 0.0) (= abs-a6 a6)));added
(assert (=> (< a6 0.0) (= abs-a6 (- a6))));added
(assert (or (and (<= 1.0  a6) (< a6 1073741824.0)) (and (>= -1.0  a6) (> a6 -1073741824.0))))

(assert (=> (and (<= 1.0 abs-a6) (< abs-a6 2.0)) (and (= two-to-exp-a6 1.0) (= two-to-exp-p-minus-e-a6 8388608.0))))
(assert (=> (and (<= 2.0 abs-a6) (< abs-a6 4.0)) (and (= two-to-exp-a6 2.0) (= two-to-exp-p-minus-e-a6 4194304.0))))
(assert (=> (and (<= 4.0 abs-a6) (< abs-a6 8.0)) (and (= two-to-exp-a6 4.0) (= two-to-exp-p-minus-e-a6 2097152.0))))
(assert (=> (and (<= 8.0 abs-a6) (< abs-a6 16.0)) (and (= two-to-exp-a6 8.0) (= two-to-exp-p-minus-e-a6 1048576.0))))
(assert (=> (and (<= 16.0 abs-a6) (< abs-a6 32.0)) (and (= two-to-exp-a6 16.0) (= two-to-exp-p-minus-e-a6 524288.0))))
(assert (=> (and (<= 32.0 abs-a6) (< abs-a6 64.0)) (and (= two-to-exp-a6 32.0) (= two-to-exp-p-minus-e-a6 262144.0))))
(assert (=> (and (<= 64.0 abs-a6) (< abs-a6 128.0)) (and (= two-to-exp-a6 64.0) (= two-to-exp-p-minus-e-a6 131072.0))))
(assert (=> (and (<= 128.0 abs-a6) (< abs-a6 256.0)) (and (= two-to-exp-a6 128.0) (= two-to-exp-p-minus-e-a6 65536.0))))
(assert (=> (and (<= 256.0 abs-a6) (< abs-a6 512.0)) (and (= two-to-exp-a6 256.0) (= two-to-exp-p-minus-e-a6 32768.0))))
(assert (=> (and (<= 512.0 abs-a6) (< abs-a6 1024.0)) (and (= two-to-exp-a6 512.0) (= two-to-exp-p-minus-e-a6 16384.0))))
(assert (=> (and (<= 1024.0 abs-a6) (< abs-a6 2048.0)) (and (= two-to-exp-a6 1024.0) (= two-to-exp-p-minus-e-a6 8192.0))))
(assert (=> (and (<= 2048.0 abs-a6) (< abs-a6 4096.0)) (and (= two-to-exp-a6 2048.0) (= two-to-exp-p-minus-e-a6 4096.0))))
(assert (=> (and (<= 4096.0 abs-a6) (< abs-a6 8192.0)) (and (= two-to-exp-a6 4096.0) (= two-to-exp-p-minus-e-a6 2048.0))))
(assert (=> (and (<= 8192.0 abs-a6) (< abs-a6 16384.0)) (and (= two-to-exp-a6 8192.0) (= two-to-exp-p-minus-e-a6 1024.0))))
(assert (=> (and (<= 16384.0 abs-a6) (< abs-a6 32768.0)) (and (= two-to-exp-a6 16384.0) (= two-to-exp-p-minus-e-a6 512.0))))
(assert (=> (and (<= 32768.0 abs-a6) (< abs-a6 65536.0)) (and (= two-to-exp-a6 32768.0) (= two-to-exp-p-minus-e-a6 256.0))))
(assert (=> (and (<= 65536.0 abs-a6) (< abs-a6 131072.0)) (and (= two-to-exp-a6 65536.0) (= two-to-exp-p-minus-e-a6 128.0))))
(assert (=> (and (<= 131072.0 abs-a6) (< abs-a6 262144.0)) (and (= two-to-exp-a6 131072.0) (= two-to-exp-p-minus-e-a6 64.0))))
(assert (=> (and (<= 262144.0 abs-a6) (< abs-a6 524288.0)) (and (= two-to-exp-a6 262144.0) (= two-to-exp-p-minus-e-a6 32.0))))
(assert (=> (and (<= 524288.0 abs-a6) (< abs-a6 1048576.0)) (and (= two-to-exp-a6 524288.0) (= two-to-exp-p-minus-e-a6 16.0))))
(assert (=> (and (<= 1048576.0 abs-a6) (< abs-a6 2097152.0)) (and (= two-to-exp-a6 1048576.0) (= two-to-exp-p-minus-e-a6 8.0))))
(assert (=> (and (<= 2097152.0 abs-a6) (< abs-a6 4194304.0)) (and (= two-to-exp-a6 2097152.0) (= two-to-exp-p-minus-e-a6 4.0))))
(assert (=> (and (<= 4194304.0 abs-a6) (< abs-a6 8388608.0)) (and (= two-to-exp-a6 4194304.0) (= two-to-exp-p-minus-e-a6 2.0))))
(assert (=> (and (<= 8388608.0 abs-a6) (< abs-a6 16777216.0)) (and (= two-to-exp-a6 8388608.0) (= two-to-exp-p-minus-e-a6 1.0))))
(assert (=> (and (<= 16777216.0 abs-a6) (< abs-a6 33554432.0)) (and (= two-to-exp-a6 16777216.0) (= two-to-exp-p-minus-e-a6 0.5))))
(assert (=> (and (<= 33554432.0 abs-a6) (< abs-a6 67108864.0)) (and (= two-to-exp-a6 33554432.0) (= two-to-exp-p-minus-e-a6 0.25))))
(assert (=> (and (<= 67108864.0 abs-a6) (< abs-a6 134217728.0)) (and (= two-to-exp-a6 67108864.0) (= two-to-exp-p-minus-e-a6 0.125))))
(assert (=> (and (<= 134217728.0 abs-a6) (< abs-a6 268435456.0)) (and (= two-to-exp-a6 134217728.0) (= two-to-exp-p-minus-e-a6 0.0625))))
(assert (=> (and (<= 268435456.0 abs-a6) (< abs-a6 536870912.0)) (and (= two-to-exp-a6 268435456.0) (= two-to-exp-p-minus-e-a6 0.03125))))
(assert (=> (and (<= 536870912.0 abs-a6) (< abs-a6 1073741824.0)) (and (= two-to-exp-a6 536870912.0) (= two-to-exp-p-minus-e-a6 0.015625))))

(declare-const temp-a6 Real)
(assert (= temp-a6 (* a6 two-to-exp-p-minus-e-a6)))
(assert (= temp-a6 (to_real (to_int temp-a6))))
(declare-const a7 Real)
(declare-const abs-a7 Real)
(declare-const two-to-exp-a7 Real)
(declare-const two-to-exp-p-minus-e-a7 Real)
(assert (=> (>= a7 0.0) (= abs-a7 a7)));added
(assert (=> (< a7 0.0) (= abs-a7 (- a7))));added
(assert (or (and (<= 1.0  a7) (< a7 1073741824.0)) (and (>= -1.0  a7) (> a7 -1073741824.0))))

(assert (=> (and (<= 1.0 abs-a7) (< abs-a7 2.0)) (and (= two-to-exp-a7 1.0) (= two-to-exp-p-minus-e-a7 8388608.0))))
(assert (=> (and (<= 2.0 abs-a7) (< abs-a7 4.0)) (and (= two-to-exp-a7 2.0) (= two-to-exp-p-minus-e-a7 4194304.0))))
(assert (=> (and (<= 4.0 abs-a7) (< abs-a7 8.0)) (and (= two-to-exp-a7 4.0) (= two-to-exp-p-minus-e-a7 2097152.0))))
(assert (=> (and (<= 8.0 abs-a7) (< abs-a7 16.0)) (and (= two-to-exp-a7 8.0) (= two-to-exp-p-minus-e-a7 1048576.0))))
(assert (=> (and (<= 16.0 abs-a7) (< abs-a7 32.0)) (and (= two-to-exp-a7 16.0) (= two-to-exp-p-minus-e-a7 524288.0))))
(assert (=> (and (<= 32.0 abs-a7) (< abs-a7 64.0)) (and (= two-to-exp-a7 32.0) (= two-to-exp-p-minus-e-a7 262144.0))))
(assert (=> (and (<= 64.0 abs-a7) (< abs-a7 128.0)) (and (= two-to-exp-a7 64.0) (= two-to-exp-p-minus-e-a7 131072.0))))
(assert (=> (and (<= 128.0 abs-a7) (< abs-a7 256.0)) (and (= two-to-exp-a7 128.0) (= two-to-exp-p-minus-e-a7 65536.0))))
(assert (=> (and (<= 256.0 abs-a7) (< abs-a7 512.0)) (and (= two-to-exp-a7 256.0) (= two-to-exp-p-minus-e-a7 32768.0))))
(assert (=> (and (<= 512.0 abs-a7) (< abs-a7 1024.0)) (and (= two-to-exp-a7 512.0) (= two-to-exp-p-minus-e-a7 16384.0))))
(assert (=> (and (<= 1024.0 abs-a7) (< abs-a7 2048.0)) (and (= two-to-exp-a7 1024.0) (= two-to-exp-p-minus-e-a7 8192.0))))
(assert (=> (and (<= 2048.0 abs-a7) (< abs-a7 4096.0)) (and (= two-to-exp-a7 2048.0) (= two-to-exp-p-minus-e-a7 4096.0))))
(assert (=> (and (<= 4096.0 abs-a7) (< abs-a7 8192.0)) (and (= two-to-exp-a7 4096.0) (= two-to-exp-p-minus-e-a7 2048.0))))
(assert (=> (and (<= 8192.0 abs-a7) (< abs-a7 16384.0)) (and (= two-to-exp-a7 8192.0) (= two-to-exp-p-minus-e-a7 1024.0))))
(assert (=> (and (<= 16384.0 abs-a7) (< abs-a7 32768.0)) (and (= two-to-exp-a7 16384.0) (= two-to-exp-p-minus-e-a7 512.0))))
(assert (=> (and (<= 32768.0 abs-a7) (< abs-a7 65536.0)) (and (= two-to-exp-a7 32768.0) (= two-to-exp-p-minus-e-a7 256.0))))
(assert (=> (and (<= 65536.0 abs-a7) (< abs-a7 131072.0)) (and (= two-to-exp-a7 65536.0) (= two-to-exp-p-minus-e-a7 128.0))))
(assert (=> (and (<= 131072.0 abs-a7) (< abs-a7 262144.0)) (and (= two-to-exp-a7 131072.0) (= two-to-exp-p-minus-e-a7 64.0))))
(assert (=> (and (<= 262144.0 abs-a7) (< abs-a7 524288.0)) (and (= two-to-exp-a7 262144.0) (= two-to-exp-p-minus-e-a7 32.0))))
(assert (=> (and (<= 524288.0 abs-a7) (< abs-a7 1048576.0)) (and (= two-to-exp-a7 524288.0) (= two-to-exp-p-minus-e-a7 16.0))))
(assert (=> (and (<= 1048576.0 abs-a7) (< abs-a7 2097152.0)) (and (= two-to-exp-a7 1048576.0) (= two-to-exp-p-minus-e-a7 8.0))))
(assert (=> (and (<= 2097152.0 abs-a7) (< abs-a7 4194304.0)) (and (= two-to-exp-a7 2097152.0) (= two-to-exp-p-minus-e-a7 4.0))))
(assert (=> (and (<= 4194304.0 abs-a7) (< abs-a7 8388608.0)) (and (= two-to-exp-a7 4194304.0) (= two-to-exp-p-minus-e-a7 2.0))))
(assert (=> (and (<= 8388608.0 abs-a7) (< abs-a7 16777216.0)) (and (= two-to-exp-a7 8388608.0) (= two-to-exp-p-minus-e-a7 1.0))))
(assert (=> (and (<= 16777216.0 abs-a7) (< abs-a7 33554432.0)) (and (= two-to-exp-a7 16777216.0) (= two-to-exp-p-minus-e-a7 0.5))))
(assert (=> (and (<= 33554432.0 abs-a7) (< abs-a7 67108864.0)) (and (= two-to-exp-a7 33554432.0) (= two-to-exp-p-minus-e-a7 0.25))))
(assert (=> (and (<= 67108864.0 abs-a7) (< abs-a7 134217728.0)) (and (= two-to-exp-a7 67108864.0) (= two-to-exp-p-minus-e-a7 0.125))))
(assert (=> (and (<= 134217728.0 abs-a7) (< abs-a7 268435456.0)) (and (= two-to-exp-a7 134217728.0) (= two-to-exp-p-minus-e-a7 0.0625))))
(assert (=> (and (<= 268435456.0 abs-a7) (< abs-a7 536870912.0)) (and (= two-to-exp-a7 268435456.0) (= two-to-exp-p-minus-e-a7 0.03125))))
(assert (=> (and (<= 536870912.0 abs-a7) (< abs-a7 1073741824.0)) (and (= two-to-exp-a7 536870912.0) (= two-to-exp-p-minus-e-a7 0.015625))))

(declare-const temp-a7 Real)
(assert (= temp-a7 (* a7 two-to-exp-p-minus-e-a7)))
(assert (= temp-a7 (to_real (to_int temp-a7))))
(declare-const a8 Real)
(declare-const abs-a8 Real)
(declare-const two-to-exp-a8 Real)
(declare-const two-to-exp-p-minus-e-a8 Real)
(assert (=> (>= a8 0.0) (= abs-a8 a8)));added
(assert (=> (< a8 0.0) (= abs-a8 (- a8))));added
(assert (or (and (<= 1.0  a8) (< a8 1073741824.0)) (and (>= -1.0  a8) (> a8 -1073741824.0))))

(assert (=> (and (<= 1.0 abs-a8) (< abs-a8 2.0)) (and (= two-to-exp-a8 1.0) (= two-to-exp-p-minus-e-a8 8388608.0))))
(assert (=> (and (<= 2.0 abs-a8) (< abs-a8 4.0)) (and (= two-to-exp-a8 2.0) (= two-to-exp-p-minus-e-a8 4194304.0))))
(assert (=> (and (<= 4.0 abs-a8) (< abs-a8 8.0)) (and (= two-to-exp-a8 4.0) (= two-to-exp-p-minus-e-a8 2097152.0))))
(assert (=> (and (<= 8.0 abs-a8) (< abs-a8 16.0)) (and (= two-to-exp-a8 8.0) (= two-to-exp-p-minus-e-a8 1048576.0))))
(assert (=> (and (<= 16.0 abs-a8) (< abs-a8 32.0)) (and (= two-to-exp-a8 16.0) (= two-to-exp-p-minus-e-a8 524288.0))))
(assert (=> (and (<= 32.0 abs-a8) (< abs-a8 64.0)) (and (= two-to-exp-a8 32.0) (= two-to-exp-p-minus-e-a8 262144.0))))
(assert (=> (and (<= 64.0 abs-a8) (< abs-a8 128.0)) (and (= two-to-exp-a8 64.0) (= two-to-exp-p-minus-e-a8 131072.0))))
(assert (=> (and (<= 128.0 abs-a8) (< abs-a8 256.0)) (and (= two-to-exp-a8 128.0) (= two-to-exp-p-minus-e-a8 65536.0))))
(assert (=> (and (<= 256.0 abs-a8) (< abs-a8 512.0)) (and (= two-to-exp-a8 256.0) (= two-to-exp-p-minus-e-a8 32768.0))))
(assert (=> (and (<= 512.0 abs-a8) (< abs-a8 1024.0)) (and (= two-to-exp-a8 512.0) (= two-to-exp-p-minus-e-a8 16384.0))))
(assert (=> (and (<= 1024.0 abs-a8) (< abs-a8 2048.0)) (and (= two-to-exp-a8 1024.0) (= two-to-exp-p-minus-e-a8 8192.0))))
(assert (=> (and (<= 2048.0 abs-a8) (< abs-a8 4096.0)) (and (= two-to-exp-a8 2048.0) (= two-to-exp-p-minus-e-a8 4096.0))))
(assert (=> (and (<= 4096.0 abs-a8) (< abs-a8 8192.0)) (and (= two-to-exp-a8 4096.0) (= two-to-exp-p-minus-e-a8 2048.0))))
(assert (=> (and (<= 8192.0 abs-a8) (< abs-a8 16384.0)) (and (= two-to-exp-a8 8192.0) (= two-to-exp-p-minus-e-a8 1024.0))))
(assert (=> (and (<= 16384.0 abs-a8) (< abs-a8 32768.0)) (and (= two-to-exp-a8 16384.0) (= two-to-exp-p-minus-e-a8 512.0))))
(assert (=> (and (<= 32768.0 abs-a8) (< abs-a8 65536.0)) (and (= two-to-exp-a8 32768.0) (= two-to-exp-p-minus-e-a8 256.0))))
(assert (=> (and (<= 65536.0 abs-a8) (< abs-a8 131072.0)) (and (= two-to-exp-a8 65536.0) (= two-to-exp-p-minus-e-a8 128.0))))
(assert (=> (and (<= 131072.0 abs-a8) (< abs-a8 262144.0)) (and (= two-to-exp-a8 131072.0) (= two-to-exp-p-minus-e-a8 64.0))))
(assert (=> (and (<= 262144.0 abs-a8) (< abs-a8 524288.0)) (and (= two-to-exp-a8 262144.0) (= two-to-exp-p-minus-e-a8 32.0))))
(assert (=> (and (<= 524288.0 abs-a8) (< abs-a8 1048576.0)) (and (= two-to-exp-a8 524288.0) (= two-to-exp-p-minus-e-a8 16.0))))
(assert (=> (and (<= 1048576.0 abs-a8) (< abs-a8 2097152.0)) (and (= two-to-exp-a8 1048576.0) (= two-to-exp-p-minus-e-a8 8.0))))
(assert (=> (and (<= 2097152.0 abs-a8) (< abs-a8 4194304.0)) (and (= two-to-exp-a8 2097152.0) (= two-to-exp-p-minus-e-a8 4.0))))
(assert (=> (and (<= 4194304.0 abs-a8) (< abs-a8 8388608.0)) (and (= two-to-exp-a8 4194304.0) (= two-to-exp-p-minus-e-a8 2.0))))
(assert (=> (and (<= 8388608.0 abs-a8) (< abs-a8 16777216.0)) (and (= two-to-exp-a8 8388608.0) (= two-to-exp-p-minus-e-a8 1.0))))
(assert (=> (and (<= 16777216.0 abs-a8) (< abs-a8 33554432.0)) (and (= two-to-exp-a8 16777216.0) (= two-to-exp-p-minus-e-a8 0.5))))
(assert (=> (and (<= 33554432.0 abs-a8) (< abs-a8 67108864.0)) (and (= two-to-exp-a8 33554432.0) (= two-to-exp-p-minus-e-a8 0.25))))
(assert (=> (and (<= 67108864.0 abs-a8) (< abs-a8 134217728.0)) (and (= two-to-exp-a8 67108864.0) (= two-to-exp-p-minus-e-a8 0.125))))
(assert (=> (and (<= 134217728.0 abs-a8) (< abs-a8 268435456.0)) (and (= two-to-exp-a8 134217728.0) (= two-to-exp-p-minus-e-a8 0.0625))))
(assert (=> (and (<= 268435456.0 abs-a8) (< abs-a8 536870912.0)) (and (= two-to-exp-a8 268435456.0) (= two-to-exp-p-minus-e-a8 0.03125))))
(assert (=> (and (<= 536870912.0 abs-a8) (< abs-a8 1073741824.0)) (and (= two-to-exp-a8 536870912.0) (= two-to-exp-p-minus-e-a8 0.015625))))

(declare-const temp-a8 Real)
(assert (= temp-a8 (* a8 two-to-exp-p-minus-e-a8)))
(assert (= temp-a8 (to_real (to_int temp-a8))))
(declare-const a9 Real)
(declare-const abs-a9 Real)
(declare-const two-to-exp-a9 Real)
(declare-const two-to-exp-p-minus-e-a9 Real)
(assert (=> (>= a9 0.0) (= abs-a9 a9)));added
(assert (=> (< a9 0.0) (= abs-a9 (- a9))));added
(assert (or (and (<= 1.0  a9) (< a9 1073741824.0)) (and (>= -1.0  a9) (> a9 -1073741824.0))))

(assert (=> (and (<= 1.0 abs-a9) (< abs-a9 2.0)) (and (= two-to-exp-a9 1.0) (= two-to-exp-p-minus-e-a9 8388608.0))))
(assert (=> (and (<= 2.0 abs-a9) (< abs-a9 4.0)) (and (= two-to-exp-a9 2.0) (= two-to-exp-p-minus-e-a9 4194304.0))))
(assert (=> (and (<= 4.0 abs-a9) (< abs-a9 8.0)) (and (= two-to-exp-a9 4.0) (= two-to-exp-p-minus-e-a9 2097152.0))))
(assert (=> (and (<= 8.0 abs-a9) (< abs-a9 16.0)) (and (= two-to-exp-a9 8.0) (= two-to-exp-p-minus-e-a9 1048576.0))))
(assert (=> (and (<= 16.0 abs-a9) (< abs-a9 32.0)) (and (= two-to-exp-a9 16.0) (= two-to-exp-p-minus-e-a9 524288.0))))
(assert (=> (and (<= 32.0 abs-a9) (< abs-a9 64.0)) (and (= two-to-exp-a9 32.0) (= two-to-exp-p-minus-e-a9 262144.0))))
(assert (=> (and (<= 64.0 abs-a9) (< abs-a9 128.0)) (and (= two-to-exp-a9 64.0) (= two-to-exp-p-minus-e-a9 131072.0))))
(assert (=> (and (<= 128.0 abs-a9) (< abs-a9 256.0)) (and (= two-to-exp-a9 128.0) (= two-to-exp-p-minus-e-a9 65536.0))))
(assert (=> (and (<= 256.0 abs-a9) (< abs-a9 512.0)) (and (= two-to-exp-a9 256.0) (= two-to-exp-p-minus-e-a9 32768.0))))
(assert (=> (and (<= 512.0 abs-a9) (< abs-a9 1024.0)) (and (= two-to-exp-a9 512.0) (= two-to-exp-p-minus-e-a9 16384.0))))
(assert (=> (and (<= 1024.0 abs-a9) (< abs-a9 2048.0)) (and (= two-to-exp-a9 1024.0) (= two-to-exp-p-minus-e-a9 8192.0))))
(assert (=> (and (<= 2048.0 abs-a9) (< abs-a9 4096.0)) (and (= two-to-exp-a9 2048.0) (= two-to-exp-p-minus-e-a9 4096.0))))
(assert (=> (and (<= 4096.0 abs-a9) (< abs-a9 8192.0)) (and (= two-to-exp-a9 4096.0) (= two-to-exp-p-minus-e-a9 2048.0))))
(assert (=> (and (<= 8192.0 abs-a9) (< abs-a9 16384.0)) (and (= two-to-exp-a9 8192.0) (= two-to-exp-p-minus-e-a9 1024.0))))
(assert (=> (and (<= 16384.0 abs-a9) (< abs-a9 32768.0)) (and (= two-to-exp-a9 16384.0) (= two-to-exp-p-minus-e-a9 512.0))))
(assert (=> (and (<= 32768.0 abs-a9) (< abs-a9 65536.0)) (and (= two-to-exp-a9 32768.0) (= two-to-exp-p-minus-e-a9 256.0))))
(assert (=> (and (<= 65536.0 abs-a9) (< abs-a9 131072.0)) (and (= two-to-exp-a9 65536.0) (= two-to-exp-p-minus-e-a9 128.0))))
(assert (=> (and (<= 131072.0 abs-a9) (< abs-a9 262144.0)) (and (= two-to-exp-a9 131072.0) (= two-to-exp-p-minus-e-a9 64.0))))
(assert (=> (and (<= 262144.0 abs-a9) (< abs-a9 524288.0)) (and (= two-to-exp-a9 262144.0) (= two-to-exp-p-minus-e-a9 32.0))))
(assert (=> (and (<= 524288.0 abs-a9) (< abs-a9 1048576.0)) (and (= two-to-exp-a9 524288.0) (= two-to-exp-p-minus-e-a9 16.0))))
(assert (=> (and (<= 1048576.0 abs-a9) (< abs-a9 2097152.0)) (and (= two-to-exp-a9 1048576.0) (= two-to-exp-p-minus-e-a9 8.0))))
(assert (=> (and (<= 2097152.0 abs-a9) (< abs-a9 4194304.0)) (and (= two-to-exp-a9 2097152.0) (= two-to-exp-p-minus-e-a9 4.0))))
(assert (=> (and (<= 4194304.0 abs-a9) (< abs-a9 8388608.0)) (and (= two-to-exp-a9 4194304.0) (= two-to-exp-p-minus-e-a9 2.0))))
(assert (=> (and (<= 8388608.0 abs-a9) (< abs-a9 16777216.0)) (and (= two-to-exp-a9 8388608.0) (= two-to-exp-p-minus-e-a9 1.0))))
(assert (=> (and (<= 16777216.0 abs-a9) (< abs-a9 33554432.0)) (and (= two-to-exp-a9 16777216.0) (= two-to-exp-p-minus-e-a9 0.5))))
(assert (=> (and (<= 33554432.0 abs-a9) (< abs-a9 67108864.0)) (and (= two-to-exp-a9 33554432.0) (= two-to-exp-p-minus-e-a9 0.25))))
(assert (=> (and (<= 67108864.0 abs-a9) (< abs-a9 134217728.0)) (and (= two-to-exp-a9 67108864.0) (= two-to-exp-p-minus-e-a9 0.125))))
(assert (=> (and (<= 134217728.0 abs-a9) (< abs-a9 268435456.0)) (and (= two-to-exp-a9 134217728.0) (= two-to-exp-p-minus-e-a9 0.0625))))
(assert (=> (and (<= 268435456.0 abs-a9) (< abs-a9 536870912.0)) (and (= two-to-exp-a9 268435456.0) (= two-to-exp-p-minus-e-a9 0.03125))))
(assert (=> (and (<= 536870912.0 abs-a9) (< abs-a9 1073741824.0)) (and (= two-to-exp-a9 536870912.0) (= two-to-exp-p-minus-e-a9 0.015625))))

(declare-const temp-a9 Real)
(assert (= temp-a9 (* a9 two-to-exp-p-minus-e-a9)))
(assert (= temp-a9 (to_real (to_int temp-a9))))
(declare-const a10 Real)
(declare-const abs-a10 Real)
(declare-const two-to-exp-a10 Real)
(declare-const two-to-exp-p-minus-e-a10 Real)
(assert (=> (>= a10 0.0) (= abs-a10 a10)));added
(assert (=> (< a10 0.0) (= abs-a10 (- a10))));added
(assert (or (and (<= 1.0  a10) (< a10 1073741824.0)) (and (>= -1.0  a10) (> a10 -1073741824.0))))

(assert (=> (and (<= 1.0 abs-a10) (< abs-a10 2.0)) (and (= two-to-exp-a10 1.0) (= two-to-exp-p-minus-e-a10 8388608.0))))
(assert (=> (and (<= 2.0 abs-a10) (< abs-a10 4.0)) (and (= two-to-exp-a10 2.0) (= two-to-exp-p-minus-e-a10 4194304.0))))
(assert (=> (and (<= 4.0 abs-a10) (< abs-a10 8.0)) (and (= two-to-exp-a10 4.0) (= two-to-exp-p-minus-e-a10 2097152.0))))
(assert (=> (and (<= 8.0 abs-a10) (< abs-a10 16.0)) (and (= two-to-exp-a10 8.0) (= two-to-exp-p-minus-e-a10 1048576.0))))
(assert (=> (and (<= 16.0 abs-a10) (< abs-a10 32.0)) (and (= two-to-exp-a10 16.0) (= two-to-exp-p-minus-e-a10 524288.0))))
(assert (=> (and (<= 32.0 abs-a10) (< abs-a10 64.0)) (and (= two-to-exp-a10 32.0) (= two-to-exp-p-minus-e-a10 262144.0))))
(assert (=> (and (<= 64.0 abs-a10) (< abs-a10 128.0)) (and (= two-to-exp-a10 64.0) (= two-to-exp-p-minus-e-a10 131072.0))))
(assert (=> (and (<= 128.0 abs-a10) (< abs-a10 256.0)) (and (= two-to-exp-a10 128.0) (= two-to-exp-p-minus-e-a10 65536.0))))
(assert (=> (and (<= 256.0 abs-a10) (< abs-a10 512.0)) (and (= two-to-exp-a10 256.0) (= two-to-exp-p-minus-e-a10 32768.0))))
(assert (=> (and (<= 512.0 abs-a10) (< abs-a10 1024.0)) (and (= two-to-exp-a10 512.0) (= two-to-exp-p-minus-e-a10 16384.0))))
(assert (=> (and (<= 1024.0 abs-a10) (< abs-a10 2048.0)) (and (= two-to-exp-a10 1024.0) (= two-to-exp-p-minus-e-a10 8192.0))))
(assert (=> (and (<= 2048.0 abs-a10) (< abs-a10 4096.0)) (and (= two-to-exp-a10 2048.0) (= two-to-exp-p-minus-e-a10 4096.0))))
(assert (=> (and (<= 4096.0 abs-a10) (< abs-a10 8192.0)) (and (= two-to-exp-a10 4096.0) (= two-to-exp-p-minus-e-a10 2048.0))))
(assert (=> (and (<= 8192.0 abs-a10) (< abs-a10 16384.0)) (and (= two-to-exp-a10 8192.0) (= two-to-exp-p-minus-e-a10 1024.0))))
(assert (=> (and (<= 16384.0 abs-a10) (< abs-a10 32768.0)) (and (= two-to-exp-a10 16384.0) (= two-to-exp-p-minus-e-a10 512.0))))
(assert (=> (and (<= 32768.0 abs-a10) (< abs-a10 65536.0)) (and (= two-to-exp-a10 32768.0) (= two-to-exp-p-minus-e-a10 256.0))))
(assert (=> (and (<= 65536.0 abs-a10) (< abs-a10 131072.0)) (and (= two-to-exp-a10 65536.0) (= two-to-exp-p-minus-e-a10 128.0))))
(assert (=> (and (<= 131072.0 abs-a10) (< abs-a10 262144.0)) (and (= two-to-exp-a10 131072.0) (= two-to-exp-p-minus-e-a10 64.0))))
(assert (=> (and (<= 262144.0 abs-a10) (< abs-a10 524288.0)) (and (= two-to-exp-a10 262144.0) (= two-to-exp-p-minus-e-a10 32.0))))
(assert (=> (and (<= 524288.0 abs-a10) (< abs-a10 1048576.0)) (and (= two-to-exp-a10 524288.0) (= two-to-exp-p-minus-e-a10 16.0))))
(assert (=> (and (<= 1048576.0 abs-a10) (< abs-a10 2097152.0)) (and (= two-to-exp-a10 1048576.0) (= two-to-exp-p-minus-e-a10 8.0))))
(assert (=> (and (<= 2097152.0 abs-a10) (< abs-a10 4194304.0)) (and (= two-to-exp-a10 2097152.0) (= two-to-exp-p-minus-e-a10 4.0))))
(assert (=> (and (<= 4194304.0 abs-a10) (< abs-a10 8388608.0)) (and (= two-to-exp-a10 4194304.0) (= two-to-exp-p-minus-e-a10 2.0))))
(assert (=> (and (<= 8388608.0 abs-a10) (< abs-a10 16777216.0)) (and (= two-to-exp-a10 8388608.0) (= two-to-exp-p-minus-e-a10 1.0))))
(assert (=> (and (<= 16777216.0 abs-a10) (< abs-a10 33554432.0)) (and (= two-to-exp-a10 16777216.0) (= two-to-exp-p-minus-e-a10 0.5))))
(assert (=> (and (<= 33554432.0 abs-a10) (< abs-a10 67108864.0)) (and (= two-to-exp-a10 33554432.0) (= two-to-exp-p-minus-e-a10 0.25))))
(assert (=> (and (<= 67108864.0 abs-a10) (< abs-a10 134217728.0)) (and (= two-to-exp-a10 67108864.0) (= two-to-exp-p-minus-e-a10 0.125))))
(assert (=> (and (<= 134217728.0 abs-a10) (< abs-a10 268435456.0)) (and (= two-to-exp-a10 134217728.0) (= two-to-exp-p-minus-e-a10 0.0625))))
(assert (=> (and (<= 268435456.0 abs-a10) (< abs-a10 536870912.0)) (and (= two-to-exp-a10 268435456.0) (= two-to-exp-p-minus-e-a10 0.03125))))
(assert (=> (and (<= 536870912.0 abs-a10) (< abs-a10 1073741824.0)) (and (= two-to-exp-a10 536870912.0) (= two-to-exp-p-minus-e-a10 0.015625))))

(declare-const temp-a10 Real)
(assert (= temp-a10 (* a10 two-to-exp-p-minus-e-a10)))
(assert (= temp-a10 (to_real (to_int temp-a10))))
(declare-const a11 Real)
(declare-const abs-a11 Real)
(declare-const two-to-exp-a11 Real)
(declare-const two-to-exp-p-minus-e-a11 Real)
(assert (=> (>= a11 0.0) (= abs-a11 a11)));added
(assert (=> (< a11 0.0) (= abs-a11 (- a11))));added
(assert (or (and (<= 1.0  a11) (< a11 1073741824.0)) (and (>= -1.0  a11) (> a11 -1073741824.0))))

(assert (=> (and (<= 1.0 abs-a11) (< abs-a11 2.0)) (and (= two-to-exp-a11 1.0) (= two-to-exp-p-minus-e-a11 8388608.0))))
(assert (=> (and (<= 2.0 abs-a11) (< abs-a11 4.0)) (and (= two-to-exp-a11 2.0) (= two-to-exp-p-minus-e-a11 4194304.0))))
(assert (=> (and (<= 4.0 abs-a11) (< abs-a11 8.0)) (and (= two-to-exp-a11 4.0) (= two-to-exp-p-minus-e-a11 2097152.0))))
(assert (=> (and (<= 8.0 abs-a11) (< abs-a11 16.0)) (and (= two-to-exp-a11 8.0) (= two-to-exp-p-minus-e-a11 1048576.0))))
(assert (=> (and (<= 16.0 abs-a11) (< abs-a11 32.0)) (and (= two-to-exp-a11 16.0) (= two-to-exp-p-minus-e-a11 524288.0))))
(assert (=> (and (<= 32.0 abs-a11) (< abs-a11 64.0)) (and (= two-to-exp-a11 32.0) (= two-to-exp-p-minus-e-a11 262144.0))))
(assert (=> (and (<= 64.0 abs-a11) (< abs-a11 128.0)) (and (= two-to-exp-a11 64.0) (= two-to-exp-p-minus-e-a11 131072.0))))
(assert (=> (and (<= 128.0 abs-a11) (< abs-a11 256.0)) (and (= two-to-exp-a11 128.0) (= two-to-exp-p-minus-e-a11 65536.0))))
(assert (=> (and (<= 256.0 abs-a11) (< abs-a11 512.0)) (and (= two-to-exp-a11 256.0) (= two-to-exp-p-minus-e-a11 32768.0))))
(assert (=> (and (<= 512.0 abs-a11) (< abs-a11 1024.0)) (and (= two-to-exp-a11 512.0) (= two-to-exp-p-minus-e-a11 16384.0))))
(assert (=> (and (<= 1024.0 abs-a11) (< abs-a11 2048.0)) (and (= two-to-exp-a11 1024.0) (= two-to-exp-p-minus-e-a11 8192.0))))
(assert (=> (and (<= 2048.0 abs-a11) (< abs-a11 4096.0)) (and (= two-to-exp-a11 2048.0) (= two-to-exp-p-minus-e-a11 4096.0))))
(assert (=> (and (<= 4096.0 abs-a11) (< abs-a11 8192.0)) (and (= two-to-exp-a11 4096.0) (= two-to-exp-p-minus-e-a11 2048.0))))
(assert (=> (and (<= 8192.0 abs-a11) (< abs-a11 16384.0)) (and (= two-to-exp-a11 8192.0) (= two-to-exp-p-minus-e-a11 1024.0))))
(assert (=> (and (<= 16384.0 abs-a11) (< abs-a11 32768.0)) (and (= two-to-exp-a11 16384.0) (= two-to-exp-p-minus-e-a11 512.0))))
(assert (=> (and (<= 32768.0 abs-a11) (< abs-a11 65536.0)) (and (= two-to-exp-a11 32768.0) (= two-to-exp-p-minus-e-a11 256.0))))
(assert (=> (and (<= 65536.0 abs-a11) (< abs-a11 131072.0)) (and (= two-to-exp-a11 65536.0) (= two-to-exp-p-minus-e-a11 128.0))))
(assert (=> (and (<= 131072.0 abs-a11) (< abs-a11 262144.0)) (and (= two-to-exp-a11 131072.0) (= two-to-exp-p-minus-e-a11 64.0))))
(assert (=> (and (<= 262144.0 abs-a11) (< abs-a11 524288.0)) (and (= two-to-exp-a11 262144.0) (= two-to-exp-p-minus-e-a11 32.0))))
(assert (=> (and (<= 524288.0 abs-a11) (< abs-a11 1048576.0)) (and (= two-to-exp-a11 524288.0) (= two-to-exp-p-minus-e-a11 16.0))))
(assert (=> (and (<= 1048576.0 abs-a11) (< abs-a11 2097152.0)) (and (= two-to-exp-a11 1048576.0) (= two-to-exp-p-minus-e-a11 8.0))))
(assert (=> (and (<= 2097152.0 abs-a11) (< abs-a11 4194304.0)) (and (= two-to-exp-a11 2097152.0) (= two-to-exp-p-minus-e-a11 4.0))))
(assert (=> (and (<= 4194304.0 abs-a11) (< abs-a11 8388608.0)) (and (= two-to-exp-a11 4194304.0) (= two-to-exp-p-minus-e-a11 2.0))))
(assert (=> (and (<= 8388608.0 abs-a11) (< abs-a11 16777216.0)) (and (= two-to-exp-a11 8388608.0) (= two-to-exp-p-minus-e-a11 1.0))))
(assert (=> (and (<= 16777216.0 abs-a11) (< abs-a11 33554432.0)) (and (= two-to-exp-a11 16777216.0) (= two-to-exp-p-minus-e-a11 0.5))))
(assert (=> (and (<= 33554432.0 abs-a11) (< abs-a11 67108864.0)) (and (= two-to-exp-a11 33554432.0) (= two-to-exp-p-minus-e-a11 0.25))))
(assert (=> (and (<= 67108864.0 abs-a11) (< abs-a11 134217728.0)) (and (= two-to-exp-a11 67108864.0) (= two-to-exp-p-minus-e-a11 0.125))))
(assert (=> (and (<= 134217728.0 abs-a11) (< abs-a11 268435456.0)) (and (= two-to-exp-a11 134217728.0) (= two-to-exp-p-minus-e-a11 0.0625))))
(assert (=> (and (<= 268435456.0 abs-a11) (< abs-a11 536870912.0)) (and (= two-to-exp-a11 268435456.0) (= two-to-exp-p-minus-e-a11 0.03125))))
(assert (=> (and (<= 536870912.0 abs-a11) (< abs-a11 1073741824.0)) (and (= two-to-exp-a11 536870912.0) (= two-to-exp-p-minus-e-a11 0.015625))))

(declare-const temp-a11 Real)
(assert (= temp-a11 (* a11 two-to-exp-p-minus-e-a11)))
(assert (= temp-a11 (to_real (to_int temp-a11))))
(declare-const a12 Real)
(declare-const abs-a12 Real)
(declare-const two-to-exp-a12 Real)
(declare-const two-to-exp-p-minus-e-a12 Real)
(assert (=> (>= a12 0.0) (= abs-a12 a12)));added
(assert (=> (< a12 0.0) (= abs-a12 (- a12))));added
(assert (or (and (<= 1.0  a12) (< a12 1073741824.0)) (and (>= -1.0  a12) (> a12 -1073741824.0))))

(assert (=> (and (<= 1.0 abs-a12) (< abs-a12 2.0)) (and (= two-to-exp-a12 1.0) (= two-to-exp-p-minus-e-a12 8388608.0))))
(assert (=> (and (<= 2.0 abs-a12) (< abs-a12 4.0)) (and (= two-to-exp-a12 2.0) (= two-to-exp-p-minus-e-a12 4194304.0))))
(assert (=> (and (<= 4.0 abs-a12) (< abs-a12 8.0)) (and (= two-to-exp-a12 4.0) (= two-to-exp-p-minus-e-a12 2097152.0))))
(assert (=> (and (<= 8.0 abs-a12) (< abs-a12 16.0)) (and (= two-to-exp-a12 8.0) (= two-to-exp-p-minus-e-a12 1048576.0))))
(assert (=> (and (<= 16.0 abs-a12) (< abs-a12 32.0)) (and (= two-to-exp-a12 16.0) (= two-to-exp-p-minus-e-a12 524288.0))))
(assert (=> (and (<= 32.0 abs-a12) (< abs-a12 64.0)) (and (= two-to-exp-a12 32.0) (= two-to-exp-p-minus-e-a12 262144.0))))
(assert (=> (and (<= 64.0 abs-a12) (< abs-a12 128.0)) (and (= two-to-exp-a12 64.0) (= two-to-exp-p-minus-e-a12 131072.0))))
(assert (=> (and (<= 128.0 abs-a12) (< abs-a12 256.0)) (and (= two-to-exp-a12 128.0) (= two-to-exp-p-minus-e-a12 65536.0))))
(assert (=> (and (<= 256.0 abs-a12) (< abs-a12 512.0)) (and (= two-to-exp-a12 256.0) (= two-to-exp-p-minus-e-a12 32768.0))))
(assert (=> (and (<= 512.0 abs-a12) (< abs-a12 1024.0)) (and (= two-to-exp-a12 512.0) (= two-to-exp-p-minus-e-a12 16384.0))))
(assert (=> (and (<= 1024.0 abs-a12) (< abs-a12 2048.0)) (and (= two-to-exp-a12 1024.0) (= two-to-exp-p-minus-e-a12 8192.0))))
(assert (=> (and (<= 2048.0 abs-a12) (< abs-a12 4096.0)) (and (= two-to-exp-a12 2048.0) (= two-to-exp-p-minus-e-a12 4096.0))))
(assert (=> (and (<= 4096.0 abs-a12) (< abs-a12 8192.0)) (and (= two-to-exp-a12 4096.0) (= two-to-exp-p-minus-e-a12 2048.0))))
(assert (=> (and (<= 8192.0 abs-a12) (< abs-a12 16384.0)) (and (= two-to-exp-a12 8192.0) (= two-to-exp-p-minus-e-a12 1024.0))))
(assert (=> (and (<= 16384.0 abs-a12) (< abs-a12 32768.0)) (and (= two-to-exp-a12 16384.0) (= two-to-exp-p-minus-e-a12 512.0))))
(assert (=> (and (<= 32768.0 abs-a12) (< abs-a12 65536.0)) (and (= two-to-exp-a12 32768.0) (= two-to-exp-p-minus-e-a12 256.0))))
(assert (=> (and (<= 65536.0 abs-a12) (< abs-a12 131072.0)) (and (= two-to-exp-a12 65536.0) (= two-to-exp-p-minus-e-a12 128.0))))
(assert (=> (and (<= 131072.0 abs-a12) (< abs-a12 262144.0)) (and (= two-to-exp-a12 131072.0) (= two-to-exp-p-minus-e-a12 64.0))))
(assert (=> (and (<= 262144.0 abs-a12) (< abs-a12 524288.0)) (and (= two-to-exp-a12 262144.0) (= two-to-exp-p-minus-e-a12 32.0))))
(assert (=> (and (<= 524288.0 abs-a12) (< abs-a12 1048576.0)) (and (= two-to-exp-a12 524288.0) (= two-to-exp-p-minus-e-a12 16.0))))
(assert (=> (and (<= 1048576.0 abs-a12) (< abs-a12 2097152.0)) (and (= two-to-exp-a12 1048576.0) (= two-to-exp-p-minus-e-a12 8.0))))
(assert (=> (and (<= 2097152.0 abs-a12) (< abs-a12 4194304.0)) (and (= two-to-exp-a12 2097152.0) (= two-to-exp-p-minus-e-a12 4.0))))
(assert (=> (and (<= 4194304.0 abs-a12) (< abs-a12 8388608.0)) (and (= two-to-exp-a12 4194304.0) (= two-to-exp-p-minus-e-a12 2.0))))
(assert (=> (and (<= 8388608.0 abs-a12) (< abs-a12 16777216.0)) (and (= two-to-exp-a12 8388608.0) (= two-to-exp-p-minus-e-a12 1.0))))
(assert (=> (and (<= 16777216.0 abs-a12) (< abs-a12 33554432.0)) (and (= two-to-exp-a12 16777216.0) (= two-to-exp-p-minus-e-a12 0.5))))
(assert (=> (and (<= 33554432.0 abs-a12) (< abs-a12 67108864.0)) (and (= two-to-exp-a12 33554432.0) (= two-to-exp-p-minus-e-a12 0.25))))
(assert (=> (and (<= 67108864.0 abs-a12) (< abs-a12 134217728.0)) (and (= two-to-exp-a12 67108864.0) (= two-to-exp-p-minus-e-a12 0.125))))
(assert (=> (and (<= 134217728.0 abs-a12) (< abs-a12 268435456.0)) (and (= two-to-exp-a12 134217728.0) (= two-to-exp-p-minus-e-a12 0.0625))))
(assert (=> (and (<= 268435456.0 abs-a12) (< abs-a12 536870912.0)) (and (= two-to-exp-a12 268435456.0) (= two-to-exp-p-minus-e-a12 0.03125))))
(assert (=> (and (<= 536870912.0 abs-a12) (< abs-a12 1073741824.0)) (and (= two-to-exp-a12 536870912.0) (= two-to-exp-p-minus-e-a12 0.015625))))

(declare-const temp-a12 Real)
(assert (= temp-a12 (* a12 two-to-exp-p-minus-e-a12)))
(assert (= temp-a12 (to_real (to_int temp-a12))))


(declare-const new10 Real)

(declare-const abs-new10 Real)
(assert (or (and (<= 1.0  new10) (< new10 1073741824.0)) (and (>= -1.0  new10) (> new10 -1073741824.0))))
(assert (=> (>= new10 0.0) (= abs-new10 new10)));added
(assert (=> (< new10 0.0) (= abs-new10 (- new10))));added
(declare-const new10-real Real)
(declare-const two-to-exp-new10 Real)
(declare-const two-to-exp-p-minus-e-new10 Real)
(assert (=> (and (<= 1.0 abs-new10) (< abs-new10 2.0)) (and (= two-to-exp-new10 1.0) (= two-to-exp-p-minus-e-new10 8388608.0))))
(assert (=> (and (<= 2.0 abs-new10) (< abs-new10 4.0)) (and (= two-to-exp-new10 2.0) (= two-to-exp-p-minus-e-new10 4194304.0))))
(assert (=> (and (<= 4.0 abs-new10) (< abs-new10 8.0)) (and (= two-to-exp-new10 4.0) (= two-to-exp-p-minus-e-new10 2097152.0))))
(assert (=> (and (<= 8.0 abs-new10) (< abs-new10 16.0)) (and (= two-to-exp-new10 8.0) (= two-to-exp-p-minus-e-new10 1048576.0))))
(assert (=> (and (<= 16.0 abs-new10) (< abs-new10 32.0)) (and (= two-to-exp-new10 16.0) (= two-to-exp-p-minus-e-new10 524288.0))))
(assert (=> (and (<= 32.0 abs-new10) (< abs-new10 64.0)) (and (= two-to-exp-new10 32.0) (= two-to-exp-p-minus-e-new10 262144.0))))
(assert (=> (and (<= 64.0 abs-new10) (< abs-new10 128.0)) (and (= two-to-exp-new10 64.0) (= two-to-exp-p-minus-e-new10 131072.0))))
(assert (=> (and (<= 128.0 abs-new10) (< abs-new10 256.0)) (and (= two-to-exp-new10 128.0) (= two-to-exp-p-minus-e-new10 65536.0))))
(assert (=> (and (<= 256.0 abs-new10) (< abs-new10 512.0)) (and (= two-to-exp-new10 256.0) (= two-to-exp-p-minus-e-new10 32768.0))))
(assert (=> (and (<= 512.0 abs-new10) (< abs-new10 1024.0)) (and (= two-to-exp-new10 512.0) (= two-to-exp-p-minus-e-new10 16384.0))))
(assert (=> (and (<= 1024.0 abs-new10) (< abs-new10 2048.0)) (and (= two-to-exp-new10 1024.0) (= two-to-exp-p-minus-e-new10 8192.0))))
(assert (=> (and (<= 2048.0 abs-new10) (< abs-new10 4096.0)) (and (= two-to-exp-new10 2048.0) (= two-to-exp-p-minus-e-new10 4096.0))))
(assert (=> (and (<= 4096.0 abs-new10) (< abs-new10 8192.0)) (and (= two-to-exp-new10 4096.0) (= two-to-exp-p-minus-e-new10 2048.0))))
(assert (=> (and (<= 8192.0 abs-new10) (< abs-new10 16384.0)) (and (= two-to-exp-new10 8192.0) (= two-to-exp-p-minus-e-new10 1024.0))))
(assert (=> (and (<= 16384.0 abs-new10) (< abs-new10 32768.0)) (and (= two-to-exp-new10 16384.0) (= two-to-exp-p-minus-e-new10 512.0))))
(assert (=> (and (<= 32768.0 abs-new10) (< abs-new10 65536.0)) (and (= two-to-exp-new10 32768.0) (= two-to-exp-p-minus-e-new10 256.0))))
(assert (=> (and (<= 65536.0 abs-new10) (< abs-new10 131072.0)) (and (= two-to-exp-new10 65536.0) (= two-to-exp-p-minus-e-new10 128.0))))
(assert (=> (and (<= 131072.0 abs-new10) (< abs-new10 262144.0)) (and (= two-to-exp-new10 131072.0) (= two-to-exp-p-minus-e-new10 64.0))))
(assert (=> (and (<= 262144.0 abs-new10) (< abs-new10 524288.0)) (and (= two-to-exp-new10 262144.0) (= two-to-exp-p-minus-e-new10 32.0))))
(assert (=> (and (<= 524288.0 abs-new10) (< abs-new10 1048576.0)) (and (= two-to-exp-new10 524288.0) (= two-to-exp-p-minus-e-new10 16.0))))
(assert (=> (and (<= 1048576.0 abs-new10) (< abs-new10 2097152.0)) (and (= two-to-exp-new10 1048576.0) (= two-to-exp-p-minus-e-new10 8.0))))
(assert (=> (and (<= 2097152.0 abs-new10) (< abs-new10 4194304.0)) (and (= two-to-exp-new10 2097152.0) (= two-to-exp-p-minus-e-new10 4.0))))
(assert (=> (and (<= 4194304.0 abs-new10) (< abs-new10 8388608.0)) (and (= two-to-exp-new10 4194304.0) (= two-to-exp-p-minus-e-new10 2.0))))
(assert (=> (and (<= 8388608.0 abs-new10) (< abs-new10 16777216.0)) (and (= two-to-exp-new10 8388608.0) (= two-to-exp-p-minus-e-new10 1.0))))
(assert (=> (and (<= 16777216.0 abs-new10) (< abs-new10 33554432.0)) (and (= two-to-exp-new10 16777216.0) (= two-to-exp-p-minus-e-new10 0.5))))
(assert (=> (and (<= 33554432.0 abs-new10) (< abs-new10 67108864.0)) (and (= two-to-exp-new10 33554432.0) (= two-to-exp-p-minus-e-new10 0.25))))
(assert (=> (and (<= 67108864.0 abs-new10) (< abs-new10 134217728.0)) (and (= two-to-exp-new10 67108864.0) (= two-to-exp-p-minus-e-new10 0.125))))
(assert (=> (and (<= 134217728.0 abs-new10) (< abs-new10 268435456.0)) (and (= two-to-exp-new10 134217728.0) (= two-to-exp-p-minus-e-new10 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new10) (< abs-new10 536870912.0)) (and (= two-to-exp-new10 268435456.0) (= two-to-exp-p-minus-e-new10 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new10) (< abs-new10 1073741824.0)) (and (= two-to-exp-new10 536870912.0) (= two-to-exp-p-minus-e-new10 0.015625))))

(assert (= new10-real (+ a1 a2)))

;(assert (= new10  (* (/ (to_real (to_int (* (/ new10-real two-to-exp-new10) two-to-p))) two-to-p) two-to-exp-new10 )))
(assert (= (* two-to-exp-p-minus-e-new10 new10) (to_real (to_int (* new10-real two-to-exp-p-minus-e-new10)))))

(declare-const new9 Real)

(declare-const abs-new9 Real)
(assert (or (and (<= 1.0  new9) (< new9 1073741824.0)) (and (>= -1.0  new9) (> new9 -1073741824.0))))
(assert (=> (>= new9 0.0) (= abs-new9 new9)));added
(assert (=> (< new9 0.0) (= abs-new9 (- new9))));added
(declare-const new9-real Real)
(declare-const two-to-exp-new9 Real)
(declare-const two-to-exp-p-minus-e-new9 Real)
(assert (=> (and (<= 1.0 abs-new9) (< abs-new9 2.0)) (and (= two-to-exp-new9 1.0) (= two-to-exp-p-minus-e-new9 8388608.0))))
(assert (=> (and (<= 2.0 abs-new9) (< abs-new9 4.0)) (and (= two-to-exp-new9 2.0) (= two-to-exp-p-minus-e-new9 4194304.0))))
(assert (=> (and (<= 4.0 abs-new9) (< abs-new9 8.0)) (and (= two-to-exp-new9 4.0) (= two-to-exp-p-minus-e-new9 2097152.0))))
(assert (=> (and (<= 8.0 abs-new9) (< abs-new9 16.0)) (and (= two-to-exp-new9 8.0) (= two-to-exp-p-minus-e-new9 1048576.0))))
(assert (=> (and (<= 16.0 abs-new9) (< abs-new9 32.0)) (and (= two-to-exp-new9 16.0) (= two-to-exp-p-minus-e-new9 524288.0))))
(assert (=> (and (<= 32.0 abs-new9) (< abs-new9 64.0)) (and (= two-to-exp-new9 32.0) (= two-to-exp-p-minus-e-new9 262144.0))))
(assert (=> (and (<= 64.0 abs-new9) (< abs-new9 128.0)) (and (= two-to-exp-new9 64.0) (= two-to-exp-p-minus-e-new9 131072.0))))
(assert (=> (and (<= 128.0 abs-new9) (< abs-new9 256.0)) (and (= two-to-exp-new9 128.0) (= two-to-exp-p-minus-e-new9 65536.0))))
(assert (=> (and (<= 256.0 abs-new9) (< abs-new9 512.0)) (and (= two-to-exp-new9 256.0) (= two-to-exp-p-minus-e-new9 32768.0))))
(assert (=> (and (<= 512.0 abs-new9) (< abs-new9 1024.0)) (and (= two-to-exp-new9 512.0) (= two-to-exp-p-minus-e-new9 16384.0))))
(assert (=> (and (<= 1024.0 abs-new9) (< abs-new9 2048.0)) (and (= two-to-exp-new9 1024.0) (= two-to-exp-p-minus-e-new9 8192.0))))
(assert (=> (and (<= 2048.0 abs-new9) (< abs-new9 4096.0)) (and (= two-to-exp-new9 2048.0) (= two-to-exp-p-minus-e-new9 4096.0))))
(assert (=> (and (<= 4096.0 abs-new9) (< abs-new9 8192.0)) (and (= two-to-exp-new9 4096.0) (= two-to-exp-p-minus-e-new9 2048.0))))
(assert (=> (and (<= 8192.0 abs-new9) (< abs-new9 16384.0)) (and (= two-to-exp-new9 8192.0) (= two-to-exp-p-minus-e-new9 1024.0))))
(assert (=> (and (<= 16384.0 abs-new9) (< abs-new9 32768.0)) (and (= two-to-exp-new9 16384.0) (= two-to-exp-p-minus-e-new9 512.0))))
(assert (=> (and (<= 32768.0 abs-new9) (< abs-new9 65536.0)) (and (= two-to-exp-new9 32768.0) (= two-to-exp-p-minus-e-new9 256.0))))
(assert (=> (and (<= 65536.0 abs-new9) (< abs-new9 131072.0)) (and (= two-to-exp-new9 65536.0) (= two-to-exp-p-minus-e-new9 128.0))))
(assert (=> (and (<= 131072.0 abs-new9) (< abs-new9 262144.0)) (and (= two-to-exp-new9 131072.0) (= two-to-exp-p-minus-e-new9 64.0))))
(assert (=> (and (<= 262144.0 abs-new9) (< abs-new9 524288.0)) (and (= two-to-exp-new9 262144.0) (= two-to-exp-p-minus-e-new9 32.0))))
(assert (=> (and (<= 524288.0 abs-new9) (< abs-new9 1048576.0)) (and (= two-to-exp-new9 524288.0) (= two-to-exp-p-minus-e-new9 16.0))))
(assert (=> (and (<= 1048576.0 abs-new9) (< abs-new9 2097152.0)) (and (= two-to-exp-new9 1048576.0) (= two-to-exp-p-minus-e-new9 8.0))))
(assert (=> (and (<= 2097152.0 abs-new9) (< abs-new9 4194304.0)) (and (= two-to-exp-new9 2097152.0) (= two-to-exp-p-minus-e-new9 4.0))))
(assert (=> (and (<= 4194304.0 abs-new9) (< abs-new9 8388608.0)) (and (= two-to-exp-new9 4194304.0) (= two-to-exp-p-minus-e-new9 2.0))))
(assert (=> (and (<= 8388608.0 abs-new9) (< abs-new9 16777216.0)) (and (= two-to-exp-new9 8388608.0) (= two-to-exp-p-minus-e-new9 1.0))))
(assert (=> (and (<= 16777216.0 abs-new9) (< abs-new9 33554432.0)) (and (= two-to-exp-new9 16777216.0) (= two-to-exp-p-minus-e-new9 0.5))))
(assert (=> (and (<= 33554432.0 abs-new9) (< abs-new9 67108864.0)) (and (= two-to-exp-new9 33554432.0) (= two-to-exp-p-minus-e-new9 0.25))))
(assert (=> (and (<= 67108864.0 abs-new9) (< abs-new9 134217728.0)) (and (= two-to-exp-new9 67108864.0) (= two-to-exp-p-minus-e-new9 0.125))))
(assert (=> (and (<= 134217728.0 abs-new9) (< abs-new9 268435456.0)) (and (= two-to-exp-new9 134217728.0) (= two-to-exp-p-minus-e-new9 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new9) (< abs-new9 536870912.0)) (and (= two-to-exp-new9 268435456.0) (= two-to-exp-p-minus-e-new9 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new9) (< abs-new9 1073741824.0)) (and (= two-to-exp-new9 536870912.0) (= two-to-exp-p-minus-e-new9 0.015625))))

(assert (= new9-real (+ new10 a3)))

;(assert (= new9  (* (/ (to_real (to_int (* (/ new9-real two-to-exp-new9) two-to-p))) two-to-p) two-to-exp-new9 )))
(assert (= (* two-to-exp-p-minus-e-new9 new9) (to_real (to_int (* new9-real two-to-exp-p-minus-e-new9)))))

(declare-const new8 Real)

(declare-const abs-new8 Real)
(assert (or (and (<= 1.0  new8) (< new8 1073741824.0)) (and (>= -1.0  new8) (> new8 -1073741824.0))))
(assert (=> (>= new8 0.0) (= abs-new8 new8)));added
(assert (=> (< new8 0.0) (= abs-new8 (- new8))));added
(declare-const new8-real Real)
(declare-const two-to-exp-new8 Real)
(declare-const two-to-exp-p-minus-e-new8 Real)
(assert (=> (and (<= 1.0 abs-new8) (< abs-new8 2.0)) (and (= two-to-exp-new8 1.0) (= two-to-exp-p-minus-e-new8 8388608.0))))
(assert (=> (and (<= 2.0 abs-new8) (< abs-new8 4.0)) (and (= two-to-exp-new8 2.0) (= two-to-exp-p-minus-e-new8 4194304.0))))
(assert (=> (and (<= 4.0 abs-new8) (< abs-new8 8.0)) (and (= two-to-exp-new8 4.0) (= two-to-exp-p-minus-e-new8 2097152.0))))
(assert (=> (and (<= 8.0 abs-new8) (< abs-new8 16.0)) (and (= two-to-exp-new8 8.0) (= two-to-exp-p-minus-e-new8 1048576.0))))
(assert (=> (and (<= 16.0 abs-new8) (< abs-new8 32.0)) (and (= two-to-exp-new8 16.0) (= two-to-exp-p-minus-e-new8 524288.0))))
(assert (=> (and (<= 32.0 abs-new8) (< abs-new8 64.0)) (and (= two-to-exp-new8 32.0) (= two-to-exp-p-minus-e-new8 262144.0))))
(assert (=> (and (<= 64.0 abs-new8) (< abs-new8 128.0)) (and (= two-to-exp-new8 64.0) (= two-to-exp-p-minus-e-new8 131072.0))))
(assert (=> (and (<= 128.0 abs-new8) (< abs-new8 256.0)) (and (= two-to-exp-new8 128.0) (= two-to-exp-p-minus-e-new8 65536.0))))
(assert (=> (and (<= 256.0 abs-new8) (< abs-new8 512.0)) (and (= two-to-exp-new8 256.0) (= two-to-exp-p-minus-e-new8 32768.0))))
(assert (=> (and (<= 512.0 abs-new8) (< abs-new8 1024.0)) (and (= two-to-exp-new8 512.0) (= two-to-exp-p-minus-e-new8 16384.0))))
(assert (=> (and (<= 1024.0 abs-new8) (< abs-new8 2048.0)) (and (= two-to-exp-new8 1024.0) (= two-to-exp-p-minus-e-new8 8192.0))))
(assert (=> (and (<= 2048.0 abs-new8) (< abs-new8 4096.0)) (and (= two-to-exp-new8 2048.0) (= two-to-exp-p-minus-e-new8 4096.0))))
(assert (=> (and (<= 4096.0 abs-new8) (< abs-new8 8192.0)) (and (= two-to-exp-new8 4096.0) (= two-to-exp-p-minus-e-new8 2048.0))))
(assert (=> (and (<= 8192.0 abs-new8) (< abs-new8 16384.0)) (and (= two-to-exp-new8 8192.0) (= two-to-exp-p-minus-e-new8 1024.0))))
(assert (=> (and (<= 16384.0 abs-new8) (< abs-new8 32768.0)) (and (= two-to-exp-new8 16384.0) (= two-to-exp-p-minus-e-new8 512.0))))
(assert (=> (and (<= 32768.0 abs-new8) (< abs-new8 65536.0)) (and (= two-to-exp-new8 32768.0) (= two-to-exp-p-minus-e-new8 256.0))))
(assert (=> (and (<= 65536.0 abs-new8) (< abs-new8 131072.0)) (and (= two-to-exp-new8 65536.0) (= two-to-exp-p-minus-e-new8 128.0))))
(assert (=> (and (<= 131072.0 abs-new8) (< abs-new8 262144.0)) (and (= two-to-exp-new8 131072.0) (= two-to-exp-p-minus-e-new8 64.0))))
(assert (=> (and (<= 262144.0 abs-new8) (< abs-new8 524288.0)) (and (= two-to-exp-new8 262144.0) (= two-to-exp-p-minus-e-new8 32.0))))
(assert (=> (and (<= 524288.0 abs-new8) (< abs-new8 1048576.0)) (and (= two-to-exp-new8 524288.0) (= two-to-exp-p-minus-e-new8 16.0))))
(assert (=> (and (<= 1048576.0 abs-new8) (< abs-new8 2097152.0)) (and (= two-to-exp-new8 1048576.0) (= two-to-exp-p-minus-e-new8 8.0))))
(assert (=> (and (<= 2097152.0 abs-new8) (< abs-new8 4194304.0)) (and (= two-to-exp-new8 2097152.0) (= two-to-exp-p-minus-e-new8 4.0))))
(assert (=> (and (<= 4194304.0 abs-new8) (< abs-new8 8388608.0)) (and (= two-to-exp-new8 4194304.0) (= two-to-exp-p-minus-e-new8 2.0))))
(assert (=> (and (<= 8388608.0 abs-new8) (< abs-new8 16777216.0)) (and (= two-to-exp-new8 8388608.0) (= two-to-exp-p-minus-e-new8 1.0))))
(assert (=> (and (<= 16777216.0 abs-new8) (< abs-new8 33554432.0)) (and (= two-to-exp-new8 16777216.0) (= two-to-exp-p-minus-e-new8 0.5))))
(assert (=> (and (<= 33554432.0 abs-new8) (< abs-new8 67108864.0)) (and (= two-to-exp-new8 33554432.0) (= two-to-exp-p-minus-e-new8 0.25))))
(assert (=> (and (<= 67108864.0 abs-new8) (< abs-new8 134217728.0)) (and (= two-to-exp-new8 67108864.0) (= two-to-exp-p-minus-e-new8 0.125))))
(assert (=> (and (<= 134217728.0 abs-new8) (< abs-new8 268435456.0)) (and (= two-to-exp-new8 134217728.0) (= two-to-exp-p-minus-e-new8 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new8) (< abs-new8 536870912.0)) (and (= two-to-exp-new8 268435456.0) (= two-to-exp-p-minus-e-new8 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new8) (< abs-new8 1073741824.0)) (and (= two-to-exp-new8 536870912.0) (= two-to-exp-p-minus-e-new8 0.015625))))

(assert (= new8-real (+ new9 a4)))

;(assert (= new8  (* (/ (to_real (to_int (* (/ new8-real two-to-exp-new8) two-to-p))) two-to-p) two-to-exp-new8 )))
(assert (= (* two-to-exp-p-minus-e-new8 new8) (to_real (to_int (* new8-real two-to-exp-p-minus-e-new8)))))

(declare-const new7 Real)

(declare-const abs-new7 Real)
(assert (or (and (<= 1.0  new7) (< new7 1073741824.0)) (and (>= -1.0  new7) (> new7 -1073741824.0))))
(assert (=> (>= new7 0.0) (= abs-new7 new7)));added
(assert (=> (< new7 0.0) (= abs-new7 (- new7))));added
(declare-const new7-real Real)
(declare-const two-to-exp-new7 Real)
(declare-const two-to-exp-p-minus-e-new7 Real)
(assert (=> (and (<= 1.0 abs-new7) (< abs-new7 2.0)) (and (= two-to-exp-new7 1.0) (= two-to-exp-p-minus-e-new7 8388608.0))))
(assert (=> (and (<= 2.0 abs-new7) (< abs-new7 4.0)) (and (= two-to-exp-new7 2.0) (= two-to-exp-p-minus-e-new7 4194304.0))))
(assert (=> (and (<= 4.0 abs-new7) (< abs-new7 8.0)) (and (= two-to-exp-new7 4.0) (= two-to-exp-p-minus-e-new7 2097152.0))))
(assert (=> (and (<= 8.0 abs-new7) (< abs-new7 16.0)) (and (= two-to-exp-new7 8.0) (= two-to-exp-p-minus-e-new7 1048576.0))))
(assert (=> (and (<= 16.0 abs-new7) (< abs-new7 32.0)) (and (= two-to-exp-new7 16.0) (= two-to-exp-p-minus-e-new7 524288.0))))
(assert (=> (and (<= 32.0 abs-new7) (< abs-new7 64.0)) (and (= two-to-exp-new7 32.0) (= two-to-exp-p-minus-e-new7 262144.0))))
(assert (=> (and (<= 64.0 abs-new7) (< abs-new7 128.0)) (and (= two-to-exp-new7 64.0) (= two-to-exp-p-minus-e-new7 131072.0))))
(assert (=> (and (<= 128.0 abs-new7) (< abs-new7 256.0)) (and (= two-to-exp-new7 128.0) (= two-to-exp-p-minus-e-new7 65536.0))))
(assert (=> (and (<= 256.0 abs-new7) (< abs-new7 512.0)) (and (= two-to-exp-new7 256.0) (= two-to-exp-p-minus-e-new7 32768.0))))
(assert (=> (and (<= 512.0 abs-new7) (< abs-new7 1024.0)) (and (= two-to-exp-new7 512.0) (= two-to-exp-p-minus-e-new7 16384.0))))
(assert (=> (and (<= 1024.0 abs-new7) (< abs-new7 2048.0)) (and (= two-to-exp-new7 1024.0) (= two-to-exp-p-minus-e-new7 8192.0))))
(assert (=> (and (<= 2048.0 abs-new7) (< abs-new7 4096.0)) (and (= two-to-exp-new7 2048.0) (= two-to-exp-p-minus-e-new7 4096.0))))
(assert (=> (and (<= 4096.0 abs-new7) (< abs-new7 8192.0)) (and (= two-to-exp-new7 4096.0) (= two-to-exp-p-minus-e-new7 2048.0))))
(assert (=> (and (<= 8192.0 abs-new7) (< abs-new7 16384.0)) (and (= two-to-exp-new7 8192.0) (= two-to-exp-p-minus-e-new7 1024.0))))
(assert (=> (and (<= 16384.0 abs-new7) (< abs-new7 32768.0)) (and (= two-to-exp-new7 16384.0) (= two-to-exp-p-minus-e-new7 512.0))))
(assert (=> (and (<= 32768.0 abs-new7) (< abs-new7 65536.0)) (and (= two-to-exp-new7 32768.0) (= two-to-exp-p-minus-e-new7 256.0))))
(assert (=> (and (<= 65536.0 abs-new7) (< abs-new7 131072.0)) (and (= two-to-exp-new7 65536.0) (= two-to-exp-p-minus-e-new7 128.0))))
(assert (=> (and (<= 131072.0 abs-new7) (< abs-new7 262144.0)) (and (= two-to-exp-new7 131072.0) (= two-to-exp-p-minus-e-new7 64.0))))
(assert (=> (and (<= 262144.0 abs-new7) (< abs-new7 524288.0)) (and (= two-to-exp-new7 262144.0) (= two-to-exp-p-minus-e-new7 32.0))))
(assert (=> (and (<= 524288.0 abs-new7) (< abs-new7 1048576.0)) (and (= two-to-exp-new7 524288.0) (= two-to-exp-p-minus-e-new7 16.0))))
(assert (=> (and (<= 1048576.0 abs-new7) (< abs-new7 2097152.0)) (and (= two-to-exp-new7 1048576.0) (= two-to-exp-p-minus-e-new7 8.0))))
(assert (=> (and (<= 2097152.0 abs-new7) (< abs-new7 4194304.0)) (and (= two-to-exp-new7 2097152.0) (= two-to-exp-p-minus-e-new7 4.0))))
(assert (=> (and (<= 4194304.0 abs-new7) (< abs-new7 8388608.0)) (and (= two-to-exp-new7 4194304.0) (= two-to-exp-p-minus-e-new7 2.0))))
(assert (=> (and (<= 8388608.0 abs-new7) (< abs-new7 16777216.0)) (and (= two-to-exp-new7 8388608.0) (= two-to-exp-p-minus-e-new7 1.0))))
(assert (=> (and (<= 16777216.0 abs-new7) (< abs-new7 33554432.0)) (and (= two-to-exp-new7 16777216.0) (= two-to-exp-p-minus-e-new7 0.5))))
(assert (=> (and (<= 33554432.0 abs-new7) (< abs-new7 67108864.0)) (and (= two-to-exp-new7 33554432.0) (= two-to-exp-p-minus-e-new7 0.25))))
(assert (=> (and (<= 67108864.0 abs-new7) (< abs-new7 134217728.0)) (and (= two-to-exp-new7 67108864.0) (= two-to-exp-p-minus-e-new7 0.125))))
(assert (=> (and (<= 134217728.0 abs-new7) (< abs-new7 268435456.0)) (and (= two-to-exp-new7 134217728.0) (= two-to-exp-p-minus-e-new7 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new7) (< abs-new7 536870912.0)) (and (= two-to-exp-new7 268435456.0) (= two-to-exp-p-minus-e-new7 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new7) (< abs-new7 1073741824.0)) (and (= two-to-exp-new7 536870912.0) (= two-to-exp-p-minus-e-new7 0.015625))))

(assert (= new7-real (+ new8 a5)))

;(assert (= new7  (* (/ (to_real (to_int (* (/ new7-real two-to-exp-new7) two-to-p))) two-to-p) two-to-exp-new7 )))
(assert (= (* two-to-exp-p-minus-e-new7 new7) (to_real (to_int (* new7-real two-to-exp-p-minus-e-new7)))))

(declare-const new6 Real)

(declare-const abs-new6 Real)
(assert (or (and (<= 1.0  new6) (< new6 1073741824.0)) (and (>= -1.0  new6) (> new6 -1073741824.0))))
(assert (=> (>= new6 0.0) (= abs-new6 new6)));added
(assert (=> (< new6 0.0) (= abs-new6 (- new6))));added
(declare-const new6-real Real)
(declare-const two-to-exp-new6 Real)
(declare-const two-to-exp-p-minus-e-new6 Real)
(assert (=> (and (<= 1.0 abs-new6) (< abs-new6 2.0)) (and (= two-to-exp-new6 1.0) (= two-to-exp-p-minus-e-new6 8388608.0))))
(assert (=> (and (<= 2.0 abs-new6) (< abs-new6 4.0)) (and (= two-to-exp-new6 2.0) (= two-to-exp-p-minus-e-new6 4194304.0))))
(assert (=> (and (<= 4.0 abs-new6) (< abs-new6 8.0)) (and (= two-to-exp-new6 4.0) (= two-to-exp-p-minus-e-new6 2097152.0))))
(assert (=> (and (<= 8.0 abs-new6) (< abs-new6 16.0)) (and (= two-to-exp-new6 8.0) (= two-to-exp-p-minus-e-new6 1048576.0))))
(assert (=> (and (<= 16.0 abs-new6) (< abs-new6 32.0)) (and (= two-to-exp-new6 16.0) (= two-to-exp-p-minus-e-new6 524288.0))))
(assert (=> (and (<= 32.0 abs-new6) (< abs-new6 64.0)) (and (= two-to-exp-new6 32.0) (= two-to-exp-p-minus-e-new6 262144.0))))
(assert (=> (and (<= 64.0 abs-new6) (< abs-new6 128.0)) (and (= two-to-exp-new6 64.0) (= two-to-exp-p-minus-e-new6 131072.0))))
(assert (=> (and (<= 128.0 abs-new6) (< abs-new6 256.0)) (and (= two-to-exp-new6 128.0) (= two-to-exp-p-minus-e-new6 65536.0))))
(assert (=> (and (<= 256.0 abs-new6) (< abs-new6 512.0)) (and (= two-to-exp-new6 256.0) (= two-to-exp-p-minus-e-new6 32768.0))))
(assert (=> (and (<= 512.0 abs-new6) (< abs-new6 1024.0)) (and (= two-to-exp-new6 512.0) (= two-to-exp-p-minus-e-new6 16384.0))))
(assert (=> (and (<= 1024.0 abs-new6) (< abs-new6 2048.0)) (and (= two-to-exp-new6 1024.0) (= two-to-exp-p-minus-e-new6 8192.0))))
(assert (=> (and (<= 2048.0 abs-new6) (< abs-new6 4096.0)) (and (= two-to-exp-new6 2048.0) (= two-to-exp-p-minus-e-new6 4096.0))))
(assert (=> (and (<= 4096.0 abs-new6) (< abs-new6 8192.0)) (and (= two-to-exp-new6 4096.0) (= two-to-exp-p-minus-e-new6 2048.0))))
(assert (=> (and (<= 8192.0 abs-new6) (< abs-new6 16384.0)) (and (= two-to-exp-new6 8192.0) (= two-to-exp-p-minus-e-new6 1024.0))))
(assert (=> (and (<= 16384.0 abs-new6) (< abs-new6 32768.0)) (and (= two-to-exp-new6 16384.0) (= two-to-exp-p-minus-e-new6 512.0))))
(assert (=> (and (<= 32768.0 abs-new6) (< abs-new6 65536.0)) (and (= two-to-exp-new6 32768.0) (= two-to-exp-p-minus-e-new6 256.0))))
(assert (=> (and (<= 65536.0 abs-new6) (< abs-new6 131072.0)) (and (= two-to-exp-new6 65536.0) (= two-to-exp-p-minus-e-new6 128.0))))
(assert (=> (and (<= 131072.0 abs-new6) (< abs-new6 262144.0)) (and (= two-to-exp-new6 131072.0) (= two-to-exp-p-minus-e-new6 64.0))))
(assert (=> (and (<= 262144.0 abs-new6) (< abs-new6 524288.0)) (and (= two-to-exp-new6 262144.0) (= two-to-exp-p-minus-e-new6 32.0))))
(assert (=> (and (<= 524288.0 abs-new6) (< abs-new6 1048576.0)) (and (= two-to-exp-new6 524288.0) (= two-to-exp-p-minus-e-new6 16.0))))
(assert (=> (and (<= 1048576.0 abs-new6) (< abs-new6 2097152.0)) (and (= two-to-exp-new6 1048576.0) (= two-to-exp-p-minus-e-new6 8.0))))
(assert (=> (and (<= 2097152.0 abs-new6) (< abs-new6 4194304.0)) (and (= two-to-exp-new6 2097152.0) (= two-to-exp-p-minus-e-new6 4.0))))
(assert (=> (and (<= 4194304.0 abs-new6) (< abs-new6 8388608.0)) (and (= two-to-exp-new6 4194304.0) (= two-to-exp-p-minus-e-new6 2.0))))
(assert (=> (and (<= 8388608.0 abs-new6) (< abs-new6 16777216.0)) (and (= two-to-exp-new6 8388608.0) (= two-to-exp-p-minus-e-new6 1.0))))
(assert (=> (and (<= 16777216.0 abs-new6) (< abs-new6 33554432.0)) (and (= two-to-exp-new6 16777216.0) (= two-to-exp-p-minus-e-new6 0.5))))
(assert (=> (and (<= 33554432.0 abs-new6) (< abs-new6 67108864.0)) (and (= two-to-exp-new6 33554432.0) (= two-to-exp-p-minus-e-new6 0.25))))
(assert (=> (and (<= 67108864.0 abs-new6) (< abs-new6 134217728.0)) (and (= two-to-exp-new6 67108864.0) (= two-to-exp-p-minus-e-new6 0.125))))
(assert (=> (and (<= 134217728.0 abs-new6) (< abs-new6 268435456.0)) (and (= two-to-exp-new6 134217728.0) (= two-to-exp-p-minus-e-new6 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new6) (< abs-new6 536870912.0)) (and (= two-to-exp-new6 268435456.0) (= two-to-exp-p-minus-e-new6 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new6) (< abs-new6 1073741824.0)) (and (= two-to-exp-new6 536870912.0) (= two-to-exp-p-minus-e-new6 0.015625))))

(assert (= new6-real (+ new7 a6)))

;(assert (= new6  (* (/ (to_real (to_int (* (/ new6-real two-to-exp-new6) two-to-p))) two-to-p) two-to-exp-new6 )))
(assert (= (* two-to-exp-p-minus-e-new6 new6) (to_real (to_int (* new6-real two-to-exp-p-minus-e-new6)))))

(declare-const new5 Real)

(declare-const abs-new5 Real)
(assert (or (and (<= 1.0  new5) (< new5 1073741824.0)) (and (>= -1.0  new5) (> new5 -1073741824.0))))
(assert (=> (>= new5 0.0) (= abs-new5 new5)));added
(assert (=> (< new5 0.0) (= abs-new5 (- new5))));added
(declare-const new5-real Real)
(declare-const two-to-exp-new5 Real)
(declare-const two-to-exp-p-minus-e-new5 Real)
(assert (=> (and (<= 1.0 abs-new5) (< abs-new5 2.0)) (and (= two-to-exp-new5 1.0) (= two-to-exp-p-minus-e-new5 8388608.0))))
(assert (=> (and (<= 2.0 abs-new5) (< abs-new5 4.0)) (and (= two-to-exp-new5 2.0) (= two-to-exp-p-minus-e-new5 4194304.0))))
(assert (=> (and (<= 4.0 abs-new5) (< abs-new5 8.0)) (and (= two-to-exp-new5 4.0) (= two-to-exp-p-minus-e-new5 2097152.0))))
(assert (=> (and (<= 8.0 abs-new5) (< abs-new5 16.0)) (and (= two-to-exp-new5 8.0) (= two-to-exp-p-minus-e-new5 1048576.0))))
(assert (=> (and (<= 16.0 abs-new5) (< abs-new5 32.0)) (and (= two-to-exp-new5 16.0) (= two-to-exp-p-minus-e-new5 524288.0))))
(assert (=> (and (<= 32.0 abs-new5) (< abs-new5 64.0)) (and (= two-to-exp-new5 32.0) (= two-to-exp-p-minus-e-new5 262144.0))))
(assert (=> (and (<= 64.0 abs-new5) (< abs-new5 128.0)) (and (= two-to-exp-new5 64.0) (= two-to-exp-p-minus-e-new5 131072.0))))
(assert (=> (and (<= 128.0 abs-new5) (< abs-new5 256.0)) (and (= two-to-exp-new5 128.0) (= two-to-exp-p-minus-e-new5 65536.0))))
(assert (=> (and (<= 256.0 abs-new5) (< abs-new5 512.0)) (and (= two-to-exp-new5 256.0) (= two-to-exp-p-minus-e-new5 32768.0))))
(assert (=> (and (<= 512.0 abs-new5) (< abs-new5 1024.0)) (and (= two-to-exp-new5 512.0) (= two-to-exp-p-minus-e-new5 16384.0))))
(assert (=> (and (<= 1024.0 abs-new5) (< abs-new5 2048.0)) (and (= two-to-exp-new5 1024.0) (= two-to-exp-p-minus-e-new5 8192.0))))
(assert (=> (and (<= 2048.0 abs-new5) (< abs-new5 4096.0)) (and (= two-to-exp-new5 2048.0) (= two-to-exp-p-minus-e-new5 4096.0))))
(assert (=> (and (<= 4096.0 abs-new5) (< abs-new5 8192.0)) (and (= two-to-exp-new5 4096.0) (= two-to-exp-p-minus-e-new5 2048.0))))
(assert (=> (and (<= 8192.0 abs-new5) (< abs-new5 16384.0)) (and (= two-to-exp-new5 8192.0) (= two-to-exp-p-minus-e-new5 1024.0))))
(assert (=> (and (<= 16384.0 abs-new5) (< abs-new5 32768.0)) (and (= two-to-exp-new5 16384.0) (= two-to-exp-p-minus-e-new5 512.0))))
(assert (=> (and (<= 32768.0 abs-new5) (< abs-new5 65536.0)) (and (= two-to-exp-new5 32768.0) (= two-to-exp-p-minus-e-new5 256.0))))
(assert (=> (and (<= 65536.0 abs-new5) (< abs-new5 131072.0)) (and (= two-to-exp-new5 65536.0) (= two-to-exp-p-minus-e-new5 128.0))))
(assert (=> (and (<= 131072.0 abs-new5) (< abs-new5 262144.0)) (and (= two-to-exp-new5 131072.0) (= two-to-exp-p-minus-e-new5 64.0))))
(assert (=> (and (<= 262144.0 abs-new5) (< abs-new5 524288.0)) (and (= two-to-exp-new5 262144.0) (= two-to-exp-p-minus-e-new5 32.0))))
(assert (=> (and (<= 524288.0 abs-new5) (< abs-new5 1048576.0)) (and (= two-to-exp-new5 524288.0) (= two-to-exp-p-minus-e-new5 16.0))))
(assert (=> (and (<= 1048576.0 abs-new5) (< abs-new5 2097152.0)) (and (= two-to-exp-new5 1048576.0) (= two-to-exp-p-minus-e-new5 8.0))))
(assert (=> (and (<= 2097152.0 abs-new5) (< abs-new5 4194304.0)) (and (= two-to-exp-new5 2097152.0) (= two-to-exp-p-minus-e-new5 4.0))))
(assert (=> (and (<= 4194304.0 abs-new5) (< abs-new5 8388608.0)) (and (= two-to-exp-new5 4194304.0) (= two-to-exp-p-minus-e-new5 2.0))))
(assert (=> (and (<= 8388608.0 abs-new5) (< abs-new5 16777216.0)) (and (= two-to-exp-new5 8388608.0) (= two-to-exp-p-minus-e-new5 1.0))))
(assert (=> (and (<= 16777216.0 abs-new5) (< abs-new5 33554432.0)) (and (= two-to-exp-new5 16777216.0) (= two-to-exp-p-minus-e-new5 0.5))))
(assert (=> (and (<= 33554432.0 abs-new5) (< abs-new5 67108864.0)) (and (= two-to-exp-new5 33554432.0) (= two-to-exp-p-minus-e-new5 0.25))))
(assert (=> (and (<= 67108864.0 abs-new5) (< abs-new5 134217728.0)) (and (= two-to-exp-new5 67108864.0) (= two-to-exp-p-minus-e-new5 0.125))))
(assert (=> (and (<= 134217728.0 abs-new5) (< abs-new5 268435456.0)) (and (= two-to-exp-new5 134217728.0) (= two-to-exp-p-minus-e-new5 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new5) (< abs-new5 536870912.0)) (and (= two-to-exp-new5 268435456.0) (= two-to-exp-p-minus-e-new5 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new5) (< abs-new5 1073741824.0)) (and (= two-to-exp-new5 536870912.0) (= two-to-exp-p-minus-e-new5 0.015625))))

(assert (= new5-real (+ new6 a7)))

;(assert (= new5  (* (/ (to_real (to_int (* (/ new5-real two-to-exp-new5) two-to-p))) two-to-p) two-to-exp-new5 )))
(assert (= (* two-to-exp-p-minus-e-new5 new5) (to_real (to_int (* new5-real two-to-exp-p-minus-e-new5)))))

(declare-const new4 Real)

(declare-const abs-new4 Real)
(assert (or (and (<= 1.0  new4) (< new4 1073741824.0)) (and (>= -1.0  new4) (> new4 -1073741824.0))))
(assert (=> (>= new4 0.0) (= abs-new4 new4)));added
(assert (=> (< new4 0.0) (= abs-new4 (- new4))));added
(declare-const new4-real Real)
(declare-const two-to-exp-new4 Real)
(declare-const two-to-exp-p-minus-e-new4 Real)
(assert (=> (and (<= 1.0 abs-new4) (< abs-new4 2.0)) (and (= two-to-exp-new4 1.0) (= two-to-exp-p-minus-e-new4 8388608.0))))
(assert (=> (and (<= 2.0 abs-new4) (< abs-new4 4.0)) (and (= two-to-exp-new4 2.0) (= two-to-exp-p-minus-e-new4 4194304.0))))
(assert (=> (and (<= 4.0 abs-new4) (< abs-new4 8.0)) (and (= two-to-exp-new4 4.0) (= two-to-exp-p-minus-e-new4 2097152.0))))
(assert (=> (and (<= 8.0 abs-new4) (< abs-new4 16.0)) (and (= two-to-exp-new4 8.0) (= two-to-exp-p-minus-e-new4 1048576.0))))
(assert (=> (and (<= 16.0 abs-new4) (< abs-new4 32.0)) (and (= two-to-exp-new4 16.0) (= two-to-exp-p-minus-e-new4 524288.0))))
(assert (=> (and (<= 32.0 abs-new4) (< abs-new4 64.0)) (and (= two-to-exp-new4 32.0) (= two-to-exp-p-minus-e-new4 262144.0))))
(assert (=> (and (<= 64.0 abs-new4) (< abs-new4 128.0)) (and (= two-to-exp-new4 64.0) (= two-to-exp-p-minus-e-new4 131072.0))))
(assert (=> (and (<= 128.0 abs-new4) (< abs-new4 256.0)) (and (= two-to-exp-new4 128.0) (= two-to-exp-p-minus-e-new4 65536.0))))
(assert (=> (and (<= 256.0 abs-new4) (< abs-new4 512.0)) (and (= two-to-exp-new4 256.0) (= two-to-exp-p-minus-e-new4 32768.0))))
(assert (=> (and (<= 512.0 abs-new4) (< abs-new4 1024.0)) (and (= two-to-exp-new4 512.0) (= two-to-exp-p-minus-e-new4 16384.0))))
(assert (=> (and (<= 1024.0 abs-new4) (< abs-new4 2048.0)) (and (= two-to-exp-new4 1024.0) (= two-to-exp-p-minus-e-new4 8192.0))))
(assert (=> (and (<= 2048.0 abs-new4) (< abs-new4 4096.0)) (and (= two-to-exp-new4 2048.0) (= two-to-exp-p-minus-e-new4 4096.0))))
(assert (=> (and (<= 4096.0 abs-new4) (< abs-new4 8192.0)) (and (= two-to-exp-new4 4096.0) (= two-to-exp-p-minus-e-new4 2048.0))))
(assert (=> (and (<= 8192.0 abs-new4) (< abs-new4 16384.0)) (and (= two-to-exp-new4 8192.0) (= two-to-exp-p-minus-e-new4 1024.0))))
(assert (=> (and (<= 16384.0 abs-new4) (< abs-new4 32768.0)) (and (= two-to-exp-new4 16384.0) (= two-to-exp-p-minus-e-new4 512.0))))
(assert (=> (and (<= 32768.0 abs-new4) (< abs-new4 65536.0)) (and (= two-to-exp-new4 32768.0) (= two-to-exp-p-minus-e-new4 256.0))))
(assert (=> (and (<= 65536.0 abs-new4) (< abs-new4 131072.0)) (and (= two-to-exp-new4 65536.0) (= two-to-exp-p-minus-e-new4 128.0))))
(assert (=> (and (<= 131072.0 abs-new4) (< abs-new4 262144.0)) (and (= two-to-exp-new4 131072.0) (= two-to-exp-p-minus-e-new4 64.0))))
(assert (=> (and (<= 262144.0 abs-new4) (< abs-new4 524288.0)) (and (= two-to-exp-new4 262144.0) (= two-to-exp-p-minus-e-new4 32.0))))
(assert (=> (and (<= 524288.0 abs-new4) (< abs-new4 1048576.0)) (and (= two-to-exp-new4 524288.0) (= two-to-exp-p-minus-e-new4 16.0))))
(assert (=> (and (<= 1048576.0 abs-new4) (< abs-new4 2097152.0)) (and (= two-to-exp-new4 1048576.0) (= two-to-exp-p-minus-e-new4 8.0))))
(assert (=> (and (<= 2097152.0 abs-new4) (< abs-new4 4194304.0)) (and (= two-to-exp-new4 2097152.0) (= two-to-exp-p-minus-e-new4 4.0))))
(assert (=> (and (<= 4194304.0 abs-new4) (< abs-new4 8388608.0)) (and (= two-to-exp-new4 4194304.0) (= two-to-exp-p-minus-e-new4 2.0))))
(assert (=> (and (<= 8388608.0 abs-new4) (< abs-new4 16777216.0)) (and (= two-to-exp-new4 8388608.0) (= two-to-exp-p-minus-e-new4 1.0))))
(assert (=> (and (<= 16777216.0 abs-new4) (< abs-new4 33554432.0)) (and (= two-to-exp-new4 16777216.0) (= two-to-exp-p-minus-e-new4 0.5))))
(assert (=> (and (<= 33554432.0 abs-new4) (< abs-new4 67108864.0)) (and (= two-to-exp-new4 33554432.0) (= two-to-exp-p-minus-e-new4 0.25))))
(assert (=> (and (<= 67108864.0 abs-new4) (< abs-new4 134217728.0)) (and (= two-to-exp-new4 67108864.0) (= two-to-exp-p-minus-e-new4 0.125))))
(assert (=> (and (<= 134217728.0 abs-new4) (< abs-new4 268435456.0)) (and (= two-to-exp-new4 134217728.0) (= two-to-exp-p-minus-e-new4 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new4) (< abs-new4 536870912.0)) (and (= two-to-exp-new4 268435456.0) (= two-to-exp-p-minus-e-new4 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new4) (< abs-new4 1073741824.0)) (and (= two-to-exp-new4 536870912.0) (= two-to-exp-p-minus-e-new4 0.015625))))

(assert (= new4-real (+ new5 a8)))

;(assert (= new4  (* (/ (to_real (to_int (* (/ new4-real two-to-exp-new4) two-to-p))) two-to-p) two-to-exp-new4 )))
(assert (= (* two-to-exp-p-minus-e-new4 new4) (to_real (to_int (* new4-real two-to-exp-p-minus-e-new4)))))

(declare-const new3 Real)

(declare-const abs-new3 Real)
(assert (or (and (<= 1.0  new3) (< new3 1073741824.0)) (and (>= -1.0  new3) (> new3 -1073741824.0))))
(assert (=> (>= new3 0.0) (= abs-new3 new3)));added
(assert (=> (< new3 0.0) (= abs-new3 (- new3))));added
(declare-const new3-real Real)
(declare-const two-to-exp-new3 Real)
(declare-const two-to-exp-p-minus-e-new3 Real)
(assert (=> (and (<= 1.0 abs-new3) (< abs-new3 2.0)) (and (= two-to-exp-new3 1.0) (= two-to-exp-p-minus-e-new3 8388608.0))))
(assert (=> (and (<= 2.0 abs-new3) (< abs-new3 4.0)) (and (= two-to-exp-new3 2.0) (= two-to-exp-p-minus-e-new3 4194304.0))))
(assert (=> (and (<= 4.0 abs-new3) (< abs-new3 8.0)) (and (= two-to-exp-new3 4.0) (= two-to-exp-p-minus-e-new3 2097152.0))))
(assert (=> (and (<= 8.0 abs-new3) (< abs-new3 16.0)) (and (= two-to-exp-new3 8.0) (= two-to-exp-p-minus-e-new3 1048576.0))))
(assert (=> (and (<= 16.0 abs-new3) (< abs-new3 32.0)) (and (= two-to-exp-new3 16.0) (= two-to-exp-p-minus-e-new3 524288.0))))
(assert (=> (and (<= 32.0 abs-new3) (< abs-new3 64.0)) (and (= two-to-exp-new3 32.0) (= two-to-exp-p-minus-e-new3 262144.0))))
(assert (=> (and (<= 64.0 abs-new3) (< abs-new3 128.0)) (and (= two-to-exp-new3 64.0) (= two-to-exp-p-minus-e-new3 131072.0))))
(assert (=> (and (<= 128.0 abs-new3) (< abs-new3 256.0)) (and (= two-to-exp-new3 128.0) (= two-to-exp-p-minus-e-new3 65536.0))))
(assert (=> (and (<= 256.0 abs-new3) (< abs-new3 512.0)) (and (= two-to-exp-new3 256.0) (= two-to-exp-p-minus-e-new3 32768.0))))
(assert (=> (and (<= 512.0 abs-new3) (< abs-new3 1024.0)) (and (= two-to-exp-new3 512.0) (= two-to-exp-p-minus-e-new3 16384.0))))
(assert (=> (and (<= 1024.0 abs-new3) (< abs-new3 2048.0)) (and (= two-to-exp-new3 1024.0) (= two-to-exp-p-minus-e-new3 8192.0))))
(assert (=> (and (<= 2048.0 abs-new3) (< abs-new3 4096.0)) (and (= two-to-exp-new3 2048.0) (= two-to-exp-p-minus-e-new3 4096.0))))
(assert (=> (and (<= 4096.0 abs-new3) (< abs-new3 8192.0)) (and (= two-to-exp-new3 4096.0) (= two-to-exp-p-minus-e-new3 2048.0))))
(assert (=> (and (<= 8192.0 abs-new3) (< abs-new3 16384.0)) (and (= two-to-exp-new3 8192.0) (= two-to-exp-p-minus-e-new3 1024.0))))
(assert (=> (and (<= 16384.0 abs-new3) (< abs-new3 32768.0)) (and (= two-to-exp-new3 16384.0) (= two-to-exp-p-minus-e-new3 512.0))))
(assert (=> (and (<= 32768.0 abs-new3) (< abs-new3 65536.0)) (and (= two-to-exp-new3 32768.0) (= two-to-exp-p-minus-e-new3 256.0))))
(assert (=> (and (<= 65536.0 abs-new3) (< abs-new3 131072.0)) (and (= two-to-exp-new3 65536.0) (= two-to-exp-p-minus-e-new3 128.0))))
(assert (=> (and (<= 131072.0 abs-new3) (< abs-new3 262144.0)) (and (= two-to-exp-new3 131072.0) (= two-to-exp-p-minus-e-new3 64.0))))
(assert (=> (and (<= 262144.0 abs-new3) (< abs-new3 524288.0)) (and (= two-to-exp-new3 262144.0) (= two-to-exp-p-minus-e-new3 32.0))))
(assert (=> (and (<= 524288.0 abs-new3) (< abs-new3 1048576.0)) (and (= two-to-exp-new3 524288.0) (= two-to-exp-p-minus-e-new3 16.0))))
(assert (=> (and (<= 1048576.0 abs-new3) (< abs-new3 2097152.0)) (and (= two-to-exp-new3 1048576.0) (= two-to-exp-p-minus-e-new3 8.0))))
(assert (=> (and (<= 2097152.0 abs-new3) (< abs-new3 4194304.0)) (and (= two-to-exp-new3 2097152.0) (= two-to-exp-p-minus-e-new3 4.0))))
(assert (=> (and (<= 4194304.0 abs-new3) (< abs-new3 8388608.0)) (and (= two-to-exp-new3 4194304.0) (= two-to-exp-p-minus-e-new3 2.0))))
(assert (=> (and (<= 8388608.0 abs-new3) (< abs-new3 16777216.0)) (and (= two-to-exp-new3 8388608.0) (= two-to-exp-p-minus-e-new3 1.0))))
(assert (=> (and (<= 16777216.0 abs-new3) (< abs-new3 33554432.0)) (and (= two-to-exp-new3 16777216.0) (= two-to-exp-p-minus-e-new3 0.5))))
(assert (=> (and (<= 33554432.0 abs-new3) (< abs-new3 67108864.0)) (and (= two-to-exp-new3 33554432.0) (= two-to-exp-p-minus-e-new3 0.25))))
(assert (=> (and (<= 67108864.0 abs-new3) (< abs-new3 134217728.0)) (and (= two-to-exp-new3 67108864.0) (= two-to-exp-p-minus-e-new3 0.125))))
(assert (=> (and (<= 134217728.0 abs-new3) (< abs-new3 268435456.0)) (and (= two-to-exp-new3 134217728.0) (= two-to-exp-p-minus-e-new3 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new3) (< abs-new3 536870912.0)) (and (= two-to-exp-new3 268435456.0) (= two-to-exp-p-minus-e-new3 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new3) (< abs-new3 1073741824.0)) (and (= two-to-exp-new3 536870912.0) (= two-to-exp-p-minus-e-new3 0.015625))))

(assert (= new3-real (+ new4 a9)))

;(assert (= new3  (* (/ (to_real (to_int (* (/ new3-real two-to-exp-new3) two-to-p))) two-to-p) two-to-exp-new3 )))
(assert (= (* two-to-exp-p-minus-e-new3 new3) (to_real (to_int (* new3-real two-to-exp-p-minus-e-new3)))))

(declare-const new2 Real)

(declare-const abs-new2 Real)
(assert (or (and (<= 1.0  new2) (< new2 1073741824.0)) (and (>= -1.0  new2) (> new2 -1073741824.0))))
(assert (=> (>= new2 0.0) (= abs-new2 new2)));added
(assert (=> (< new2 0.0) (= abs-new2 (- new2))));added
(declare-const new2-real Real)
(declare-const two-to-exp-new2 Real)
(declare-const two-to-exp-p-minus-e-new2 Real)
(assert (=> (and (<= 1.0 abs-new2) (< abs-new2 2.0)) (and (= two-to-exp-new2 1.0) (= two-to-exp-p-minus-e-new2 8388608.0))))
(assert (=> (and (<= 2.0 abs-new2) (< abs-new2 4.0)) (and (= two-to-exp-new2 2.0) (= two-to-exp-p-minus-e-new2 4194304.0))))
(assert (=> (and (<= 4.0 abs-new2) (< abs-new2 8.0)) (and (= two-to-exp-new2 4.0) (= two-to-exp-p-minus-e-new2 2097152.0))))
(assert (=> (and (<= 8.0 abs-new2) (< abs-new2 16.0)) (and (= two-to-exp-new2 8.0) (= two-to-exp-p-minus-e-new2 1048576.0))))
(assert (=> (and (<= 16.0 abs-new2) (< abs-new2 32.0)) (and (= two-to-exp-new2 16.0) (= two-to-exp-p-minus-e-new2 524288.0))))
(assert (=> (and (<= 32.0 abs-new2) (< abs-new2 64.0)) (and (= two-to-exp-new2 32.0) (= two-to-exp-p-minus-e-new2 262144.0))))
(assert (=> (and (<= 64.0 abs-new2) (< abs-new2 128.0)) (and (= two-to-exp-new2 64.0) (= two-to-exp-p-minus-e-new2 131072.0))))
(assert (=> (and (<= 128.0 abs-new2) (< abs-new2 256.0)) (and (= two-to-exp-new2 128.0) (= two-to-exp-p-minus-e-new2 65536.0))))
(assert (=> (and (<= 256.0 abs-new2) (< abs-new2 512.0)) (and (= two-to-exp-new2 256.0) (= two-to-exp-p-minus-e-new2 32768.0))))
(assert (=> (and (<= 512.0 abs-new2) (< abs-new2 1024.0)) (and (= two-to-exp-new2 512.0) (= two-to-exp-p-minus-e-new2 16384.0))))
(assert (=> (and (<= 1024.0 abs-new2) (< abs-new2 2048.0)) (and (= two-to-exp-new2 1024.0) (= two-to-exp-p-minus-e-new2 8192.0))))
(assert (=> (and (<= 2048.0 abs-new2) (< abs-new2 4096.0)) (and (= two-to-exp-new2 2048.0) (= two-to-exp-p-minus-e-new2 4096.0))))
(assert (=> (and (<= 4096.0 abs-new2) (< abs-new2 8192.0)) (and (= two-to-exp-new2 4096.0) (= two-to-exp-p-minus-e-new2 2048.0))))
(assert (=> (and (<= 8192.0 abs-new2) (< abs-new2 16384.0)) (and (= two-to-exp-new2 8192.0) (= two-to-exp-p-minus-e-new2 1024.0))))
(assert (=> (and (<= 16384.0 abs-new2) (< abs-new2 32768.0)) (and (= two-to-exp-new2 16384.0) (= two-to-exp-p-minus-e-new2 512.0))))
(assert (=> (and (<= 32768.0 abs-new2) (< abs-new2 65536.0)) (and (= two-to-exp-new2 32768.0) (= two-to-exp-p-minus-e-new2 256.0))))
(assert (=> (and (<= 65536.0 abs-new2) (< abs-new2 131072.0)) (and (= two-to-exp-new2 65536.0) (= two-to-exp-p-minus-e-new2 128.0))))
(assert (=> (and (<= 131072.0 abs-new2) (< abs-new2 262144.0)) (and (= two-to-exp-new2 131072.0) (= two-to-exp-p-minus-e-new2 64.0))))
(assert (=> (and (<= 262144.0 abs-new2) (< abs-new2 524288.0)) (and (= two-to-exp-new2 262144.0) (= two-to-exp-p-minus-e-new2 32.0))))
(assert (=> (and (<= 524288.0 abs-new2) (< abs-new2 1048576.0)) (and (= two-to-exp-new2 524288.0) (= two-to-exp-p-minus-e-new2 16.0))))
(assert (=> (and (<= 1048576.0 abs-new2) (< abs-new2 2097152.0)) (and (= two-to-exp-new2 1048576.0) (= two-to-exp-p-minus-e-new2 8.0))))
(assert (=> (and (<= 2097152.0 abs-new2) (< abs-new2 4194304.0)) (and (= two-to-exp-new2 2097152.0) (= two-to-exp-p-minus-e-new2 4.0))))
(assert (=> (and (<= 4194304.0 abs-new2) (< abs-new2 8388608.0)) (and (= two-to-exp-new2 4194304.0) (= two-to-exp-p-minus-e-new2 2.0))))
(assert (=> (and (<= 8388608.0 abs-new2) (< abs-new2 16777216.0)) (and (= two-to-exp-new2 8388608.0) (= two-to-exp-p-minus-e-new2 1.0))))
(assert (=> (and (<= 16777216.0 abs-new2) (< abs-new2 33554432.0)) (and (= two-to-exp-new2 16777216.0) (= two-to-exp-p-minus-e-new2 0.5))))
(assert (=> (and (<= 33554432.0 abs-new2) (< abs-new2 67108864.0)) (and (= two-to-exp-new2 33554432.0) (= two-to-exp-p-minus-e-new2 0.25))))
(assert (=> (and (<= 67108864.0 abs-new2) (< abs-new2 134217728.0)) (and (= two-to-exp-new2 67108864.0) (= two-to-exp-p-minus-e-new2 0.125))))
(assert (=> (and (<= 134217728.0 abs-new2) (< abs-new2 268435456.0)) (and (= two-to-exp-new2 134217728.0) (= two-to-exp-p-minus-e-new2 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new2) (< abs-new2 536870912.0)) (and (= two-to-exp-new2 268435456.0) (= two-to-exp-p-minus-e-new2 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new2) (< abs-new2 1073741824.0)) (and (= two-to-exp-new2 536870912.0) (= two-to-exp-p-minus-e-new2 0.015625))))

(assert (= new2-real (+ new3 a10)))

;(assert (= new2  (* (/ (to_real (to_int (* (/ new2-real two-to-exp-new2) two-to-p))) two-to-p) two-to-exp-new2 )))
(assert (= (* two-to-exp-p-minus-e-new2 new2) (to_real (to_int (* new2-real two-to-exp-p-minus-e-new2)))))

(declare-const new1 Real)

(declare-const abs-new1 Real)
(assert (or (and (<= 1.0  new1) (< new1 1073741824.0)) (and (>= -1.0  new1) (> new1 -1073741824.0))))
(assert (=> (>= new1 0.0) (= abs-new1 new1)));added
(assert (=> (< new1 0.0) (= abs-new1 (- new1))));added
(declare-const new1-real Real)
(declare-const two-to-exp-new1 Real)
(declare-const two-to-exp-p-minus-e-new1 Real)
(assert (=> (and (<= 1.0 abs-new1) (< abs-new1 2.0)) (and (= two-to-exp-new1 1.0) (= two-to-exp-p-minus-e-new1 8388608.0))))
(assert (=> (and (<= 2.0 abs-new1) (< abs-new1 4.0)) (and (= two-to-exp-new1 2.0) (= two-to-exp-p-minus-e-new1 4194304.0))))
(assert (=> (and (<= 4.0 abs-new1) (< abs-new1 8.0)) (and (= two-to-exp-new1 4.0) (= two-to-exp-p-minus-e-new1 2097152.0))))
(assert (=> (and (<= 8.0 abs-new1) (< abs-new1 16.0)) (and (= two-to-exp-new1 8.0) (= two-to-exp-p-minus-e-new1 1048576.0))))
(assert (=> (and (<= 16.0 abs-new1) (< abs-new1 32.0)) (and (= two-to-exp-new1 16.0) (= two-to-exp-p-minus-e-new1 524288.0))))
(assert (=> (and (<= 32.0 abs-new1) (< abs-new1 64.0)) (and (= two-to-exp-new1 32.0) (= two-to-exp-p-minus-e-new1 262144.0))))
(assert (=> (and (<= 64.0 abs-new1) (< abs-new1 128.0)) (and (= two-to-exp-new1 64.0) (= two-to-exp-p-minus-e-new1 131072.0))))
(assert (=> (and (<= 128.0 abs-new1) (< abs-new1 256.0)) (and (= two-to-exp-new1 128.0) (= two-to-exp-p-minus-e-new1 65536.0))))
(assert (=> (and (<= 256.0 abs-new1) (< abs-new1 512.0)) (and (= two-to-exp-new1 256.0) (= two-to-exp-p-minus-e-new1 32768.0))))
(assert (=> (and (<= 512.0 abs-new1) (< abs-new1 1024.0)) (and (= two-to-exp-new1 512.0) (= two-to-exp-p-minus-e-new1 16384.0))))
(assert (=> (and (<= 1024.0 abs-new1) (< abs-new1 2048.0)) (and (= two-to-exp-new1 1024.0) (= two-to-exp-p-minus-e-new1 8192.0))))
(assert (=> (and (<= 2048.0 abs-new1) (< abs-new1 4096.0)) (and (= two-to-exp-new1 2048.0) (= two-to-exp-p-minus-e-new1 4096.0))))
(assert (=> (and (<= 4096.0 abs-new1) (< abs-new1 8192.0)) (and (= two-to-exp-new1 4096.0) (= two-to-exp-p-minus-e-new1 2048.0))))
(assert (=> (and (<= 8192.0 abs-new1) (< abs-new1 16384.0)) (and (= two-to-exp-new1 8192.0) (= two-to-exp-p-minus-e-new1 1024.0))))
(assert (=> (and (<= 16384.0 abs-new1) (< abs-new1 32768.0)) (and (= two-to-exp-new1 16384.0) (= two-to-exp-p-minus-e-new1 512.0))))
(assert (=> (and (<= 32768.0 abs-new1) (< abs-new1 65536.0)) (and (= two-to-exp-new1 32768.0) (= two-to-exp-p-minus-e-new1 256.0))))
(assert (=> (and (<= 65536.0 abs-new1) (< abs-new1 131072.0)) (and (= two-to-exp-new1 65536.0) (= two-to-exp-p-minus-e-new1 128.0))))
(assert (=> (and (<= 131072.0 abs-new1) (< abs-new1 262144.0)) (and (= two-to-exp-new1 131072.0) (= two-to-exp-p-minus-e-new1 64.0))))
(assert (=> (and (<= 262144.0 abs-new1) (< abs-new1 524288.0)) (and (= two-to-exp-new1 262144.0) (= two-to-exp-p-minus-e-new1 32.0))))
(assert (=> (and (<= 524288.0 abs-new1) (< abs-new1 1048576.0)) (and (= two-to-exp-new1 524288.0) (= two-to-exp-p-minus-e-new1 16.0))))
(assert (=> (and (<= 1048576.0 abs-new1) (< abs-new1 2097152.0)) (and (= two-to-exp-new1 1048576.0) (= two-to-exp-p-minus-e-new1 8.0))))
(assert (=> (and (<= 2097152.0 abs-new1) (< abs-new1 4194304.0)) (and (= two-to-exp-new1 2097152.0) (= two-to-exp-p-minus-e-new1 4.0))))
(assert (=> (and (<= 4194304.0 abs-new1) (< abs-new1 8388608.0)) (and (= two-to-exp-new1 4194304.0) (= two-to-exp-p-minus-e-new1 2.0))))
(assert (=> (and (<= 8388608.0 abs-new1) (< abs-new1 16777216.0)) (and (= two-to-exp-new1 8388608.0) (= two-to-exp-p-minus-e-new1 1.0))))
(assert (=> (and (<= 16777216.0 abs-new1) (< abs-new1 33554432.0)) (and (= two-to-exp-new1 16777216.0) (= two-to-exp-p-minus-e-new1 0.5))))
(assert (=> (and (<= 33554432.0 abs-new1) (< abs-new1 67108864.0)) (and (= two-to-exp-new1 33554432.0) (= two-to-exp-p-minus-e-new1 0.25))))
(assert (=> (and (<= 67108864.0 abs-new1) (< abs-new1 134217728.0)) (and (= two-to-exp-new1 67108864.0) (= two-to-exp-p-minus-e-new1 0.125))))
(assert (=> (and (<= 134217728.0 abs-new1) (< abs-new1 268435456.0)) (and (= two-to-exp-new1 134217728.0) (= two-to-exp-p-minus-e-new1 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new1) (< abs-new1 536870912.0)) (and (= two-to-exp-new1 268435456.0) (= two-to-exp-p-minus-e-new1 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new1) (< abs-new1 1073741824.0)) (and (= two-to-exp-new1 536870912.0) (= two-to-exp-p-minus-e-new1 0.015625))))

(assert (= new1-real (+ new2 a11)))

;(assert (= new1  (* (/ (to_real (to_int (* (/ new1-real two-to-exp-new1) two-to-p))) two-to-p) two-to-exp-new1 )))
(assert (= (* two-to-exp-p-minus-e-new1 new1) (to_real (to_int (* new1-real two-to-exp-p-minus-e-new1)))))

(declare-const new Real)

(declare-const abs-new Real)
(assert (or (and (<= 1.0  new) (< new 1073741824.0)) (and (>= -1.0  new) (> new -1073741824.0))))
(assert (=> (>= new 0.0) (= abs-new new)));added
(assert (=> (< new 0.0) (= abs-new (- new))));added
(declare-const new-real Real)
(declare-const two-to-exp-new Real)
(declare-const two-to-exp-p-minus-e-new Real)
(assert (=> (and (<= 1.0 abs-new) (< abs-new 2.0)) (and (= two-to-exp-new 1.0) (= two-to-exp-p-minus-e-new 8388608.0))))
(assert (=> (and (<= 2.0 abs-new) (< abs-new 4.0)) (and (= two-to-exp-new 2.0) (= two-to-exp-p-minus-e-new 4194304.0))))
(assert (=> (and (<= 4.0 abs-new) (< abs-new 8.0)) (and (= two-to-exp-new 4.0) (= two-to-exp-p-minus-e-new 2097152.0))))
(assert (=> (and (<= 8.0 abs-new) (< abs-new 16.0)) (and (= two-to-exp-new 8.0) (= two-to-exp-p-minus-e-new 1048576.0))))
(assert (=> (and (<= 16.0 abs-new) (< abs-new 32.0)) (and (= two-to-exp-new 16.0) (= two-to-exp-p-minus-e-new 524288.0))))
(assert (=> (and (<= 32.0 abs-new) (< abs-new 64.0)) (and (= two-to-exp-new 32.0) (= two-to-exp-p-minus-e-new 262144.0))))
(assert (=> (and (<= 64.0 abs-new) (< abs-new 128.0)) (and (= two-to-exp-new 64.0) (= two-to-exp-p-minus-e-new 131072.0))))
(assert (=> (and (<= 128.0 abs-new) (< abs-new 256.0)) (and (= two-to-exp-new 128.0) (= two-to-exp-p-minus-e-new 65536.0))))
(assert (=> (and (<= 256.0 abs-new) (< abs-new 512.0)) (and (= two-to-exp-new 256.0) (= two-to-exp-p-minus-e-new 32768.0))))
(assert (=> (and (<= 512.0 abs-new) (< abs-new 1024.0)) (and (= two-to-exp-new 512.0) (= two-to-exp-p-minus-e-new 16384.0))))
(assert (=> (and (<= 1024.0 abs-new) (< abs-new 2048.0)) (and (= two-to-exp-new 1024.0) (= two-to-exp-p-minus-e-new 8192.0))))
(assert (=> (and (<= 2048.0 abs-new) (< abs-new 4096.0)) (and (= two-to-exp-new 2048.0) (= two-to-exp-p-minus-e-new 4096.0))))
(assert (=> (and (<= 4096.0 abs-new) (< abs-new 8192.0)) (and (= two-to-exp-new 4096.0) (= two-to-exp-p-minus-e-new 2048.0))))
(assert (=> (and (<= 8192.0 abs-new) (< abs-new 16384.0)) (and (= two-to-exp-new 8192.0) (= two-to-exp-p-minus-e-new 1024.0))))
(assert (=> (and (<= 16384.0 abs-new) (< abs-new 32768.0)) (and (= two-to-exp-new 16384.0) (= two-to-exp-p-minus-e-new 512.0))))
(assert (=> (and (<= 32768.0 abs-new) (< abs-new 65536.0)) (and (= two-to-exp-new 32768.0) (= two-to-exp-p-minus-e-new 256.0))))
(assert (=> (and (<= 65536.0 abs-new) (< abs-new 131072.0)) (and (= two-to-exp-new 65536.0) (= two-to-exp-p-minus-e-new 128.0))))
(assert (=> (and (<= 131072.0 abs-new) (< abs-new 262144.0)) (and (= two-to-exp-new 131072.0) (= two-to-exp-p-minus-e-new 64.0))))
(assert (=> (and (<= 262144.0 abs-new) (< abs-new 524288.0)) (and (= two-to-exp-new 262144.0) (= two-to-exp-p-minus-e-new 32.0))))
(assert (=> (and (<= 524288.0 abs-new) (< abs-new 1048576.0)) (and (= two-to-exp-new 524288.0) (= two-to-exp-p-minus-e-new 16.0))))
(assert (=> (and (<= 1048576.0 abs-new) (< abs-new 2097152.0)) (and (= two-to-exp-new 1048576.0) (= two-to-exp-p-minus-e-new 8.0))))
(assert (=> (and (<= 2097152.0 abs-new) (< abs-new 4194304.0)) (and (= two-to-exp-new 2097152.0) (= two-to-exp-p-minus-e-new 4.0))))
(assert (=> (and (<= 4194304.0 abs-new) (< abs-new 8388608.0)) (and (= two-to-exp-new 4194304.0) (= two-to-exp-p-minus-e-new 2.0))))
(assert (=> (and (<= 8388608.0 abs-new) (< abs-new 16777216.0)) (and (= two-to-exp-new 8388608.0) (= two-to-exp-p-minus-e-new 1.0))))
(assert (=> (and (<= 16777216.0 abs-new) (< abs-new 33554432.0)) (and (= two-to-exp-new 16777216.0) (= two-to-exp-p-minus-e-new 0.5))))
(assert (=> (and (<= 33554432.0 abs-new) (< abs-new 67108864.0)) (and (= two-to-exp-new 33554432.0) (= two-to-exp-p-minus-e-new 0.25))))
(assert (=> (and (<= 67108864.0 abs-new) (< abs-new 134217728.0)) (and (= two-to-exp-new 67108864.0) (= two-to-exp-p-minus-e-new 0.125))))
(assert (=> (and (<= 134217728.0 abs-new) (< abs-new 268435456.0)) (and (= two-to-exp-new 134217728.0) (= two-to-exp-p-minus-e-new 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new) (< abs-new 536870912.0)) (and (= two-to-exp-new 268435456.0) (= two-to-exp-p-minus-e-new 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new) (< abs-new 1073741824.0)) (and (= two-to-exp-new 536870912.0) (= two-to-exp-p-minus-e-new 0.015625))))

(assert (= new-real (+ new1 a12)))

;(assert (= new  (* (/ (to_real (to_int (* (/ new-real two-to-exp-new) two-to-p))) two-to-p) two-to-exp-new )))
(assert (= (* two-to-exp-p-minus-e-new new) (to_real (to_int (* new-real two-to-exp-p-minus-e-new)))))

(declare-const new16 Real)

(declare-const abs-new16 Real)
(assert (or (and (<= 1.0  new16) (< new16 1073741824.0)) (and (>= -1.0  new16) (> new16 -1073741824.0))))
(assert (=> (>= new16 0.0) (= abs-new16 new16)));added
(assert (=> (< new16 0.0) (= abs-new16 (- new16))));added
(declare-const new16-real Real)
(declare-const two-to-exp-new16 Real)
(declare-const two-to-exp-p-minus-e-new16 Real)
(assert (=> (and (<= 1.0 abs-new16) (< abs-new16 2.0)) (and (= two-to-exp-new16 1.0) (= two-to-exp-p-minus-e-new16 8388608.0))))
(assert (=> (and (<= 2.0 abs-new16) (< abs-new16 4.0)) (and (= two-to-exp-new16 2.0) (= two-to-exp-p-minus-e-new16 4194304.0))))
(assert (=> (and (<= 4.0 abs-new16) (< abs-new16 8.0)) (and (= two-to-exp-new16 4.0) (= two-to-exp-p-minus-e-new16 2097152.0))))
(assert (=> (and (<= 8.0 abs-new16) (< abs-new16 16.0)) (and (= two-to-exp-new16 8.0) (= two-to-exp-p-minus-e-new16 1048576.0))))
(assert (=> (and (<= 16.0 abs-new16) (< abs-new16 32.0)) (and (= two-to-exp-new16 16.0) (= two-to-exp-p-minus-e-new16 524288.0))))
(assert (=> (and (<= 32.0 abs-new16) (< abs-new16 64.0)) (and (= two-to-exp-new16 32.0) (= two-to-exp-p-minus-e-new16 262144.0))))
(assert (=> (and (<= 64.0 abs-new16) (< abs-new16 128.0)) (and (= two-to-exp-new16 64.0) (= two-to-exp-p-minus-e-new16 131072.0))))
(assert (=> (and (<= 128.0 abs-new16) (< abs-new16 256.0)) (and (= two-to-exp-new16 128.0) (= two-to-exp-p-minus-e-new16 65536.0))))
(assert (=> (and (<= 256.0 abs-new16) (< abs-new16 512.0)) (and (= two-to-exp-new16 256.0) (= two-to-exp-p-minus-e-new16 32768.0))))
(assert (=> (and (<= 512.0 abs-new16) (< abs-new16 1024.0)) (and (= two-to-exp-new16 512.0) (= two-to-exp-p-minus-e-new16 16384.0))))
(assert (=> (and (<= 1024.0 abs-new16) (< abs-new16 2048.0)) (and (= two-to-exp-new16 1024.0) (= two-to-exp-p-minus-e-new16 8192.0))))
(assert (=> (and (<= 2048.0 abs-new16) (< abs-new16 4096.0)) (and (= two-to-exp-new16 2048.0) (= two-to-exp-p-minus-e-new16 4096.0))))
(assert (=> (and (<= 4096.0 abs-new16) (< abs-new16 8192.0)) (and (= two-to-exp-new16 4096.0) (= two-to-exp-p-minus-e-new16 2048.0))))
(assert (=> (and (<= 8192.0 abs-new16) (< abs-new16 16384.0)) (and (= two-to-exp-new16 8192.0) (= two-to-exp-p-minus-e-new16 1024.0))))
(assert (=> (and (<= 16384.0 abs-new16) (< abs-new16 32768.0)) (and (= two-to-exp-new16 16384.0) (= two-to-exp-p-minus-e-new16 512.0))))
(assert (=> (and (<= 32768.0 abs-new16) (< abs-new16 65536.0)) (and (= two-to-exp-new16 32768.0) (= two-to-exp-p-minus-e-new16 256.0))))
(assert (=> (and (<= 65536.0 abs-new16) (< abs-new16 131072.0)) (and (= two-to-exp-new16 65536.0) (= two-to-exp-p-minus-e-new16 128.0))))
(assert (=> (and (<= 131072.0 abs-new16) (< abs-new16 262144.0)) (and (= two-to-exp-new16 131072.0) (= two-to-exp-p-minus-e-new16 64.0))))
(assert (=> (and (<= 262144.0 abs-new16) (< abs-new16 524288.0)) (and (= two-to-exp-new16 262144.0) (= two-to-exp-p-minus-e-new16 32.0))))
(assert (=> (and (<= 524288.0 abs-new16) (< abs-new16 1048576.0)) (and (= two-to-exp-new16 524288.0) (= two-to-exp-p-minus-e-new16 16.0))))
(assert (=> (and (<= 1048576.0 abs-new16) (< abs-new16 2097152.0)) (and (= two-to-exp-new16 1048576.0) (= two-to-exp-p-minus-e-new16 8.0))))
(assert (=> (and (<= 2097152.0 abs-new16) (< abs-new16 4194304.0)) (and (= two-to-exp-new16 2097152.0) (= two-to-exp-p-minus-e-new16 4.0))))
(assert (=> (and (<= 4194304.0 abs-new16) (< abs-new16 8388608.0)) (and (= two-to-exp-new16 4194304.0) (= two-to-exp-p-minus-e-new16 2.0))))
(assert (=> (and (<= 8388608.0 abs-new16) (< abs-new16 16777216.0)) (and (= two-to-exp-new16 8388608.0) (= two-to-exp-p-minus-e-new16 1.0))))
(assert (=> (and (<= 16777216.0 abs-new16) (< abs-new16 33554432.0)) (and (= two-to-exp-new16 16777216.0) (= two-to-exp-p-minus-e-new16 0.5))))
(assert (=> (and (<= 33554432.0 abs-new16) (< abs-new16 67108864.0)) (and (= two-to-exp-new16 33554432.0) (= two-to-exp-p-minus-e-new16 0.25))))
(assert (=> (and (<= 67108864.0 abs-new16) (< abs-new16 134217728.0)) (and (= two-to-exp-new16 67108864.0) (= two-to-exp-p-minus-e-new16 0.125))))
(assert (=> (and (<= 134217728.0 abs-new16) (< abs-new16 268435456.0)) (and (= two-to-exp-new16 134217728.0) (= two-to-exp-p-minus-e-new16 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new16) (< abs-new16 536870912.0)) (and (= two-to-exp-new16 268435456.0) (= two-to-exp-p-minus-e-new16 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new16) (< abs-new16 1073741824.0)) (and (= two-to-exp-new16 536870912.0) (= two-to-exp-p-minus-e-new16 0.015625))))

(assert (= new16-real (+ a1 a2)))

;(assert (= new16  (* (/ (to_real (to_int (* (/ new16-real two-to-exp-new16) two-to-p))) two-to-p) two-to-exp-new16 )))
(assert (= (* two-to-exp-p-minus-e-new16 new16) (to_real (to_int (* new16-real two-to-exp-p-minus-e-new16)))))

(declare-const new17 Real)

(declare-const abs-new17 Real)
(assert (or (and (<= 1.0  new17) (< new17 1073741824.0)) (and (>= -1.0  new17) (> new17 -1073741824.0))))
(assert (=> (>= new17 0.0) (= abs-new17 new17)));added
(assert (=> (< new17 0.0) (= abs-new17 (- new17))));added
(declare-const new17-real Real)
(declare-const two-to-exp-new17 Real)
(declare-const two-to-exp-p-minus-e-new17 Real)
(assert (=> (and (<= 1.0 abs-new17) (< abs-new17 2.0)) (and (= two-to-exp-new17 1.0) (= two-to-exp-p-minus-e-new17 8388608.0))))
(assert (=> (and (<= 2.0 abs-new17) (< abs-new17 4.0)) (and (= two-to-exp-new17 2.0) (= two-to-exp-p-minus-e-new17 4194304.0))))
(assert (=> (and (<= 4.0 abs-new17) (< abs-new17 8.0)) (and (= two-to-exp-new17 4.0) (= two-to-exp-p-minus-e-new17 2097152.0))))
(assert (=> (and (<= 8.0 abs-new17) (< abs-new17 16.0)) (and (= two-to-exp-new17 8.0) (= two-to-exp-p-minus-e-new17 1048576.0))))
(assert (=> (and (<= 16.0 abs-new17) (< abs-new17 32.0)) (and (= two-to-exp-new17 16.0) (= two-to-exp-p-minus-e-new17 524288.0))))
(assert (=> (and (<= 32.0 abs-new17) (< abs-new17 64.0)) (and (= two-to-exp-new17 32.0) (= two-to-exp-p-minus-e-new17 262144.0))))
(assert (=> (and (<= 64.0 abs-new17) (< abs-new17 128.0)) (and (= two-to-exp-new17 64.0) (= two-to-exp-p-minus-e-new17 131072.0))))
(assert (=> (and (<= 128.0 abs-new17) (< abs-new17 256.0)) (and (= two-to-exp-new17 128.0) (= two-to-exp-p-minus-e-new17 65536.0))))
(assert (=> (and (<= 256.0 abs-new17) (< abs-new17 512.0)) (and (= two-to-exp-new17 256.0) (= two-to-exp-p-minus-e-new17 32768.0))))
(assert (=> (and (<= 512.0 abs-new17) (< abs-new17 1024.0)) (and (= two-to-exp-new17 512.0) (= two-to-exp-p-minus-e-new17 16384.0))))
(assert (=> (and (<= 1024.0 abs-new17) (< abs-new17 2048.0)) (and (= two-to-exp-new17 1024.0) (= two-to-exp-p-minus-e-new17 8192.0))))
(assert (=> (and (<= 2048.0 abs-new17) (< abs-new17 4096.0)) (and (= two-to-exp-new17 2048.0) (= two-to-exp-p-minus-e-new17 4096.0))))
(assert (=> (and (<= 4096.0 abs-new17) (< abs-new17 8192.0)) (and (= two-to-exp-new17 4096.0) (= two-to-exp-p-minus-e-new17 2048.0))))
(assert (=> (and (<= 8192.0 abs-new17) (< abs-new17 16384.0)) (and (= two-to-exp-new17 8192.0) (= two-to-exp-p-minus-e-new17 1024.0))))
(assert (=> (and (<= 16384.0 abs-new17) (< abs-new17 32768.0)) (and (= two-to-exp-new17 16384.0) (= two-to-exp-p-minus-e-new17 512.0))))
(assert (=> (and (<= 32768.0 abs-new17) (< abs-new17 65536.0)) (and (= two-to-exp-new17 32768.0) (= two-to-exp-p-minus-e-new17 256.0))))
(assert (=> (and (<= 65536.0 abs-new17) (< abs-new17 131072.0)) (and (= two-to-exp-new17 65536.0) (= two-to-exp-p-minus-e-new17 128.0))))
(assert (=> (and (<= 131072.0 abs-new17) (< abs-new17 262144.0)) (and (= two-to-exp-new17 131072.0) (= two-to-exp-p-minus-e-new17 64.0))))
(assert (=> (and (<= 262144.0 abs-new17) (< abs-new17 524288.0)) (and (= two-to-exp-new17 262144.0) (= two-to-exp-p-minus-e-new17 32.0))))
(assert (=> (and (<= 524288.0 abs-new17) (< abs-new17 1048576.0)) (and (= two-to-exp-new17 524288.0) (= two-to-exp-p-minus-e-new17 16.0))))
(assert (=> (and (<= 1048576.0 abs-new17) (< abs-new17 2097152.0)) (and (= two-to-exp-new17 1048576.0) (= two-to-exp-p-minus-e-new17 8.0))))
(assert (=> (and (<= 2097152.0 abs-new17) (< abs-new17 4194304.0)) (and (= two-to-exp-new17 2097152.0) (= two-to-exp-p-minus-e-new17 4.0))))
(assert (=> (and (<= 4194304.0 abs-new17) (< abs-new17 8388608.0)) (and (= two-to-exp-new17 4194304.0) (= two-to-exp-p-minus-e-new17 2.0))))
(assert (=> (and (<= 8388608.0 abs-new17) (< abs-new17 16777216.0)) (and (= two-to-exp-new17 8388608.0) (= two-to-exp-p-minus-e-new17 1.0))))
(assert (=> (and (<= 16777216.0 abs-new17) (< abs-new17 33554432.0)) (and (= two-to-exp-new17 16777216.0) (= two-to-exp-p-minus-e-new17 0.5))))
(assert (=> (and (<= 33554432.0 abs-new17) (< abs-new17 67108864.0)) (and (= two-to-exp-new17 33554432.0) (= two-to-exp-p-minus-e-new17 0.25))))
(assert (=> (and (<= 67108864.0 abs-new17) (< abs-new17 134217728.0)) (and (= two-to-exp-new17 67108864.0) (= two-to-exp-p-minus-e-new17 0.125))))
(assert (=> (and (<= 134217728.0 abs-new17) (< abs-new17 268435456.0)) (and (= two-to-exp-new17 134217728.0) (= two-to-exp-p-minus-e-new17 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new17) (< abs-new17 536870912.0)) (and (= two-to-exp-new17 268435456.0) (= two-to-exp-p-minus-e-new17 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new17) (< abs-new17 1073741824.0)) (and (= two-to-exp-new17 536870912.0) (= two-to-exp-p-minus-e-new17 0.015625))))

(assert (= new17-real (+ a3 a4)))

;(assert (= new17  (* (/ (to_real (to_int (* (/ new17-real two-to-exp-new17) two-to-p))) two-to-p) two-to-exp-new17 )))
(assert (= (* two-to-exp-p-minus-e-new17 new17) (to_real (to_int (* new17-real two-to-exp-p-minus-e-new17)))))

(declare-const new14 Real)

(declare-const abs-new14 Real)
(assert (or (and (<= 1.0  new14) (< new14 1073741824.0)) (and (>= -1.0  new14) (> new14 -1073741824.0))))
(assert (=> (>= new14 0.0) (= abs-new14 new14)));added
(assert (=> (< new14 0.0) (= abs-new14 (- new14))));added
(declare-const new14-real Real)
(declare-const two-to-exp-new14 Real)
(declare-const two-to-exp-p-minus-e-new14 Real)
(assert (=> (and (<= 1.0 abs-new14) (< abs-new14 2.0)) (and (= two-to-exp-new14 1.0) (= two-to-exp-p-minus-e-new14 8388608.0))))
(assert (=> (and (<= 2.0 abs-new14) (< abs-new14 4.0)) (and (= two-to-exp-new14 2.0) (= two-to-exp-p-minus-e-new14 4194304.0))))
(assert (=> (and (<= 4.0 abs-new14) (< abs-new14 8.0)) (and (= two-to-exp-new14 4.0) (= two-to-exp-p-minus-e-new14 2097152.0))))
(assert (=> (and (<= 8.0 abs-new14) (< abs-new14 16.0)) (and (= two-to-exp-new14 8.0) (= two-to-exp-p-minus-e-new14 1048576.0))))
(assert (=> (and (<= 16.0 abs-new14) (< abs-new14 32.0)) (and (= two-to-exp-new14 16.0) (= two-to-exp-p-minus-e-new14 524288.0))))
(assert (=> (and (<= 32.0 abs-new14) (< abs-new14 64.0)) (and (= two-to-exp-new14 32.0) (= two-to-exp-p-minus-e-new14 262144.0))))
(assert (=> (and (<= 64.0 abs-new14) (< abs-new14 128.0)) (and (= two-to-exp-new14 64.0) (= two-to-exp-p-minus-e-new14 131072.0))))
(assert (=> (and (<= 128.0 abs-new14) (< abs-new14 256.0)) (and (= two-to-exp-new14 128.0) (= two-to-exp-p-minus-e-new14 65536.0))))
(assert (=> (and (<= 256.0 abs-new14) (< abs-new14 512.0)) (and (= two-to-exp-new14 256.0) (= two-to-exp-p-minus-e-new14 32768.0))))
(assert (=> (and (<= 512.0 abs-new14) (< abs-new14 1024.0)) (and (= two-to-exp-new14 512.0) (= two-to-exp-p-minus-e-new14 16384.0))))
(assert (=> (and (<= 1024.0 abs-new14) (< abs-new14 2048.0)) (and (= two-to-exp-new14 1024.0) (= two-to-exp-p-minus-e-new14 8192.0))))
(assert (=> (and (<= 2048.0 abs-new14) (< abs-new14 4096.0)) (and (= two-to-exp-new14 2048.0) (= two-to-exp-p-minus-e-new14 4096.0))))
(assert (=> (and (<= 4096.0 abs-new14) (< abs-new14 8192.0)) (and (= two-to-exp-new14 4096.0) (= two-to-exp-p-minus-e-new14 2048.0))))
(assert (=> (and (<= 8192.0 abs-new14) (< abs-new14 16384.0)) (and (= two-to-exp-new14 8192.0) (= two-to-exp-p-minus-e-new14 1024.0))))
(assert (=> (and (<= 16384.0 abs-new14) (< abs-new14 32768.0)) (and (= two-to-exp-new14 16384.0) (= two-to-exp-p-minus-e-new14 512.0))))
(assert (=> (and (<= 32768.0 abs-new14) (< abs-new14 65536.0)) (and (= two-to-exp-new14 32768.0) (= two-to-exp-p-minus-e-new14 256.0))))
(assert (=> (and (<= 65536.0 abs-new14) (< abs-new14 131072.0)) (and (= two-to-exp-new14 65536.0) (= two-to-exp-p-minus-e-new14 128.0))))
(assert (=> (and (<= 131072.0 abs-new14) (< abs-new14 262144.0)) (and (= two-to-exp-new14 131072.0) (= two-to-exp-p-minus-e-new14 64.0))))
(assert (=> (and (<= 262144.0 abs-new14) (< abs-new14 524288.0)) (and (= two-to-exp-new14 262144.0) (= two-to-exp-p-minus-e-new14 32.0))))
(assert (=> (and (<= 524288.0 abs-new14) (< abs-new14 1048576.0)) (and (= two-to-exp-new14 524288.0) (= two-to-exp-p-minus-e-new14 16.0))))
(assert (=> (and (<= 1048576.0 abs-new14) (< abs-new14 2097152.0)) (and (= two-to-exp-new14 1048576.0) (= two-to-exp-p-minus-e-new14 8.0))))
(assert (=> (and (<= 2097152.0 abs-new14) (< abs-new14 4194304.0)) (and (= two-to-exp-new14 2097152.0) (= two-to-exp-p-minus-e-new14 4.0))))
(assert (=> (and (<= 4194304.0 abs-new14) (< abs-new14 8388608.0)) (and (= two-to-exp-new14 4194304.0) (= two-to-exp-p-minus-e-new14 2.0))))
(assert (=> (and (<= 8388608.0 abs-new14) (< abs-new14 16777216.0)) (and (= two-to-exp-new14 8388608.0) (= two-to-exp-p-minus-e-new14 1.0))))
(assert (=> (and (<= 16777216.0 abs-new14) (< abs-new14 33554432.0)) (and (= two-to-exp-new14 16777216.0) (= two-to-exp-p-minus-e-new14 0.5))))
(assert (=> (and (<= 33554432.0 abs-new14) (< abs-new14 67108864.0)) (and (= two-to-exp-new14 33554432.0) (= two-to-exp-p-minus-e-new14 0.25))))
(assert (=> (and (<= 67108864.0 abs-new14) (< abs-new14 134217728.0)) (and (= two-to-exp-new14 67108864.0) (= two-to-exp-p-minus-e-new14 0.125))))
(assert (=> (and (<= 134217728.0 abs-new14) (< abs-new14 268435456.0)) (and (= two-to-exp-new14 134217728.0) (= two-to-exp-p-minus-e-new14 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new14) (< abs-new14 536870912.0)) (and (= two-to-exp-new14 268435456.0) (= two-to-exp-p-minus-e-new14 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new14) (< abs-new14 1073741824.0)) (and (= two-to-exp-new14 536870912.0) (= two-to-exp-p-minus-e-new14 0.015625))))

(assert (= new14-real (+ new16 new17)))

;(assert (= new14  (* (/ (to_real (to_int (* (/ new14-real two-to-exp-new14) two-to-p))) two-to-p) two-to-exp-new14 )))
(assert (= (* two-to-exp-p-minus-e-new14 new14) (to_real (to_int (* new14-real two-to-exp-p-minus-e-new14)))))

(declare-const new18 Real)

(declare-const abs-new18 Real)
(assert (or (and (<= 1.0  new18) (< new18 1073741824.0)) (and (>= -1.0  new18) (> new18 -1073741824.0))))
(assert (=> (>= new18 0.0) (= abs-new18 new18)));added
(assert (=> (< new18 0.0) (= abs-new18 (- new18))));added
(declare-const new18-real Real)
(declare-const two-to-exp-new18 Real)
(declare-const two-to-exp-p-minus-e-new18 Real)
(assert (=> (and (<= 1.0 abs-new18) (< abs-new18 2.0)) (and (= two-to-exp-new18 1.0) (= two-to-exp-p-minus-e-new18 8388608.0))))
(assert (=> (and (<= 2.0 abs-new18) (< abs-new18 4.0)) (and (= two-to-exp-new18 2.0) (= two-to-exp-p-minus-e-new18 4194304.0))))
(assert (=> (and (<= 4.0 abs-new18) (< abs-new18 8.0)) (and (= two-to-exp-new18 4.0) (= two-to-exp-p-minus-e-new18 2097152.0))))
(assert (=> (and (<= 8.0 abs-new18) (< abs-new18 16.0)) (and (= two-to-exp-new18 8.0) (= two-to-exp-p-minus-e-new18 1048576.0))))
(assert (=> (and (<= 16.0 abs-new18) (< abs-new18 32.0)) (and (= two-to-exp-new18 16.0) (= two-to-exp-p-minus-e-new18 524288.0))))
(assert (=> (and (<= 32.0 abs-new18) (< abs-new18 64.0)) (and (= two-to-exp-new18 32.0) (= two-to-exp-p-minus-e-new18 262144.0))))
(assert (=> (and (<= 64.0 abs-new18) (< abs-new18 128.0)) (and (= two-to-exp-new18 64.0) (= two-to-exp-p-minus-e-new18 131072.0))))
(assert (=> (and (<= 128.0 abs-new18) (< abs-new18 256.0)) (and (= two-to-exp-new18 128.0) (= two-to-exp-p-minus-e-new18 65536.0))))
(assert (=> (and (<= 256.0 abs-new18) (< abs-new18 512.0)) (and (= two-to-exp-new18 256.0) (= two-to-exp-p-minus-e-new18 32768.0))))
(assert (=> (and (<= 512.0 abs-new18) (< abs-new18 1024.0)) (and (= two-to-exp-new18 512.0) (= two-to-exp-p-minus-e-new18 16384.0))))
(assert (=> (and (<= 1024.0 abs-new18) (< abs-new18 2048.0)) (and (= two-to-exp-new18 1024.0) (= two-to-exp-p-minus-e-new18 8192.0))))
(assert (=> (and (<= 2048.0 abs-new18) (< abs-new18 4096.0)) (and (= two-to-exp-new18 2048.0) (= two-to-exp-p-minus-e-new18 4096.0))))
(assert (=> (and (<= 4096.0 abs-new18) (< abs-new18 8192.0)) (and (= two-to-exp-new18 4096.0) (= two-to-exp-p-minus-e-new18 2048.0))))
(assert (=> (and (<= 8192.0 abs-new18) (< abs-new18 16384.0)) (and (= two-to-exp-new18 8192.0) (= two-to-exp-p-minus-e-new18 1024.0))))
(assert (=> (and (<= 16384.0 abs-new18) (< abs-new18 32768.0)) (and (= two-to-exp-new18 16384.0) (= two-to-exp-p-minus-e-new18 512.0))))
(assert (=> (and (<= 32768.0 abs-new18) (< abs-new18 65536.0)) (and (= two-to-exp-new18 32768.0) (= two-to-exp-p-minus-e-new18 256.0))))
(assert (=> (and (<= 65536.0 abs-new18) (< abs-new18 131072.0)) (and (= two-to-exp-new18 65536.0) (= two-to-exp-p-minus-e-new18 128.0))))
(assert (=> (and (<= 131072.0 abs-new18) (< abs-new18 262144.0)) (and (= two-to-exp-new18 131072.0) (= two-to-exp-p-minus-e-new18 64.0))))
(assert (=> (and (<= 262144.0 abs-new18) (< abs-new18 524288.0)) (and (= two-to-exp-new18 262144.0) (= two-to-exp-p-minus-e-new18 32.0))))
(assert (=> (and (<= 524288.0 abs-new18) (< abs-new18 1048576.0)) (and (= two-to-exp-new18 524288.0) (= two-to-exp-p-minus-e-new18 16.0))))
(assert (=> (and (<= 1048576.0 abs-new18) (< abs-new18 2097152.0)) (and (= two-to-exp-new18 1048576.0) (= two-to-exp-p-minus-e-new18 8.0))))
(assert (=> (and (<= 2097152.0 abs-new18) (< abs-new18 4194304.0)) (and (= two-to-exp-new18 2097152.0) (= two-to-exp-p-minus-e-new18 4.0))))
(assert (=> (and (<= 4194304.0 abs-new18) (< abs-new18 8388608.0)) (and (= two-to-exp-new18 4194304.0) (= two-to-exp-p-minus-e-new18 2.0))))
(assert (=> (and (<= 8388608.0 abs-new18) (< abs-new18 16777216.0)) (and (= two-to-exp-new18 8388608.0) (= two-to-exp-p-minus-e-new18 1.0))))
(assert (=> (and (<= 16777216.0 abs-new18) (< abs-new18 33554432.0)) (and (= two-to-exp-new18 16777216.0) (= two-to-exp-p-minus-e-new18 0.5))))
(assert (=> (and (<= 33554432.0 abs-new18) (< abs-new18 67108864.0)) (and (= two-to-exp-new18 33554432.0) (= two-to-exp-p-minus-e-new18 0.25))))
(assert (=> (and (<= 67108864.0 abs-new18) (< abs-new18 134217728.0)) (and (= two-to-exp-new18 67108864.0) (= two-to-exp-p-minus-e-new18 0.125))))
(assert (=> (and (<= 134217728.0 abs-new18) (< abs-new18 268435456.0)) (and (= two-to-exp-new18 134217728.0) (= two-to-exp-p-minus-e-new18 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new18) (< abs-new18 536870912.0)) (and (= two-to-exp-new18 268435456.0) (= two-to-exp-p-minus-e-new18 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new18) (< abs-new18 1073741824.0)) (and (= two-to-exp-new18 536870912.0) (= two-to-exp-p-minus-e-new18 0.015625))))

(assert (= new18-real (+ a5 a6)))

;(assert (= new18  (* (/ (to_real (to_int (* (/ new18-real two-to-exp-new18) two-to-p))) two-to-p) two-to-exp-new18 )))
(assert (= (* two-to-exp-p-minus-e-new18 new18) (to_real (to_int (* new18-real two-to-exp-p-minus-e-new18)))))

(declare-const new19 Real)

(declare-const abs-new19 Real)
(assert (or (and (<= 1.0  new19) (< new19 1073741824.0)) (and (>= -1.0  new19) (> new19 -1073741824.0))))
(assert (=> (>= new19 0.0) (= abs-new19 new19)));added
(assert (=> (< new19 0.0) (= abs-new19 (- new19))));added
(declare-const new19-real Real)
(declare-const two-to-exp-new19 Real)
(declare-const two-to-exp-p-minus-e-new19 Real)
(assert (=> (and (<= 1.0 abs-new19) (< abs-new19 2.0)) (and (= two-to-exp-new19 1.0) (= two-to-exp-p-minus-e-new19 8388608.0))))
(assert (=> (and (<= 2.0 abs-new19) (< abs-new19 4.0)) (and (= two-to-exp-new19 2.0) (= two-to-exp-p-minus-e-new19 4194304.0))))
(assert (=> (and (<= 4.0 abs-new19) (< abs-new19 8.0)) (and (= two-to-exp-new19 4.0) (= two-to-exp-p-minus-e-new19 2097152.0))))
(assert (=> (and (<= 8.0 abs-new19) (< abs-new19 16.0)) (and (= two-to-exp-new19 8.0) (= two-to-exp-p-minus-e-new19 1048576.0))))
(assert (=> (and (<= 16.0 abs-new19) (< abs-new19 32.0)) (and (= two-to-exp-new19 16.0) (= two-to-exp-p-minus-e-new19 524288.0))))
(assert (=> (and (<= 32.0 abs-new19) (< abs-new19 64.0)) (and (= two-to-exp-new19 32.0) (= two-to-exp-p-minus-e-new19 262144.0))))
(assert (=> (and (<= 64.0 abs-new19) (< abs-new19 128.0)) (and (= two-to-exp-new19 64.0) (= two-to-exp-p-minus-e-new19 131072.0))))
(assert (=> (and (<= 128.0 abs-new19) (< abs-new19 256.0)) (and (= two-to-exp-new19 128.0) (= two-to-exp-p-minus-e-new19 65536.0))))
(assert (=> (and (<= 256.0 abs-new19) (< abs-new19 512.0)) (and (= two-to-exp-new19 256.0) (= two-to-exp-p-minus-e-new19 32768.0))))
(assert (=> (and (<= 512.0 abs-new19) (< abs-new19 1024.0)) (and (= two-to-exp-new19 512.0) (= two-to-exp-p-minus-e-new19 16384.0))))
(assert (=> (and (<= 1024.0 abs-new19) (< abs-new19 2048.0)) (and (= two-to-exp-new19 1024.0) (= two-to-exp-p-minus-e-new19 8192.0))))
(assert (=> (and (<= 2048.0 abs-new19) (< abs-new19 4096.0)) (and (= two-to-exp-new19 2048.0) (= two-to-exp-p-minus-e-new19 4096.0))))
(assert (=> (and (<= 4096.0 abs-new19) (< abs-new19 8192.0)) (and (= two-to-exp-new19 4096.0) (= two-to-exp-p-minus-e-new19 2048.0))))
(assert (=> (and (<= 8192.0 abs-new19) (< abs-new19 16384.0)) (and (= two-to-exp-new19 8192.0) (= two-to-exp-p-minus-e-new19 1024.0))))
(assert (=> (and (<= 16384.0 abs-new19) (< abs-new19 32768.0)) (and (= two-to-exp-new19 16384.0) (= two-to-exp-p-minus-e-new19 512.0))))
(assert (=> (and (<= 32768.0 abs-new19) (< abs-new19 65536.0)) (and (= two-to-exp-new19 32768.0) (= two-to-exp-p-minus-e-new19 256.0))))
(assert (=> (and (<= 65536.0 abs-new19) (< abs-new19 131072.0)) (and (= two-to-exp-new19 65536.0) (= two-to-exp-p-minus-e-new19 128.0))))
(assert (=> (and (<= 131072.0 abs-new19) (< abs-new19 262144.0)) (and (= two-to-exp-new19 131072.0) (= two-to-exp-p-minus-e-new19 64.0))))
(assert (=> (and (<= 262144.0 abs-new19) (< abs-new19 524288.0)) (and (= two-to-exp-new19 262144.0) (= two-to-exp-p-minus-e-new19 32.0))))
(assert (=> (and (<= 524288.0 abs-new19) (< abs-new19 1048576.0)) (and (= two-to-exp-new19 524288.0) (= two-to-exp-p-minus-e-new19 16.0))))
(assert (=> (and (<= 1048576.0 abs-new19) (< abs-new19 2097152.0)) (and (= two-to-exp-new19 1048576.0) (= two-to-exp-p-minus-e-new19 8.0))))
(assert (=> (and (<= 2097152.0 abs-new19) (< abs-new19 4194304.0)) (and (= two-to-exp-new19 2097152.0) (= two-to-exp-p-minus-e-new19 4.0))))
(assert (=> (and (<= 4194304.0 abs-new19) (< abs-new19 8388608.0)) (and (= two-to-exp-new19 4194304.0) (= two-to-exp-p-minus-e-new19 2.0))))
(assert (=> (and (<= 8388608.0 abs-new19) (< abs-new19 16777216.0)) (and (= two-to-exp-new19 8388608.0) (= two-to-exp-p-minus-e-new19 1.0))))
(assert (=> (and (<= 16777216.0 abs-new19) (< abs-new19 33554432.0)) (and (= two-to-exp-new19 16777216.0) (= two-to-exp-p-minus-e-new19 0.5))))
(assert (=> (and (<= 33554432.0 abs-new19) (< abs-new19 67108864.0)) (and (= two-to-exp-new19 33554432.0) (= two-to-exp-p-minus-e-new19 0.25))))
(assert (=> (and (<= 67108864.0 abs-new19) (< abs-new19 134217728.0)) (and (= two-to-exp-new19 67108864.0) (= two-to-exp-p-minus-e-new19 0.125))))
(assert (=> (and (<= 134217728.0 abs-new19) (< abs-new19 268435456.0)) (and (= two-to-exp-new19 134217728.0) (= two-to-exp-p-minus-e-new19 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new19) (< abs-new19 536870912.0)) (and (= two-to-exp-new19 268435456.0) (= two-to-exp-p-minus-e-new19 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new19) (< abs-new19 1073741824.0)) (and (= two-to-exp-new19 536870912.0) (= two-to-exp-p-minus-e-new19 0.015625))))

(assert (= new19-real (+ a7 a8)))

;(assert (= new19  (* (/ (to_real (to_int (* (/ new19-real two-to-exp-new19) two-to-p))) two-to-p) two-to-exp-new19 )))
(assert (= (* two-to-exp-p-minus-e-new19 new19) (to_real (to_int (* new19-real two-to-exp-p-minus-e-new19)))))

(declare-const new15 Real)

(declare-const abs-new15 Real)
(assert (or (and (<= 1.0  new15) (< new15 1073741824.0)) (and (>= -1.0  new15) (> new15 -1073741824.0))))
(assert (=> (>= new15 0.0) (= abs-new15 new15)));added
(assert (=> (< new15 0.0) (= abs-new15 (- new15))));added
(declare-const new15-real Real)
(declare-const two-to-exp-new15 Real)
(declare-const two-to-exp-p-minus-e-new15 Real)
(assert (=> (and (<= 1.0 abs-new15) (< abs-new15 2.0)) (and (= two-to-exp-new15 1.0) (= two-to-exp-p-minus-e-new15 8388608.0))))
(assert (=> (and (<= 2.0 abs-new15) (< abs-new15 4.0)) (and (= two-to-exp-new15 2.0) (= two-to-exp-p-minus-e-new15 4194304.0))))
(assert (=> (and (<= 4.0 abs-new15) (< abs-new15 8.0)) (and (= two-to-exp-new15 4.0) (= two-to-exp-p-minus-e-new15 2097152.0))))
(assert (=> (and (<= 8.0 abs-new15) (< abs-new15 16.0)) (and (= two-to-exp-new15 8.0) (= two-to-exp-p-minus-e-new15 1048576.0))))
(assert (=> (and (<= 16.0 abs-new15) (< abs-new15 32.0)) (and (= two-to-exp-new15 16.0) (= two-to-exp-p-minus-e-new15 524288.0))))
(assert (=> (and (<= 32.0 abs-new15) (< abs-new15 64.0)) (and (= two-to-exp-new15 32.0) (= two-to-exp-p-minus-e-new15 262144.0))))
(assert (=> (and (<= 64.0 abs-new15) (< abs-new15 128.0)) (and (= two-to-exp-new15 64.0) (= two-to-exp-p-minus-e-new15 131072.0))))
(assert (=> (and (<= 128.0 abs-new15) (< abs-new15 256.0)) (and (= two-to-exp-new15 128.0) (= two-to-exp-p-minus-e-new15 65536.0))))
(assert (=> (and (<= 256.0 abs-new15) (< abs-new15 512.0)) (and (= two-to-exp-new15 256.0) (= two-to-exp-p-minus-e-new15 32768.0))))
(assert (=> (and (<= 512.0 abs-new15) (< abs-new15 1024.0)) (and (= two-to-exp-new15 512.0) (= two-to-exp-p-minus-e-new15 16384.0))))
(assert (=> (and (<= 1024.0 abs-new15) (< abs-new15 2048.0)) (and (= two-to-exp-new15 1024.0) (= two-to-exp-p-minus-e-new15 8192.0))))
(assert (=> (and (<= 2048.0 abs-new15) (< abs-new15 4096.0)) (and (= two-to-exp-new15 2048.0) (= two-to-exp-p-minus-e-new15 4096.0))))
(assert (=> (and (<= 4096.0 abs-new15) (< abs-new15 8192.0)) (and (= two-to-exp-new15 4096.0) (= two-to-exp-p-minus-e-new15 2048.0))))
(assert (=> (and (<= 8192.0 abs-new15) (< abs-new15 16384.0)) (and (= two-to-exp-new15 8192.0) (= two-to-exp-p-minus-e-new15 1024.0))))
(assert (=> (and (<= 16384.0 abs-new15) (< abs-new15 32768.0)) (and (= two-to-exp-new15 16384.0) (= two-to-exp-p-minus-e-new15 512.0))))
(assert (=> (and (<= 32768.0 abs-new15) (< abs-new15 65536.0)) (and (= two-to-exp-new15 32768.0) (= two-to-exp-p-minus-e-new15 256.0))))
(assert (=> (and (<= 65536.0 abs-new15) (< abs-new15 131072.0)) (and (= two-to-exp-new15 65536.0) (= two-to-exp-p-minus-e-new15 128.0))))
(assert (=> (and (<= 131072.0 abs-new15) (< abs-new15 262144.0)) (and (= two-to-exp-new15 131072.0) (= two-to-exp-p-minus-e-new15 64.0))))
(assert (=> (and (<= 262144.0 abs-new15) (< abs-new15 524288.0)) (and (= two-to-exp-new15 262144.0) (= two-to-exp-p-minus-e-new15 32.0))))
(assert (=> (and (<= 524288.0 abs-new15) (< abs-new15 1048576.0)) (and (= two-to-exp-new15 524288.0) (= two-to-exp-p-minus-e-new15 16.0))))
(assert (=> (and (<= 1048576.0 abs-new15) (< abs-new15 2097152.0)) (and (= two-to-exp-new15 1048576.0) (= two-to-exp-p-minus-e-new15 8.0))))
(assert (=> (and (<= 2097152.0 abs-new15) (< abs-new15 4194304.0)) (and (= two-to-exp-new15 2097152.0) (= two-to-exp-p-minus-e-new15 4.0))))
(assert (=> (and (<= 4194304.0 abs-new15) (< abs-new15 8388608.0)) (and (= two-to-exp-new15 4194304.0) (= two-to-exp-p-minus-e-new15 2.0))))
(assert (=> (and (<= 8388608.0 abs-new15) (< abs-new15 16777216.0)) (and (= two-to-exp-new15 8388608.0) (= two-to-exp-p-minus-e-new15 1.0))))
(assert (=> (and (<= 16777216.0 abs-new15) (< abs-new15 33554432.0)) (and (= two-to-exp-new15 16777216.0) (= two-to-exp-p-minus-e-new15 0.5))))
(assert (=> (and (<= 33554432.0 abs-new15) (< abs-new15 67108864.0)) (and (= two-to-exp-new15 33554432.0) (= two-to-exp-p-minus-e-new15 0.25))))
(assert (=> (and (<= 67108864.0 abs-new15) (< abs-new15 134217728.0)) (and (= two-to-exp-new15 67108864.0) (= two-to-exp-p-minus-e-new15 0.125))))
(assert (=> (and (<= 134217728.0 abs-new15) (< abs-new15 268435456.0)) (and (= two-to-exp-new15 134217728.0) (= two-to-exp-p-minus-e-new15 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new15) (< abs-new15 536870912.0)) (and (= two-to-exp-new15 268435456.0) (= two-to-exp-p-minus-e-new15 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new15) (< abs-new15 1073741824.0)) (and (= two-to-exp-new15 536870912.0) (= two-to-exp-p-minus-e-new15 0.015625))))

(assert (= new15-real (+ new18 new19)))

;(assert (= new15  (* (/ (to_real (to_int (* (/ new15-real two-to-exp-new15) two-to-p))) two-to-p) two-to-exp-new15 )))
(assert (= (* two-to-exp-p-minus-e-new15 new15) (to_real (to_int (* new15-real two-to-exp-p-minus-e-new15)))))

(declare-const new12 Real)

(declare-const abs-new12 Real)
(assert (or (and (<= 1.0  new12) (< new12 1073741824.0)) (and (>= -1.0  new12) (> new12 -1073741824.0))))
(assert (=> (>= new12 0.0) (= abs-new12 new12)));added
(assert (=> (< new12 0.0) (= abs-new12 (- new12))));added
(declare-const new12-real Real)
(declare-const two-to-exp-new12 Real)
(declare-const two-to-exp-p-minus-e-new12 Real)
(assert (=> (and (<= 1.0 abs-new12) (< abs-new12 2.0)) (and (= two-to-exp-new12 1.0) (= two-to-exp-p-minus-e-new12 8388608.0))))
(assert (=> (and (<= 2.0 abs-new12) (< abs-new12 4.0)) (and (= two-to-exp-new12 2.0) (= two-to-exp-p-minus-e-new12 4194304.0))))
(assert (=> (and (<= 4.0 abs-new12) (< abs-new12 8.0)) (and (= two-to-exp-new12 4.0) (= two-to-exp-p-minus-e-new12 2097152.0))))
(assert (=> (and (<= 8.0 abs-new12) (< abs-new12 16.0)) (and (= two-to-exp-new12 8.0) (= two-to-exp-p-minus-e-new12 1048576.0))))
(assert (=> (and (<= 16.0 abs-new12) (< abs-new12 32.0)) (and (= two-to-exp-new12 16.0) (= two-to-exp-p-minus-e-new12 524288.0))))
(assert (=> (and (<= 32.0 abs-new12) (< abs-new12 64.0)) (and (= two-to-exp-new12 32.0) (= two-to-exp-p-minus-e-new12 262144.0))))
(assert (=> (and (<= 64.0 abs-new12) (< abs-new12 128.0)) (and (= two-to-exp-new12 64.0) (= two-to-exp-p-minus-e-new12 131072.0))))
(assert (=> (and (<= 128.0 abs-new12) (< abs-new12 256.0)) (and (= two-to-exp-new12 128.0) (= two-to-exp-p-minus-e-new12 65536.0))))
(assert (=> (and (<= 256.0 abs-new12) (< abs-new12 512.0)) (and (= two-to-exp-new12 256.0) (= two-to-exp-p-minus-e-new12 32768.0))))
(assert (=> (and (<= 512.0 abs-new12) (< abs-new12 1024.0)) (and (= two-to-exp-new12 512.0) (= two-to-exp-p-minus-e-new12 16384.0))))
(assert (=> (and (<= 1024.0 abs-new12) (< abs-new12 2048.0)) (and (= two-to-exp-new12 1024.0) (= two-to-exp-p-minus-e-new12 8192.0))))
(assert (=> (and (<= 2048.0 abs-new12) (< abs-new12 4096.0)) (and (= two-to-exp-new12 2048.0) (= two-to-exp-p-minus-e-new12 4096.0))))
(assert (=> (and (<= 4096.0 abs-new12) (< abs-new12 8192.0)) (and (= two-to-exp-new12 4096.0) (= two-to-exp-p-minus-e-new12 2048.0))))
(assert (=> (and (<= 8192.0 abs-new12) (< abs-new12 16384.0)) (and (= two-to-exp-new12 8192.0) (= two-to-exp-p-minus-e-new12 1024.0))))
(assert (=> (and (<= 16384.0 abs-new12) (< abs-new12 32768.0)) (and (= two-to-exp-new12 16384.0) (= two-to-exp-p-minus-e-new12 512.0))))
(assert (=> (and (<= 32768.0 abs-new12) (< abs-new12 65536.0)) (and (= two-to-exp-new12 32768.0) (= two-to-exp-p-minus-e-new12 256.0))))
(assert (=> (and (<= 65536.0 abs-new12) (< abs-new12 131072.0)) (and (= two-to-exp-new12 65536.0) (= two-to-exp-p-minus-e-new12 128.0))))
(assert (=> (and (<= 131072.0 abs-new12) (< abs-new12 262144.0)) (and (= two-to-exp-new12 131072.0) (= two-to-exp-p-minus-e-new12 64.0))))
(assert (=> (and (<= 262144.0 abs-new12) (< abs-new12 524288.0)) (and (= two-to-exp-new12 262144.0) (= two-to-exp-p-minus-e-new12 32.0))))
(assert (=> (and (<= 524288.0 abs-new12) (< abs-new12 1048576.0)) (and (= two-to-exp-new12 524288.0) (= two-to-exp-p-minus-e-new12 16.0))))
(assert (=> (and (<= 1048576.0 abs-new12) (< abs-new12 2097152.0)) (and (= two-to-exp-new12 1048576.0) (= two-to-exp-p-minus-e-new12 8.0))))
(assert (=> (and (<= 2097152.0 abs-new12) (< abs-new12 4194304.0)) (and (= two-to-exp-new12 2097152.0) (= two-to-exp-p-minus-e-new12 4.0))))
(assert (=> (and (<= 4194304.0 abs-new12) (< abs-new12 8388608.0)) (and (= two-to-exp-new12 4194304.0) (= two-to-exp-p-minus-e-new12 2.0))))
(assert (=> (and (<= 8388608.0 abs-new12) (< abs-new12 16777216.0)) (and (= two-to-exp-new12 8388608.0) (= two-to-exp-p-minus-e-new12 1.0))))
(assert (=> (and (<= 16777216.0 abs-new12) (< abs-new12 33554432.0)) (and (= two-to-exp-new12 16777216.0) (= two-to-exp-p-minus-e-new12 0.5))))
(assert (=> (and (<= 33554432.0 abs-new12) (< abs-new12 67108864.0)) (and (= two-to-exp-new12 33554432.0) (= two-to-exp-p-minus-e-new12 0.25))))
(assert (=> (and (<= 67108864.0 abs-new12) (< abs-new12 134217728.0)) (and (= two-to-exp-new12 67108864.0) (= two-to-exp-p-minus-e-new12 0.125))))
(assert (=> (and (<= 134217728.0 abs-new12) (< abs-new12 268435456.0)) (and (= two-to-exp-new12 134217728.0) (= two-to-exp-p-minus-e-new12 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new12) (< abs-new12 536870912.0)) (and (= two-to-exp-new12 268435456.0) (= two-to-exp-p-minus-e-new12 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new12) (< abs-new12 1073741824.0)) (and (= two-to-exp-new12 536870912.0) (= two-to-exp-p-minus-e-new12 0.015625))))

(assert (= new12-real (+ new14 new15)))

;(assert (= new12  (* (/ (to_real (to_int (* (/ new12-real two-to-exp-new12) two-to-p))) two-to-p) two-to-exp-new12 )))
(assert (= (* two-to-exp-p-minus-e-new12 new12) (to_real (to_int (* new12-real two-to-exp-p-minus-e-new12)))))

(declare-const new20 Real)

(declare-const abs-new20 Real)
(assert (or (and (<= 1.0  new20) (< new20 1073741824.0)) (and (>= -1.0  new20) (> new20 -1073741824.0))))
(assert (=> (>= new20 0.0) (= abs-new20 new20)));added
(assert (=> (< new20 0.0) (= abs-new20 (- new20))));added
(declare-const new20-real Real)
(declare-const two-to-exp-new20 Real)
(declare-const two-to-exp-p-minus-e-new20 Real)
(assert (=> (and (<= 1.0 abs-new20) (< abs-new20 2.0)) (and (= two-to-exp-new20 1.0) (= two-to-exp-p-minus-e-new20 8388608.0))))
(assert (=> (and (<= 2.0 abs-new20) (< abs-new20 4.0)) (and (= two-to-exp-new20 2.0) (= two-to-exp-p-minus-e-new20 4194304.0))))
(assert (=> (and (<= 4.0 abs-new20) (< abs-new20 8.0)) (and (= two-to-exp-new20 4.0) (= two-to-exp-p-minus-e-new20 2097152.0))))
(assert (=> (and (<= 8.0 abs-new20) (< abs-new20 16.0)) (and (= two-to-exp-new20 8.0) (= two-to-exp-p-minus-e-new20 1048576.0))))
(assert (=> (and (<= 16.0 abs-new20) (< abs-new20 32.0)) (and (= two-to-exp-new20 16.0) (= two-to-exp-p-minus-e-new20 524288.0))))
(assert (=> (and (<= 32.0 abs-new20) (< abs-new20 64.0)) (and (= two-to-exp-new20 32.0) (= two-to-exp-p-minus-e-new20 262144.0))))
(assert (=> (and (<= 64.0 abs-new20) (< abs-new20 128.0)) (and (= two-to-exp-new20 64.0) (= two-to-exp-p-minus-e-new20 131072.0))))
(assert (=> (and (<= 128.0 abs-new20) (< abs-new20 256.0)) (and (= two-to-exp-new20 128.0) (= two-to-exp-p-minus-e-new20 65536.0))))
(assert (=> (and (<= 256.0 abs-new20) (< abs-new20 512.0)) (and (= two-to-exp-new20 256.0) (= two-to-exp-p-minus-e-new20 32768.0))))
(assert (=> (and (<= 512.0 abs-new20) (< abs-new20 1024.0)) (and (= two-to-exp-new20 512.0) (= two-to-exp-p-minus-e-new20 16384.0))))
(assert (=> (and (<= 1024.0 abs-new20) (< abs-new20 2048.0)) (and (= two-to-exp-new20 1024.0) (= two-to-exp-p-minus-e-new20 8192.0))))
(assert (=> (and (<= 2048.0 abs-new20) (< abs-new20 4096.0)) (and (= two-to-exp-new20 2048.0) (= two-to-exp-p-minus-e-new20 4096.0))))
(assert (=> (and (<= 4096.0 abs-new20) (< abs-new20 8192.0)) (and (= two-to-exp-new20 4096.0) (= two-to-exp-p-minus-e-new20 2048.0))))
(assert (=> (and (<= 8192.0 abs-new20) (< abs-new20 16384.0)) (and (= two-to-exp-new20 8192.0) (= two-to-exp-p-minus-e-new20 1024.0))))
(assert (=> (and (<= 16384.0 abs-new20) (< abs-new20 32768.0)) (and (= two-to-exp-new20 16384.0) (= two-to-exp-p-minus-e-new20 512.0))))
(assert (=> (and (<= 32768.0 abs-new20) (< abs-new20 65536.0)) (and (= two-to-exp-new20 32768.0) (= two-to-exp-p-minus-e-new20 256.0))))
(assert (=> (and (<= 65536.0 abs-new20) (< abs-new20 131072.0)) (and (= two-to-exp-new20 65536.0) (= two-to-exp-p-minus-e-new20 128.0))))
(assert (=> (and (<= 131072.0 abs-new20) (< abs-new20 262144.0)) (and (= two-to-exp-new20 131072.0) (= two-to-exp-p-minus-e-new20 64.0))))
(assert (=> (and (<= 262144.0 abs-new20) (< abs-new20 524288.0)) (and (= two-to-exp-new20 262144.0) (= two-to-exp-p-minus-e-new20 32.0))))
(assert (=> (and (<= 524288.0 abs-new20) (< abs-new20 1048576.0)) (and (= two-to-exp-new20 524288.0) (= two-to-exp-p-minus-e-new20 16.0))))
(assert (=> (and (<= 1048576.0 abs-new20) (< abs-new20 2097152.0)) (and (= two-to-exp-new20 1048576.0) (= two-to-exp-p-minus-e-new20 8.0))))
(assert (=> (and (<= 2097152.0 abs-new20) (< abs-new20 4194304.0)) (and (= two-to-exp-new20 2097152.0) (= two-to-exp-p-minus-e-new20 4.0))))
(assert (=> (and (<= 4194304.0 abs-new20) (< abs-new20 8388608.0)) (and (= two-to-exp-new20 4194304.0) (= two-to-exp-p-minus-e-new20 2.0))))
(assert (=> (and (<= 8388608.0 abs-new20) (< abs-new20 16777216.0)) (and (= two-to-exp-new20 8388608.0) (= two-to-exp-p-minus-e-new20 1.0))))
(assert (=> (and (<= 16777216.0 abs-new20) (< abs-new20 33554432.0)) (and (= two-to-exp-new20 16777216.0) (= two-to-exp-p-minus-e-new20 0.5))))
(assert (=> (and (<= 33554432.0 abs-new20) (< abs-new20 67108864.0)) (and (= two-to-exp-new20 33554432.0) (= two-to-exp-p-minus-e-new20 0.25))))
(assert (=> (and (<= 67108864.0 abs-new20) (< abs-new20 134217728.0)) (and (= two-to-exp-new20 67108864.0) (= two-to-exp-p-minus-e-new20 0.125))))
(assert (=> (and (<= 134217728.0 abs-new20) (< abs-new20 268435456.0)) (and (= two-to-exp-new20 134217728.0) (= two-to-exp-p-minus-e-new20 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new20) (< abs-new20 536870912.0)) (and (= two-to-exp-new20 268435456.0) (= two-to-exp-p-minus-e-new20 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new20) (< abs-new20 1073741824.0)) (and (= two-to-exp-new20 536870912.0) (= two-to-exp-p-minus-e-new20 0.015625))))

(assert (= new20-real (+ a9 a10)))

;(assert (= new20  (* (/ (to_real (to_int (* (/ new20-real two-to-exp-new20) two-to-p))) two-to-p) two-to-exp-new20 )))
(assert (= (* two-to-exp-p-minus-e-new20 new20) (to_real (to_int (* new20-real two-to-exp-p-minus-e-new20)))))

(declare-const new21 Real)

(declare-const abs-new21 Real)
(assert (or (and (<= 1.0  new21) (< new21 1073741824.0)) (and (>= -1.0  new21) (> new21 -1073741824.0))))
(assert (=> (>= new21 0.0) (= abs-new21 new21)));added
(assert (=> (< new21 0.0) (= abs-new21 (- new21))));added
(declare-const new21-real Real)
(declare-const two-to-exp-new21 Real)
(declare-const two-to-exp-p-minus-e-new21 Real)
(assert (=> (and (<= 1.0 abs-new21) (< abs-new21 2.0)) (and (= two-to-exp-new21 1.0) (= two-to-exp-p-minus-e-new21 8388608.0))))
(assert (=> (and (<= 2.0 abs-new21) (< abs-new21 4.0)) (and (= two-to-exp-new21 2.0) (= two-to-exp-p-minus-e-new21 4194304.0))))
(assert (=> (and (<= 4.0 abs-new21) (< abs-new21 8.0)) (and (= two-to-exp-new21 4.0) (= two-to-exp-p-minus-e-new21 2097152.0))))
(assert (=> (and (<= 8.0 abs-new21) (< abs-new21 16.0)) (and (= two-to-exp-new21 8.0) (= two-to-exp-p-minus-e-new21 1048576.0))))
(assert (=> (and (<= 16.0 abs-new21) (< abs-new21 32.0)) (and (= two-to-exp-new21 16.0) (= two-to-exp-p-minus-e-new21 524288.0))))
(assert (=> (and (<= 32.0 abs-new21) (< abs-new21 64.0)) (and (= two-to-exp-new21 32.0) (= two-to-exp-p-minus-e-new21 262144.0))))
(assert (=> (and (<= 64.0 abs-new21) (< abs-new21 128.0)) (and (= two-to-exp-new21 64.0) (= two-to-exp-p-minus-e-new21 131072.0))))
(assert (=> (and (<= 128.0 abs-new21) (< abs-new21 256.0)) (and (= two-to-exp-new21 128.0) (= two-to-exp-p-minus-e-new21 65536.0))))
(assert (=> (and (<= 256.0 abs-new21) (< abs-new21 512.0)) (and (= two-to-exp-new21 256.0) (= two-to-exp-p-minus-e-new21 32768.0))))
(assert (=> (and (<= 512.0 abs-new21) (< abs-new21 1024.0)) (and (= two-to-exp-new21 512.0) (= two-to-exp-p-minus-e-new21 16384.0))))
(assert (=> (and (<= 1024.0 abs-new21) (< abs-new21 2048.0)) (and (= two-to-exp-new21 1024.0) (= two-to-exp-p-minus-e-new21 8192.0))))
(assert (=> (and (<= 2048.0 abs-new21) (< abs-new21 4096.0)) (and (= two-to-exp-new21 2048.0) (= two-to-exp-p-minus-e-new21 4096.0))))
(assert (=> (and (<= 4096.0 abs-new21) (< abs-new21 8192.0)) (and (= two-to-exp-new21 4096.0) (= two-to-exp-p-minus-e-new21 2048.0))))
(assert (=> (and (<= 8192.0 abs-new21) (< abs-new21 16384.0)) (and (= two-to-exp-new21 8192.0) (= two-to-exp-p-minus-e-new21 1024.0))))
(assert (=> (and (<= 16384.0 abs-new21) (< abs-new21 32768.0)) (and (= two-to-exp-new21 16384.0) (= two-to-exp-p-minus-e-new21 512.0))))
(assert (=> (and (<= 32768.0 abs-new21) (< abs-new21 65536.0)) (and (= two-to-exp-new21 32768.0) (= two-to-exp-p-minus-e-new21 256.0))))
(assert (=> (and (<= 65536.0 abs-new21) (< abs-new21 131072.0)) (and (= two-to-exp-new21 65536.0) (= two-to-exp-p-minus-e-new21 128.0))))
(assert (=> (and (<= 131072.0 abs-new21) (< abs-new21 262144.0)) (and (= two-to-exp-new21 131072.0) (= two-to-exp-p-minus-e-new21 64.0))))
(assert (=> (and (<= 262144.0 abs-new21) (< abs-new21 524288.0)) (and (= two-to-exp-new21 262144.0) (= two-to-exp-p-minus-e-new21 32.0))))
(assert (=> (and (<= 524288.0 abs-new21) (< abs-new21 1048576.0)) (and (= two-to-exp-new21 524288.0) (= two-to-exp-p-minus-e-new21 16.0))))
(assert (=> (and (<= 1048576.0 abs-new21) (< abs-new21 2097152.0)) (and (= two-to-exp-new21 1048576.0) (= two-to-exp-p-minus-e-new21 8.0))))
(assert (=> (and (<= 2097152.0 abs-new21) (< abs-new21 4194304.0)) (and (= two-to-exp-new21 2097152.0) (= two-to-exp-p-minus-e-new21 4.0))))
(assert (=> (and (<= 4194304.0 abs-new21) (< abs-new21 8388608.0)) (and (= two-to-exp-new21 4194304.0) (= two-to-exp-p-minus-e-new21 2.0))))
(assert (=> (and (<= 8388608.0 abs-new21) (< abs-new21 16777216.0)) (and (= two-to-exp-new21 8388608.0) (= two-to-exp-p-minus-e-new21 1.0))))
(assert (=> (and (<= 16777216.0 abs-new21) (< abs-new21 33554432.0)) (and (= two-to-exp-new21 16777216.0) (= two-to-exp-p-minus-e-new21 0.5))))
(assert (=> (and (<= 33554432.0 abs-new21) (< abs-new21 67108864.0)) (and (= two-to-exp-new21 33554432.0) (= two-to-exp-p-minus-e-new21 0.25))))
(assert (=> (and (<= 67108864.0 abs-new21) (< abs-new21 134217728.0)) (and (= two-to-exp-new21 67108864.0) (= two-to-exp-p-minus-e-new21 0.125))))
(assert (=> (and (<= 134217728.0 abs-new21) (< abs-new21 268435456.0)) (and (= two-to-exp-new21 134217728.0) (= two-to-exp-p-minus-e-new21 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new21) (< abs-new21 536870912.0)) (and (= two-to-exp-new21 268435456.0) (= two-to-exp-p-minus-e-new21 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new21) (< abs-new21 1073741824.0)) (and (= two-to-exp-new21 536870912.0) (= two-to-exp-p-minus-e-new21 0.015625))))

(assert (= new21-real (+ a11 a12)))

;(assert (= new21  (* (/ (to_real (to_int (* (/ new21-real two-to-exp-new21) two-to-p))) two-to-p) two-to-exp-new21 )))
(assert (= (* two-to-exp-p-minus-e-new21 new21) (to_real (to_int (* new21-real two-to-exp-p-minus-e-new21)))))

(declare-const new13 Real)

(declare-const abs-new13 Real)
(assert (or (and (<= 1.0  new13) (< new13 1073741824.0)) (and (>= -1.0  new13) (> new13 -1073741824.0))))
(assert (=> (>= new13 0.0) (= abs-new13 new13)));added
(assert (=> (< new13 0.0) (= abs-new13 (- new13))));added
(declare-const new13-real Real)
(declare-const two-to-exp-new13 Real)
(declare-const two-to-exp-p-minus-e-new13 Real)
(assert (=> (and (<= 1.0 abs-new13) (< abs-new13 2.0)) (and (= two-to-exp-new13 1.0) (= two-to-exp-p-minus-e-new13 8388608.0))))
(assert (=> (and (<= 2.0 abs-new13) (< abs-new13 4.0)) (and (= two-to-exp-new13 2.0) (= two-to-exp-p-minus-e-new13 4194304.0))))
(assert (=> (and (<= 4.0 abs-new13) (< abs-new13 8.0)) (and (= two-to-exp-new13 4.0) (= two-to-exp-p-minus-e-new13 2097152.0))))
(assert (=> (and (<= 8.0 abs-new13) (< abs-new13 16.0)) (and (= two-to-exp-new13 8.0) (= two-to-exp-p-minus-e-new13 1048576.0))))
(assert (=> (and (<= 16.0 abs-new13) (< abs-new13 32.0)) (and (= two-to-exp-new13 16.0) (= two-to-exp-p-minus-e-new13 524288.0))))
(assert (=> (and (<= 32.0 abs-new13) (< abs-new13 64.0)) (and (= two-to-exp-new13 32.0) (= two-to-exp-p-minus-e-new13 262144.0))))
(assert (=> (and (<= 64.0 abs-new13) (< abs-new13 128.0)) (and (= two-to-exp-new13 64.0) (= two-to-exp-p-minus-e-new13 131072.0))))
(assert (=> (and (<= 128.0 abs-new13) (< abs-new13 256.0)) (and (= two-to-exp-new13 128.0) (= two-to-exp-p-minus-e-new13 65536.0))))
(assert (=> (and (<= 256.0 abs-new13) (< abs-new13 512.0)) (and (= two-to-exp-new13 256.0) (= two-to-exp-p-minus-e-new13 32768.0))))
(assert (=> (and (<= 512.0 abs-new13) (< abs-new13 1024.0)) (and (= two-to-exp-new13 512.0) (= two-to-exp-p-minus-e-new13 16384.0))))
(assert (=> (and (<= 1024.0 abs-new13) (< abs-new13 2048.0)) (and (= two-to-exp-new13 1024.0) (= two-to-exp-p-minus-e-new13 8192.0))))
(assert (=> (and (<= 2048.0 abs-new13) (< abs-new13 4096.0)) (and (= two-to-exp-new13 2048.0) (= two-to-exp-p-minus-e-new13 4096.0))))
(assert (=> (and (<= 4096.0 abs-new13) (< abs-new13 8192.0)) (and (= two-to-exp-new13 4096.0) (= two-to-exp-p-minus-e-new13 2048.0))))
(assert (=> (and (<= 8192.0 abs-new13) (< abs-new13 16384.0)) (and (= two-to-exp-new13 8192.0) (= two-to-exp-p-minus-e-new13 1024.0))))
(assert (=> (and (<= 16384.0 abs-new13) (< abs-new13 32768.0)) (and (= two-to-exp-new13 16384.0) (= two-to-exp-p-minus-e-new13 512.0))))
(assert (=> (and (<= 32768.0 abs-new13) (< abs-new13 65536.0)) (and (= two-to-exp-new13 32768.0) (= two-to-exp-p-minus-e-new13 256.0))))
(assert (=> (and (<= 65536.0 abs-new13) (< abs-new13 131072.0)) (and (= two-to-exp-new13 65536.0) (= two-to-exp-p-minus-e-new13 128.0))))
(assert (=> (and (<= 131072.0 abs-new13) (< abs-new13 262144.0)) (and (= two-to-exp-new13 131072.0) (= two-to-exp-p-minus-e-new13 64.0))))
(assert (=> (and (<= 262144.0 abs-new13) (< abs-new13 524288.0)) (and (= two-to-exp-new13 262144.0) (= two-to-exp-p-minus-e-new13 32.0))))
(assert (=> (and (<= 524288.0 abs-new13) (< abs-new13 1048576.0)) (and (= two-to-exp-new13 524288.0) (= two-to-exp-p-minus-e-new13 16.0))))
(assert (=> (and (<= 1048576.0 abs-new13) (< abs-new13 2097152.0)) (and (= two-to-exp-new13 1048576.0) (= two-to-exp-p-minus-e-new13 8.0))))
(assert (=> (and (<= 2097152.0 abs-new13) (< abs-new13 4194304.0)) (and (= two-to-exp-new13 2097152.0) (= two-to-exp-p-minus-e-new13 4.0))))
(assert (=> (and (<= 4194304.0 abs-new13) (< abs-new13 8388608.0)) (and (= two-to-exp-new13 4194304.0) (= two-to-exp-p-minus-e-new13 2.0))))
(assert (=> (and (<= 8388608.0 abs-new13) (< abs-new13 16777216.0)) (and (= two-to-exp-new13 8388608.0) (= two-to-exp-p-minus-e-new13 1.0))))
(assert (=> (and (<= 16777216.0 abs-new13) (< abs-new13 33554432.0)) (and (= two-to-exp-new13 16777216.0) (= two-to-exp-p-minus-e-new13 0.5))))
(assert (=> (and (<= 33554432.0 abs-new13) (< abs-new13 67108864.0)) (and (= two-to-exp-new13 33554432.0) (= two-to-exp-p-minus-e-new13 0.25))))
(assert (=> (and (<= 67108864.0 abs-new13) (< abs-new13 134217728.0)) (and (= two-to-exp-new13 67108864.0) (= two-to-exp-p-minus-e-new13 0.125))))
(assert (=> (and (<= 134217728.0 abs-new13) (< abs-new13 268435456.0)) (and (= two-to-exp-new13 134217728.0) (= two-to-exp-p-minus-e-new13 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new13) (< abs-new13 536870912.0)) (and (= two-to-exp-new13 268435456.0) (= two-to-exp-p-minus-e-new13 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new13) (< abs-new13 1073741824.0)) (and (= two-to-exp-new13 536870912.0) (= two-to-exp-p-minus-e-new13 0.015625))))

(assert (= new13-real (+ new20 new21)))

;(assert (= new13  (* (/ (to_real (to_int (* (/ new13-real two-to-exp-new13) two-to-p))) two-to-p) two-to-exp-new13 )))
(assert (= (* two-to-exp-p-minus-e-new13 new13) (to_real (to_int (* new13-real two-to-exp-p-minus-e-new13)))))

(declare-const new11 Real)

(declare-const abs-new11 Real)
(assert (or (and (<= 1.0  new11) (< new11 1073741824.0)) (and (>= -1.0  new11) (> new11 -1073741824.0))))
(assert (=> (>= new11 0.0) (= abs-new11 new11)));added
(assert (=> (< new11 0.0) (= abs-new11 (- new11))));added
(declare-const new11-real Real)
(declare-const two-to-exp-new11 Real)
(declare-const two-to-exp-p-minus-e-new11 Real)
(assert (=> (and (<= 1.0 abs-new11) (< abs-new11 2.0)) (and (= two-to-exp-new11 1.0) (= two-to-exp-p-minus-e-new11 8388608.0))))
(assert (=> (and (<= 2.0 abs-new11) (< abs-new11 4.0)) (and (= two-to-exp-new11 2.0) (= two-to-exp-p-minus-e-new11 4194304.0))))
(assert (=> (and (<= 4.0 abs-new11) (< abs-new11 8.0)) (and (= two-to-exp-new11 4.0) (= two-to-exp-p-minus-e-new11 2097152.0))))
(assert (=> (and (<= 8.0 abs-new11) (< abs-new11 16.0)) (and (= two-to-exp-new11 8.0) (= two-to-exp-p-minus-e-new11 1048576.0))))
(assert (=> (and (<= 16.0 abs-new11) (< abs-new11 32.0)) (and (= two-to-exp-new11 16.0) (= two-to-exp-p-minus-e-new11 524288.0))))
(assert (=> (and (<= 32.0 abs-new11) (< abs-new11 64.0)) (and (= two-to-exp-new11 32.0) (= two-to-exp-p-minus-e-new11 262144.0))))
(assert (=> (and (<= 64.0 abs-new11) (< abs-new11 128.0)) (and (= two-to-exp-new11 64.0) (= two-to-exp-p-minus-e-new11 131072.0))))
(assert (=> (and (<= 128.0 abs-new11) (< abs-new11 256.0)) (and (= two-to-exp-new11 128.0) (= two-to-exp-p-minus-e-new11 65536.0))))
(assert (=> (and (<= 256.0 abs-new11) (< abs-new11 512.0)) (and (= two-to-exp-new11 256.0) (= two-to-exp-p-minus-e-new11 32768.0))))
(assert (=> (and (<= 512.0 abs-new11) (< abs-new11 1024.0)) (and (= two-to-exp-new11 512.0) (= two-to-exp-p-minus-e-new11 16384.0))))
(assert (=> (and (<= 1024.0 abs-new11) (< abs-new11 2048.0)) (and (= two-to-exp-new11 1024.0) (= two-to-exp-p-minus-e-new11 8192.0))))
(assert (=> (and (<= 2048.0 abs-new11) (< abs-new11 4096.0)) (and (= two-to-exp-new11 2048.0) (= two-to-exp-p-minus-e-new11 4096.0))))
(assert (=> (and (<= 4096.0 abs-new11) (< abs-new11 8192.0)) (and (= two-to-exp-new11 4096.0) (= two-to-exp-p-minus-e-new11 2048.0))))
(assert (=> (and (<= 8192.0 abs-new11) (< abs-new11 16384.0)) (and (= two-to-exp-new11 8192.0) (= two-to-exp-p-minus-e-new11 1024.0))))
(assert (=> (and (<= 16384.0 abs-new11) (< abs-new11 32768.0)) (and (= two-to-exp-new11 16384.0) (= two-to-exp-p-minus-e-new11 512.0))))
(assert (=> (and (<= 32768.0 abs-new11) (< abs-new11 65536.0)) (and (= two-to-exp-new11 32768.0) (= two-to-exp-p-minus-e-new11 256.0))))
(assert (=> (and (<= 65536.0 abs-new11) (< abs-new11 131072.0)) (and (= two-to-exp-new11 65536.0) (= two-to-exp-p-minus-e-new11 128.0))))
(assert (=> (and (<= 131072.0 abs-new11) (< abs-new11 262144.0)) (and (= two-to-exp-new11 131072.0) (= two-to-exp-p-minus-e-new11 64.0))))
(assert (=> (and (<= 262144.0 abs-new11) (< abs-new11 524288.0)) (and (= two-to-exp-new11 262144.0) (= two-to-exp-p-minus-e-new11 32.0))))
(assert (=> (and (<= 524288.0 abs-new11) (< abs-new11 1048576.0)) (and (= two-to-exp-new11 524288.0) (= two-to-exp-p-minus-e-new11 16.0))))
(assert (=> (and (<= 1048576.0 abs-new11) (< abs-new11 2097152.0)) (and (= two-to-exp-new11 1048576.0) (= two-to-exp-p-minus-e-new11 8.0))))
(assert (=> (and (<= 2097152.0 abs-new11) (< abs-new11 4194304.0)) (and (= two-to-exp-new11 2097152.0) (= two-to-exp-p-minus-e-new11 4.0))))
(assert (=> (and (<= 4194304.0 abs-new11) (< abs-new11 8388608.0)) (and (= two-to-exp-new11 4194304.0) (= two-to-exp-p-minus-e-new11 2.0))))
(assert (=> (and (<= 8388608.0 abs-new11) (< abs-new11 16777216.0)) (and (= two-to-exp-new11 8388608.0) (= two-to-exp-p-minus-e-new11 1.0))))
(assert (=> (and (<= 16777216.0 abs-new11) (< abs-new11 33554432.0)) (and (= two-to-exp-new11 16777216.0) (= two-to-exp-p-minus-e-new11 0.5))))
(assert (=> (and (<= 33554432.0 abs-new11) (< abs-new11 67108864.0)) (and (= two-to-exp-new11 33554432.0) (= two-to-exp-p-minus-e-new11 0.25))))
(assert (=> (and (<= 67108864.0 abs-new11) (< abs-new11 134217728.0)) (and (= two-to-exp-new11 67108864.0) (= two-to-exp-p-minus-e-new11 0.125))))
(assert (=> (and (<= 134217728.0 abs-new11) (< abs-new11 268435456.0)) (and (= two-to-exp-new11 134217728.0) (= two-to-exp-p-minus-e-new11 0.0625))))
(assert (=> (and (<= 268435456.0 abs-new11) (< abs-new11 536870912.0)) (and (= two-to-exp-new11 268435456.0) (= two-to-exp-p-minus-e-new11 0.03125))))
(assert (=> (and (<= 536870912.0 abs-new11) (< abs-new11 1073741824.0)) (and (= two-to-exp-new11 536870912.0) (= two-to-exp-p-minus-e-new11 0.015625))))

(assert (= new11-real (+ new12 new13)))

;(assert (= new11  (* (/ (to_real (to_int (* (/ new11-real two-to-exp-new11) two-to-p))) two-to-p) two-to-exp-new11 )))
(assert (= (* two-to-exp-p-minus-e-new11 new11) (to_real (to_int (* new11-real two-to-exp-p-minus-e-new11)))))

;; Skeleton:
(assert (> a1 0.0))
(assert (> a2 0.0))
(assert (> a3 0.0))
(assert (> a4 0.0))
(assert (> a5 0.0))
(assert (> a6 0.0))
(assert (> a7 0.0))
(assert (> a8 0.0))
(assert (> a9 0.0))
(assert (> a10 0.0))
(assert (> a11 0.0))
(assert (> a12 0.0))
;(assert (not (= new new11)))
;(assert (> new 0.0))
;(assert (> new1 0.0))
;(assert (> new2 0.0))
;(assert (> new3 0.0))
;(assert (> new4 0.0))
;(assert (> new5 0.0))
;(assert (> new6 0.0))
;(assert (> new7 0.0))
;(assert (> new8 0.0))
;(assert (> new9 0.0))
;(assert (> new10 0.0))
;(assert (> new11 0.0))
(assert (> new11 (+ new 0.001)))
(check-sat)
(get-model)