Bug in Z3 version 4.4.1

test.smt2

(define-fun T ((%init Bool) ($signal$0 Real) ($errorA$0 Real) ($errorB$0 Real) ($errorC$0 Real) ($difference$0 Real) ($sensedA$0 Real) ($sensedB$0 Real) ($sensedC$0 Real) ($equalizedA$0 Real) ($equalizedB$0 Real) ($equalizedC$0 Real) ($pre_output$0 Real) ($centering$0 Real) ($pre_equalizedA$0 Real) ($pre_equalizedB$0 Real) ($pre_equalizedC$0 Real) ($lemmaA$0 Bool) ($lemmaB$0 Bool) ($lemmaC$0 Bool) ($ok1$0 Bool) ($ok2$0 Bool) ($ok3$0 Bool) ($ok4$0 Bool) ($ok5$0 Bool) ($abs~0.out$0 Real) ($abs~1.out$0 Real) ($abs~2.out$0 Real) ($middleValue~0.out$0 Real) ($equalization~0.equalization_value$0 Real) ($equalization~0.sum1$0 Real) ($equalization~0.sum2$0 Real) ($equalization~1.equalization_value$0 Real) ($equalization~1.sum1$0 Real) ($equalization~1.sum2$0 Real) ($equalization~2.equalization_value$0 Real) ($equalization~2.sum1$0 Real) ($equalization~2.sum2$0 Real) ($middleValue~1.out$0 Real) ($abs~3.a$0 Real) ($abs~3.out$0 Real) ($abs~4.a$0 Real) ($abs~4.out$0 Real) ($abs~5.a$0 Real) ($abs~5.out$0 Real) ($abs~6.out$0 Real) ($abs~7.a$0 Real) ($abs~7.out$0 Real) ($abs~8.a$0 Real) ($abs~8.out$0 Real) ($abs~9.a$0 Real) ($abs~9.out$0 Real) ($abs~10.a$0 Real) ($abs~10.out$0 Real) ($abs~11.a$0 Real) ($abs~11.out$0 Real) ($equalization~0.saturation~0.lower_limit$0 Real) ($equalization~0.saturation~0.out$0 Real) ($equalization~0.saturation~1.lower_limit$0 Real) ($equalization~0.saturation~1.out$0 Real) ($equalization~1.saturation~0.lower_limit$0 Real) ($equalization~1.saturation~0.out$0 Real) ($equalization~1.saturation~1.lower_limit$0 Real) ($equalization~1.saturation~1.out$0 Real) ($equalization~2.saturation~0.lower_limit$0 Real) ($equalization~2.saturation~0.out$0 Real) ($equalization~2.saturation~1.lower_limit$0 Real) ($equalization~2.saturation~1.out$0 Real) ($signal$1 Real) ($errorA$1 Real) ($errorB$1 Real) ($errorC$1 Real) ($difference$1 Real) ($sensedA$1 Real) ($sensedB$1 Real) ($sensedC$1 Real) ($equalizedA$1 Real) ($equalizedB$1 Real) ($equalizedC$1 Real) ($pre_output$1 Real) ($centering$1 Real) ($pre_equalizedA$1 Real) ($pre_equalizedB$1 Real) ($pre_equalizedC$1 Real) ($lemmaA$1 Bool) ($lemmaB$1 Bool) ($lemmaC$1 Bool) ($ok1$1 Bool) ($ok2$1 Bool) ($ok3$1 Bool) ($ok4$1 Bool) ($ok5$1 Bool) ($abs~0.out$1 Real) ($abs~1.out$1 Real) ($abs~2.out$1 Real) ($middleValue~0.out$1 Real) ($equalization~0.equalization_value$1 Real) ($equalization~0.sum1$1 Real) ($equalization~0.sum2$1 Real) ($equalization~1.equalization_value$1 Real) ($equalization~1.sum1$1 Real) ($equalization~1.sum2$1 Real) ($equalization~2.equalization_value$1 Real) ($equalization~2.sum1$1 Real) ($equalization~2.sum2$1 Real) ($middleValue~1.out$1 Real) ($abs~3.a$1 Real) ($abs~3.out$1 Real) ($abs~4.a$1 Real) ($abs~4.out$1 Real) ($abs~5.a$1 Real) ($abs~5.out$1 Real) ($abs~6.out$1 Real) ($abs~7.a$1 Real) ($abs~7.out$1 Real) ($abs~8.a$1 Real) ($abs~8.out$1 Real) ($abs~9.a$1 Real) ($abs~9.out$1 Real) ($abs~10.a$1 Real) ($abs~10.out$1 Real) ($abs~11.a$1 Real) ($abs~11.out$1 Real) ($equalization~0.saturation~0.lower_limit$1 Real) ($equalization~0.saturation~0.out$1 Real) ($equalization~0.saturation~1.lower_limit$1 Real) ($equalization~0.saturation~1.out$1 Real) ($equalization~1.saturation~0.lower_limit$1 Real) ($equalization~1.saturation~0.out$1 Real) ($equalization~1.saturation~1.lower_limit$1 Real) ($equalization~1.saturation~1.out$1 Real) ($equalization~2.saturation~0.lower_limit$1 Real) ($equalization~2.saturation~0.out$1 Real) ($equalization~2.saturation~1.lower_limit$1 Real) ($equalization~2.saturation~1.out$1 Real)) Bool (and (= $abs~0.out$1 (ite (>= $errorA$1 (/ 0 10)) $errorA$1 (- 0 $errorA$1))) (= $abs~1.out$1 (ite (>= $errorB$1 (/ 0 10)) $errorB$1 (- 0 $errorB$1))) (= $abs~2.out$1 (ite (>= $errorC$1 (/ 0 10)) $errorC$1 (- 0 $errorC$1))) (= $sensedA$1 (+ $signal$1 $errorA$1)) (= $sensedB$1 (+ $signal$1 $errorB$1)) (= $sensedC$1 (+ $signal$1 $errorC$1)) (= $centering$1 (ite %init (/ 0 10) $middleValue~0.out$0)) (= $pre_output$1 (ite %init (/ 0 10) $middleValue~1.out$0)) (= $pre_equalizedA$1 (ite %init (/ 0 10) $equalizedA$0)) (= $pre_equalizedB$1 (ite %init (/ 0 10) $equalizedB$0)) (= $pre_equalizedC$1 (ite %init (/ 0 10) $equalizedC$0)) (= $equalizedA$1 (- $sensedA$1 $equalization~0.equalization_value$1)) (= $equalizedB$1 (- $sensedB$1 $equalization~1.equalization_value$1)) (= $equalizedC$1 (- $sensedC$1 $equalization~2.equalization_value$1)) (= $difference$1 (- $middleValue~1.out$1 $signal$1)) (= $lemmaA$1 (< $abs~3.out$1 (* (/ 20 10) (/ 15 100)))) (= $lemmaB$1 (< $abs~4.out$1 (* (/ 20 10) (/ 15 100)))) (= $lemmaC$1 (< $abs~5.out$1 (* (/ 20 10) (/ 15 100)))) (= $ok1$1 (< $abs~6.out$1 $abs~7.out$1)) (= $ok2$1 (< $abs~6.out$1 $abs~8.out$1)) (= $ok3$1 (< $abs~6.out$1 $abs~9.out$1)) (= $ok4$1 (< $abs~6.out$1 $abs~10.out$1)) (= $ok5$1 (< $abs~6.out$1 $abs~11.out$1)) (= $middleValue~0.out$1 (ite (< $equalization~0.equalization_value$1 $equalization~1.equalization_value$1) (ite (< $equalization~1.equalization_value$1 $equalization~2.equalization_value$1) $equalization~1.equalization_value$1 (ite (< $equalization~2.equalization_value$1 $equalization~0.equalization_value$1) $equalization~0.equalization_value$1 $equalization~2.equalization_value$1)) (ite (< $equalization~0.equalization_value$1 $equalization~2.equalization_value$1) $equalization~0.equalization_value$1 (ite (< $equalization~2.equalization_value$1 $equalization~1.equalization_value$1) $equalization~1.equalization_value$1 $equalization~2.equalization_value$1)))) (= $equalization~0.sum1$1 (- $pre_equalizedA$1 $pre_output$1)) (= $equalization~0.sum2$1 (- $equalization~0.saturation~0.out$1 $equalization~0.saturation~1.out$1)) (= $equalization~0.equalization_value$1 (+ (* $equalization~0.sum2$1 (/ 2 10)) (ite %init (/ 0 10) $equalization~0.equalization_value$0))) (= $equalization~1.sum1$1 (- $pre_equalizedB$1 $pre_output$1)) (= $equalization~1.sum2$1 (- $equalization~1.saturation~0.out$1 $equalization~1.saturation~1.out$1)) (= $equalization~1.equalization_value$1 (+ (* $equalization~1.sum2$1 (/ 2 10)) (ite %init (/ 0 10) $equalization~1.equalization_value$0))) (= $equalization~2.sum1$1 (- $pre_equalizedC$1 $pre_output$1)) (= $equalization~2.sum2$1 (- $equalization~2.saturation~0.out$1 $equalization~2.saturation~1.out$1)) (= $equalization~2.equalization_value$1 (+ (* $equalization~2.sum2$1 (/ 2 10)) (ite %init (/ 0 10) $equalization~2.equalization_value$0))) (= $middleValue~1.out$1 (ite (< $equalizedA$1 $equalizedB$1) (ite (< $equalizedB$1 $equalizedC$1) $equalizedB$1 (ite (< $equalizedC$1 $equalizedA$1) $equalizedA$1 $equalizedC$1)) (ite (< $equalizedA$1 $equalizedC$1) $equalizedA$1 (ite (< $equalizedC$1 $equalizedB$1) $equalizedB$1 $equalizedC$1)))) (= $abs~3.a$1 (- $equalizedA$1 $sensedA$1)) (= $abs~3.out$1 (ite (>= $abs~3.a$1 (/ 0 10)) $abs~3.a$1 (- 0 $abs~3.a$1))) (= $abs~4.a$1 (- $equalizedB$1 $sensedB$1)) (= $abs~4.out$1 (ite (>= $abs~4.a$1 (/ 0 10)) $abs~4.a$1 (- 0 $abs~4.a$1))) (= $abs~5.a$1 (- $equalizedC$1 $sensedC$1)) (= $abs~5.out$1 (ite (>= $abs~5.a$1 (/ 0 10)) $abs~5.a$1 (- 0 $abs~5.a$1))) (= $abs~6.out$1 (ite (>= $difference$1 (/ 0 10)) $difference$1 (- 0 $difference$1))) (= $abs~7.a$1 (* (/ 15 100) (/ 30 10))) (= $abs~7.out$1 (ite (>= $abs~7.a$1 (/ 0 10)) $abs~7.a$1 (- 0 $abs~7.a$1))) (= $abs~8.a$1 (* (/ 15 100) (/ 26 10))) (= $abs~8.out$1 (ite (>= $abs~8.a$1 (/ 0 10)) $abs~8.a$1 (- 0 $abs~8.a$1))) (= $abs~9.a$1 (* (/ 15 100) (/ 245 100))) (= $abs~9.out$1 (ite (>= $abs~9.a$1 (/ 0 10)) $abs~9.a$1 (- 0 $abs~9.a$1))) (= $abs~10.a$1 (* (/ 15 100) (/ 235 100))) (= $abs~10.out$1 (ite (>= $abs~10.a$1 (/ 0 10)) $abs~10.a$1 (- 0 $abs~10.a$1))) (= $abs~11.a$1 (* (/ 15 100) (/ 23 10))) (= $abs~11.out$1 (ite (>= $abs~11.a$1 (/ 0 10)) $abs~11.a$1 (- 0 $abs~11.a$1))) (= $equalization~0.saturation~0.lower_limit$1 (- 0 (/ 5 10))) (= $equalization~0.saturation~0.out$1 (ite (< $equalization~0.sum1$1 $equalization~0.saturation~0.lower_limit$1) $equalization~0.saturation~0.lower_limit$1 (ite (> $equalization~0.sum1$1 (/ 5 10)) (/ 5 10) $equalization~0.sum1$1))) (= $equalization~0.saturation~1.lower_limit$1 (- 0 (/ 25 100))) (= $equalization~0.saturation~1.out$1 (ite (< $centering$1 $equalization~0.saturation~1.lower_limit$1) $equalization~0.saturation~1.lower_limit$1 (ite (> $centering$1 (/ 25 100)) (/ 25 100) $centering$1))) (= $equalization~1.saturation~0.lower_limit$1 (- 0 (/ 5 10))) (= $equalization~1.saturation~0.out$1 (ite (< $equalization~1.sum1$1 $equalization~1.saturation~0.lower_limit$1) $equalization~1.saturation~0.lower_limit$1 (ite (> $equalization~1.sum1$1 (/ 5 10)) (/ 5 10) $equalization~1.sum1$1))) (= $equalization~1.saturation~1.lower_limit$1 (- 0 (/ 25 100))) (= $equalization~1.saturation~1.out$1 (ite (< $centering$1 $equalization~1.saturation~1.lower_limit$1) $equalization~1.saturation~1.lower_limit$1 (ite (> $centering$1 (/ 25 100)) (/ 25 100) $centering$1))) (= $equalization~2.saturation~0.lower_limit$1 (- 0 (/ 5 10))) (= $equalization~2.saturation~0.out$1 (ite (< $equalization~2.sum1$1 $equalization~2.saturation~0.lower_limit$1) $equalization~2.saturation~0.lower_limit$1 (ite (> $equalization~2.sum1$1 (/ 5 10)) (/ 5 10) $equalization~2.sum1$1))) (= $equalization~2.saturation~1.lower_limit$1 (- 0 (/ 25 100))) (= $equalization~2.saturation~1.out$1 (ite (< $centering$1 $equalization~2.saturation~1.lower_limit$1) $equalization~2.saturation~1.lower_limit$1 (ite (> $centering$1 (/ 25 100)) (/ 25 100) $centering$1))) (<= $abs~0.out$1 (/ 15 100)) (<= $abs~1.out$1 (/ 15 100)) (<= $abs~2.out$1 (/ 15 100))))

(declare-fun %init () Bool)
(declare-fun $signal$~1 () Real)
(declare-fun $errorA$~1 () Real)
(declare-fun $errorB$~1 () Real)
(declare-fun $errorC$~1 () Real)
(declare-fun $difference$~1 () Real)
(declare-fun $sensedA$~1 () Real)
(declare-fun $sensedB$~1 () Real)
(declare-fun $sensedC$~1 () Real)
(declare-fun $equalizedA$~1 () Real)
(declare-fun $equalizedB$~1 () Real)
(declare-fun $equalizedC$~1 () Real)
(declare-fun $pre_output$~1 () Real)
(declare-fun $centering$~1 () Real)
(declare-fun $pre_equalizedA$~1 () Real)
(declare-fun $pre_equalizedB$~1 () Real)
(declare-fun $pre_equalizedC$~1 () Real)
(declare-fun $lemmaA$~1 () Bool)
(declare-fun $lemmaB$~1 () Bool)
(declare-fun $lemmaC$~1 () Bool)
(declare-fun $ok1$~1 () Bool)
(declare-fun $ok2$~1 () Bool)
(declare-fun $ok3$~1 () Bool)
(declare-fun $ok4$~1 () Bool)
(declare-fun $ok5$~1 () Bool)
(declare-fun $abs~0.out$~1 () Real)
(declare-fun $abs~1.out$~1 () Real)
(declare-fun $abs~2.out$~1 () Real)
(declare-fun $middleValue~0.out$~1 () Real)
(declare-fun $equalization~0.equalization_value$~1 () Real)
(declare-fun $equalization~0.sum1$~1 () Real)
(declare-fun $equalization~0.sum2$~1 () Real)
(declare-fun $equalization~1.equalization_value$~1 () Real)
(declare-fun $equalization~1.sum1$~1 () Real)
(declare-fun $equalization~1.sum2$~1 () Real)
(declare-fun $equalization~2.equalization_value$~1 () Real)
(declare-fun $equalization~2.sum1$~1 () Real)
(declare-fun $equalization~2.sum2$~1 () Real)
(declare-fun $middleValue~1.out$~1 () Real)
(declare-fun $abs~3.a$~1 () Real)
(declare-fun $abs~3.out$~1 () Real)
(declare-fun $abs~4.a$~1 () Real)
(declare-fun $abs~4.out$~1 () Real)
(declare-fun $abs~5.a$~1 () Real)
(declare-fun $abs~5.out$~1 () Real)
(declare-fun $abs~6.out$~1 () Real)
(declare-fun $abs~7.a$~1 () Real)
(declare-fun $abs~7.out$~1 () Real)
(declare-fun $abs~8.a$~1 () Real)
(declare-fun $abs~8.out$~1 () Real)
(declare-fun $abs~9.a$~1 () Real)
(declare-fun $abs~9.out$~1 () Real)
(declare-fun $abs~10.a$~1 () Real)
(declare-fun $abs~10.out$~1 () Real)
(declare-fun $abs~11.a$~1 () Real)
(declare-fun $abs~11.out$~1 () Real)
(declare-fun $equalization~0.saturation~0.lower_limit$~1 () Real)
(declare-fun $equalization~0.saturation~0.out$~1 () Real)
(declare-fun $equalization~0.saturation~1.lower_limit$~1 () Real)
(declare-fun $equalization~0.saturation~1.out$~1 () Real)
(declare-fun $equalization~1.saturation~0.lower_limit$~1 () Real)
(declare-fun $equalization~1.saturation~0.out$~1 () Real)
(declare-fun $equalization~1.saturation~1.lower_limit$~1 () Real)
(declare-fun $equalization~1.saturation~1.out$~1 () Real)
(declare-fun $equalization~2.saturation~0.lower_limit$~1 () Real)
(declare-fun $equalization~2.saturation~0.out$~1 () Real)
(declare-fun $equalization~2.saturation~1.lower_limit$~1 () Real)
(declare-fun $equalization~2.saturation~1.out$~1 () Real)
(declare-fun $signal$0 () Real)
(declare-fun $errorA$0 () Real)
(declare-fun $errorB$0 () Real)
(declare-fun $errorC$0 () Real)
(declare-fun $difference$0 () Real)
(declare-fun $sensedA$0 () Real)
(declare-fun $sensedB$0 () Real)
(declare-fun $sensedC$0 () Real)
(declare-fun $equalizedA$0 () Real)
(declare-fun $equalizedB$0 () Real)
(declare-fun $equalizedC$0 () Real)
(declare-fun $pre_output$0 () Real)
(declare-fun $centering$0 () Real)
(declare-fun $pre_equalizedA$0 () Real)
(declare-fun $pre_equalizedB$0 () Real)
(declare-fun $pre_equalizedC$0 () Real)
(declare-fun $lemmaA$0 () Bool)
(declare-fun $lemmaB$0 () Bool)
(declare-fun $lemmaC$0 () Bool)
(declare-fun $ok1$0 () Bool)
(declare-fun $ok2$0 () Bool)
(declare-fun $ok3$0 () Bool)
(declare-fun $ok4$0 () Bool)
(declare-fun $ok5$0 () Bool)
(declare-fun $abs~0.out$0 () Real)
(declare-fun $abs~1.out$0 () Real)
(declare-fun $abs~2.out$0 () Real)
(declare-fun $middleValue~0.out$0 () Real)
(declare-fun $equalization~0.equalization_value$0 () Real)
(declare-fun $equalization~0.sum1$0 () Real)
(declare-fun $equalization~0.sum2$0 () Real)
(declare-fun $equalization~1.equalization_value$0 () Real)
(declare-fun $equalization~1.sum1$0 () Real)
(declare-fun $equalization~1.sum2$0 () Real)
(declare-fun $equalization~2.equalization_value$0 () Real)
(declare-fun $equalization~2.sum1$0 () Real)
(declare-fun $equalization~2.sum2$0 () Real)
(declare-fun $middleValue~1.out$0 () Real)
(declare-fun $abs~3.a$0 () Real)
(declare-fun $abs~3.out$0 () Real)
(declare-fun $abs~4.a$0 () Real)
(declare-fun $abs~4.out$0 () Real)
(declare-fun $abs~5.a$0 () Real)
(declare-fun $abs~5.out$0 () Real)
(declare-fun $abs~6.out$0 () Real)
(declare-fun $abs~7.a$0 () Real)
(declare-fun $abs~7.out$0 () Real)
(declare-fun $abs~8.a$0 () Real)
(declare-fun $abs~8.out$0 () Real)
(declare-fun $abs~9.a$0 () Real)
(declare-fun $abs~9.out$0 () Real)
(declare-fun $abs~10.a$0 () Real)
(declare-fun $abs~10.out$0 () Real)
(declare-fun $abs~11.a$0 () Real)
(declare-fun $abs~11.out$0 () Real)
(declare-fun $equalization~0.saturation~0.lower_limit$0 () Real)
(declare-fun $equalization~0.saturation~0.out$0 () Real)
(declare-fun $equalization~0.saturation~1.lower_limit$0 () Real)
(declare-fun $equalization~0.saturation~1.out$0 () Real)
(declare-fun $equalization~1.saturation~0.lower_limit$0 () Real)
(declare-fun $equalization~1.saturation~0.out$0 () Real)
(declare-fun $equalization~1.saturation~1.lower_limit$0 () Real)
(declare-fun $equalization~1.saturation~1.out$0 () Real)
(declare-fun $equalization~2.saturation~0.lower_limit$0 () Real)
(declare-fun $equalization~2.saturation~0.out$0 () Real)
(declare-fun $equalization~2.saturation~1.lower_limit$0 () Real)
(declare-fun $equalization~2.saturation~1.out$0 () Real)

;; Comment this out and the final check-sat changes from UNSAT to SAT
(push 1)

(assert (T true $signal$~1 $errorA$~1 $errorB$~1 $errorC$~1 $difference$~1 $sensedA$~1 $sensedB$~1 $sensedC$~1 $equalizedA$~1 $equalizedB$~1 $equalizedC$~1 $pre_output$~1 $centering$~1 $pre_equalizedA$~1 $pre_equalizedB$~1 $pre_equalizedC$~1 $lemmaA$~1 $lemmaB$~1 $lemmaC$~1 $ok1$~1 $ok2$~1 $ok3$~1 $ok4$~1 $ok5$~1 $abs~0.out$~1 $abs~1.out$~1 $abs~2.out$~1 $middleValue~0.out$~1 $equalization~0.equalization_value$~1 $equalization~0.sum1$~1 $equalization~0.sum2$~1 $equalization~1.equalization_value$~1 $equalization~1.sum1$~1 $equalization~1.sum2$~1 $equalization~2.equalization_value$~1 $equalization~2.sum1$~1 $equalization~2.sum2$~1 $middleValue~1.out$~1 $abs~3.a$~1 $abs~3.out$~1 $abs~4.a$~1 $abs~4.out$~1 $abs~5.a$~1 $abs~5.out$~1 $abs~6.out$~1 $abs~7.a$~1 $abs~7.out$~1 $abs~8.a$~1 $abs~8.out$~1 $abs~9.a$~1 $abs~9.out$~1 $abs~10.a$~1 $abs~10.out$~1 $abs~11.a$~1 $abs~11.out$~1 $equalization~0.saturation~0.lower_limit$~1 $equalization~0.saturation~0.out$~1 $equalization~0.saturation~1.lower_limit$~1 $equalization~0.saturation~1.out$~1 $equalization~1.saturation~0.lower_limit$~1 $equalization~1.saturation~0.out$~1 $equalization~1.saturation~1.lower_limit$~1 $equalization~1.saturation~1.out$~1 $equalization~2.saturation~0.lower_limit$~1 $equalization~2.saturation~0.out$~1 $equalization~2.saturation~1.lower_limit$~1 $equalization~2.saturation~1.out$~1 $signal$0 $errorA$0 $errorB$0 $errorC$0 $difference$0 $sensedA$0 $sensedB$0 $sensedC$0 $equalizedA$0 $equalizedB$0 $equalizedC$0 $pre_output$0 $centering$0 $pre_equalizedA$0 $pre_equalizedB$0 $pre_equalizedC$0 $lemmaA$0 $lemmaB$0 $lemmaC$0 $ok1$0 $ok2$0 $ok3$0 $ok4$0 $ok5$0 $abs~0.out$0 $abs~1.out$0 $abs~2.out$0 $middleValue~0.out$0 $equalization~0.equalization_value$0 $equalization~0.sum1$0 $equalization~0.sum2$0 $equalization~1.equalization_value$0 $equalization~1.sum1$0 $equalization~1.sum2$0 $equalization~2.equalization_value$0 $equalization~2.sum1$0 $equalization~2.sum2$0 $middleValue~1.out$0 $abs~3.a$0 $abs~3.out$0 $abs~4.a$0 $abs~4.out$0 $abs~5.a$0 $abs~5.out$0 $abs~6.out$0 $abs~7.a$0 $abs~7.out$0 $abs~8.a$0 $abs~8.out$0 $abs~9.a$0 $abs~9.out$0 $abs~10.a$0 $abs~10.out$0 $abs~11.a$0 $abs~11.out$0 $equalization~0.saturation~0.lower_limit$0 $equalization~0.saturation~0.out$0 $equalization~0.saturation~1.lower_limit$0 $equalization~0.saturation~1.out$0 $equalization~1.saturation~0.lower_limit$0 $equalization~1.saturation~0.out$0 $equalization~1.saturation~1.lower_limit$0 $equalization~1.saturation~1.out$0 $equalization~2.saturation~0.lower_limit$0 $equalization~2.saturation~0.out$0 $equalization~2.saturation~1.lower_limit$0 $equalization~2.saturation~1.out$0))
(check-sat)