From 20690ea6d4b01b54d376821f241d76b5a56327f9 Mon Sep 17 00:00:00 2001 From: Lucas Weitzendorf Date: Fri, 29 Apr 2022 17:21:05 +0200 Subject: [PATCH 1/3] Added bug directory and first confirmed bug --- bugs/config-1.txt | 895 +++++++++++++++++++++++++++++++++++++++++++++ bugs/z3/nra-1.smt2 | 25 ++ 2 files changed, 920 insertions(+) create mode 100644 bugs/config-1.txt create mode 100644 bugs/z3/nra-1.smt2 diff --git a/bugs/config-1.txt b/bugs/config-1.txt new file mode 100644 index 0000000..4098f3c --- /dev/null +++ b/bugs/config-1.txt @@ -0,0 +1,895 @@ +; Generated with: https://github.com/nicdard/fusion-function-generator +; 30 functions (number of #begin ... #end blocks) +; 25 operators per function + +#begin +(declare-const z Real) +(declare-const x Real) +(declare-const y Real) +(declare-const c24 Real) +(declare-const c23 Real) +(declare-const c22 Real) +(declare-const c21 Real) +(declare-const c20 Real) +(declare-const c19 Real) +(declare-const c18 Real) +(declare-const c17 Real) +(declare-const c16 Real) +(declare-const c15 Real) +(declare-const c14 Real) +(declare-const c13 Real) +(declare-const c12 Real) +(declare-const c11 Real) +(declare-const c10 Real) +(declare-const c9 Real) +(declare-const c8 Real) +(declare-const c7 Real) +(declare-const c6 Real) +(declare-const c5 Real) +(declare-const c4 Real) +(declare-const c3 Real) +(declare-const c2 Real) +(declare-const c1 Real) +(assert (= z (/ (* (+ (* c24 (- (/ (/ (* x (* (* c23 (* c22 (- c21 c20))) (/ (* (+ (- (* c19 (* (+ (+ y c18) c17) (- (+ (/ (+ (+ c16 c15) c14) c13) c12) c11))) c10) c9) c8) c7))) c6) c5) c4)) c3) c2) c1))) +(assert (= x (/ (* (* (+ (/ (- (/ (* z c1) c2) c3) c24) c4) c5) c6) (* (* c23 (* c22 (- c21 c20))) (/ (* (+ (- (* c19 (* (+ (+ y c18) c17) (- (+ (/ (+ (+ c16 c15) c14) c13) c12) c11))) c10) c9) c8) c7))))) +(assert (= y (- (- (/ (/ (+ (- (/ (* (/ (/ (* (* (+ (/ (- (/ (* z c1) c2) c3) c24) c4) c5) c6) x) (* c23 (* c22 (- c21 c20)))) c7) c8) c9) c10) c19) (- (+ (/ (+ (+ c16 c15) c14) c13) c12) c11)) c17) c18))) +#end + +#begin +(declare-const z Bool) +(declare-const x Bool) +(declare-const y Bool) +(declare-const c14 Bool) +(declare-const c13 Bool) +(declare-const c12 Bool) +(declare-const c11 Bool) +(declare-const c10 Bool) +(declare-const c9 Bool) +(declare-const c8 Bool) +(declare-const c7 Bool) +(declare-const c6 Bool) +(declare-const c5 Bool) +(declare-const c4 Bool) +(declare-const c3 Bool) +(declare-const c2 Bool) +(declare-const c1 Bool) +(assert (= z (xor x (not (not (xor y (xor (not c14) (xor (not c13) (xor c12 (not (not (not (not (not (not (xor (not c11) (not (not (xor c10 (not (not (not (xor c9 (xor (xor c8 c7) (xor (xor (xor c6 (xor (xor (not (not c5)) c4) c3)) c2) (not c1)))))))))))))))))))))))))) +(assert (= x (xor (not (not (xor y (xor (not c14) (xor (not c13) (xor c12 (not (not (not (not (not (not (xor (not c11) (not (not (xor c10 (not (not (not (xor c9 (xor (xor c8 c7) (xor (xor (xor c6 (xor (xor (not (not c5)) c4) c3)) c2) (not c1))))))))))))))))))))))) z))) +(assert (= y (xor (xor (not c14) (xor (not c13) (xor c12 (not (not (not (not (not (not (xor (not c11) (not (not (xor c10 (not (not (not (xor c9 (xor (xor c8 c7) (xor (xor (xor c6 (xor (xor (not (not c5)) c4) c3)) c2) (not c1)))))))))))))))))))) (not (not (xor x z)))))) +#end + +#begin +(declare-const z Bool) +(declare-const x Bool) +(declare-const y Bool) +(declare-const c16 Bool) +(declare-const c15 Bool) +(declare-const c14 Bool) +(declare-const c13 Bool) +(declare-const c12 Bool) +(declare-const c11 Bool) +(declare-const c10 Bool) +(declare-const c9 Bool) +(declare-const c8 Bool) +(declare-const c7 Bool) +(declare-const c6 Bool) +(declare-const c5 Bool) +(declare-const c4 Bool) +(declare-const c3 Bool) +(declare-const c2 Bool) +(declare-const c1 Bool) +(assert (= z (xor (xor c16 c15) (xor (not c14) (not (xor (xor (xor c13 c12) c11) (not (xor (not (not c10)) (xor (xor (not x) c9) (xor (not c8) (xor (not c7) (xor (not (not (not (xor (not c6) (xor y (not c5)))))) (not (xor c4 (not (xor c3 (xor c2 c1))))))))))))))))) +(assert (= x (not (xor c9 (xor (xor (not c8) (xor (not c7) (xor (not (not (not (xor (not c6) (xor y (not c5)))))) (not (xor c4 (not (xor c3 (xor c2 c1)))))))) (xor (not (not c10)) (not (xor (xor (xor c13 c12) c11) (not (xor (not c14) (xor (xor c16 c15) z))))))))))) +(assert (= y (xor (not c5) (xor (not c6) (not (not (not (xor (not (xor c4 (not (xor c3 (xor c2 c1))))) (xor (not c7) (xor (not c8) (xor (xor (not x) c9) (xor (not (not c10)) (not (xor (xor (xor c13 c12) c11) (not (xor (not c14) (xor (xor c16 c15) z))))))))))))))))) +#end + +#begin +(declare-const z Bool) +(declare-const x Bool) +(declare-const y Bool) +(declare-const c14 Bool) +(declare-const c13 Bool) +(declare-const c12 Bool) +(declare-const c11 Bool) +(declare-const c10 Bool) +(declare-const c9 Bool) +(declare-const c8 Bool) +(declare-const c7 Bool) +(declare-const c6 Bool) +(declare-const c5 Bool) +(declare-const c4 Bool) +(declare-const c3 Bool) +(declare-const c2 Bool) +(declare-const c1 Bool) +(assert (= z (not (not (not (xor c14 (not (not (not (not (xor c13 (xor x (xor c12 (xor c11 (not (not (not (xor c10 (xor c9 (xor c8 (xor (not (not c7)) (not (xor (xor c6 c5) (xor y (not (not (xor c4 (xor (not (xor (not (not c3)) c2)) (not c1))))))))))))))))))))))))))))) +(assert (= x (xor (xor c12 (xor c11 (not (not (not (xor c10 (xor c9 (xor c8 (xor (not (not c7)) (not (xor (xor c6 c5) (xor y (not (not (xor c4 (xor (not (xor (not (not c3)) c2)) (not c1))))))))))))))))) (xor c13 (not (not (not (not (xor c14 (not (not (not z)))))))))))) +(assert (= y (xor (not (not (xor c4 (xor (not (xor (not (not c3)) c2)) (not c1))))) (xor (xor c6 c5) (not (xor (not (not c7)) (xor c8 (xor c9 (xor c10 (not (not (not (xor c11 (xor c12 (xor x (xor c13 (not (not (not (not (xor c14 (not (not (not z)))))))))))))))))))))))) +#end + +#begin +(declare-const z Int) +(declare-const x Int) +(declare-const y Int) +(declare-const c24 Int) +(declare-const c23 Int) +(declare-const c22 Int) +(declare-const c21 Int) +(declare-const c20 Int) +(declare-const c19 Int) +(declare-const c18 Int) +(declare-const c17 Int) +(declare-const c16 Int) +(declare-const c15 Int) +(declare-const c14 Int) +(declare-const c13 Int) +(declare-const c12 Int) +(declare-const c11 Int) +(declare-const c10 Int) +(declare-const c9 Int) +(declare-const c8 Int) +(declare-const c7 Int) +(declare-const c6 Int) +(declare-const c5 Int) +(declare-const c4 Int) +(declare-const c3 Int) +(declare-const c2 Int) +(declare-const c1 Int) +(assert (= z (- c24 (- (+ (- c23 (* c22 (+ c21 (- (+ c20 (+ (- (+ (+ (* (* (+ (+ (+ (- (* (- c19 (- (+ (- (+ (- c18 x) y) c17) c16) c15)) c14) c13) c12) c11) c10) c9) c8) c7) c6) c5) c4)) c3)))) c2) c1)))) +(assert (= x (- c18 (- (+ (- (+ (- c19 (div (+ (- (- (- (div (div (- (- (+ (- (- (+ (- (div (- c23 (- (+ (- c24 z) c1) c2)) c22) c21) c3) c20) c4) c5) c6) c7) c8) c9) c10) c11) c12) c13) c14)) c15) c16) c17) y)))) +(assert (= y (- (+ (- (+ (- c19 (div (+ (- (- (- (div (div (- (- (+ (- (- (+ (- (div (- c23 (- (+ (- c24 z) c1) c2)) c22) c21) c3) c20) c4) c5) c6) c7) c8) c9) c10) c11) c12) c13) c14)) c15) c16) c17) (- c18 x)))) +#end + +#begin +(declare-const z Real) +(declare-const x Real) +(declare-const y Real) +(declare-const c24 Real) +(declare-const c23 Real) +(declare-const c22 Real) +(declare-const c21 Real) +(declare-const c20 Real) +(declare-const c19 Real) +(declare-const c18 Real) +(declare-const c17 Real) +(declare-const c16 Real) +(declare-const c15 Real) +(declare-const c14 Real) +(declare-const c13 Real) +(declare-const c12 Real) +(declare-const c11 Real) +(declare-const c10 Real) +(declare-const c9 Real) +(declare-const c8 Real) +(declare-const c7 Real) +(declare-const c6 Real) +(declare-const c5 Real) +(declare-const c4 Real) +(declare-const c3 Real) +(declare-const c2 Real) +(declare-const c1 Real) +(assert (= z (+ (- (* c24 (/ (- c23 (- (+ (- (- (+ c22 (* c21 (- (+ (/ c20 c19) c18) (- (* c17 c16) (* (- (- (/ c15 c14) c13) (/ c12 (+ (- (- (* x c11) c10) c9) c8))) c7))))) c6) c5) c4) c3)) c2)) y) c1))) +(assert (= x (/ (+ (+ (- (/ (- (- (/ c15 c14) c13) (/ (- (* c17 c16) (- (+ (/ c20 c19) c18) (/ (- (+ (+ (- (+ (- c23 (* (/ (+ (- z c1) y) c24) c2)) c3) c4) c5) c6) c22) c21))) c7)) c12) c8) c9) c10) c11))) +(assert (= y (- (* c24 (/ (- c23 (- (+ (- (- (+ c22 (* c21 (- (+ (/ c20 c19) c18) (- (* c17 c16) (* (- (- (/ c15 c14) c13) (/ c12 (+ (- (- (* x c11) c10) c9) c8))) c7))))) c6) c5) c4) c3)) c2)) (- z c1)))) +#end + +#begin +(declare-const z Real) +(declare-const x Real) +(declare-const y Real) +(declare-const c24 Real) +(declare-const c23 Real) +(declare-const c22 Real) +(declare-const c21 Real) +(declare-const c20 Real) +(declare-const c19 Real) +(declare-const c18 Real) +(declare-const c17 Real) +(declare-const c16 Real) +(declare-const c15 Real) +(declare-const c14 Real) +(declare-const c13 Real) +(declare-const c12 Real) +(declare-const c11 Real) +(declare-const c10 Real) +(declare-const c9 Real) +(declare-const c8 Real) +(declare-const c7 Real) +(declare-const c6 Real) +(declare-const c5 Real) +(declare-const c4 Real) +(declare-const c3 Real) +(declare-const c2 Real) +(declare-const c1 Real) +(assert (= z (- (/ (/ (- (* (* (* (* (/ (/ (/ (* c24 (- (- (/ (* (/ (/ (+ (- (/ c23 (+ (- (/ (/ c22 c21) c20) c19) c18)) c17) c16) c15) c14) x) c13) c12) c11)) c10) c9) c8) c7) y) c6) c5) c4) c3) c2) c1))) +(assert (= x (/ (* (+ (+ (/ (* (* (* (/ (/ (/ (/ (+ (* (* (+ z c1) c2) c3) c4) c5) c6) y) c7) c8) c9) c10) c24) c11) c12) c13) (/ (/ (+ (- (/ c23 (+ (- (/ (/ c22 c21) c20) c19) c18)) c17) c16) c15) c14)))) +(assert (= y (/ (/ (/ (+ (* (* (+ z c1) c2) c3) c4) c5) c6) (* (/ (/ (/ (* c24 (- (- (/ (* (/ (/ (+ (- (/ c23 (+ (- (/ (/ c22 c21) c20) c19) c18)) c17) c16) c15) c14) x) c13) c12) c11)) c10) c9) c8) c7)))) +#end + +#begin +(declare-const z Int) +(declare-const x Int) +(declare-const y Int) +(declare-const c24 Int) +(declare-const c23 Int) +(declare-const c22 Int) +(declare-const c21 Int) +(declare-const c20 Int) +(declare-const c19 Int) +(declare-const c18 Int) +(declare-const c17 Int) +(declare-const c16 Int) +(declare-const c15 Int) +(declare-const c14 Int) +(declare-const c13 Int) +(declare-const c12 Int) +(declare-const c11 Int) +(declare-const c10 Int) +(declare-const c9 Int) +(declare-const c8 Int) +(declare-const c7 Int) +(declare-const c6 Int) +(declare-const c5 Int) +(declare-const c4 Int) +(declare-const c3 Int) +(declare-const c2 Int) +(declare-const c1 Int) +(assert (= z (- (* (- (* (+ (+ (+ c24 (* (+ (+ c23 (* c22 c21)) (+ (* (- (+ x c20) c19) (* (- (* (* (* (+ (* (+ c18 c17) (- (* c16 c15) c14)) c13) c12) c11) c10) c9) c8)) c7)) c6)) c5) c4) y) c3) c2) c1))) +(assert (= x (- (+ (div (- (- (div (- (- (- (div (+ (div (+ z c1) c2) c3) y) c4) c5) c24) c6) (+ c23 (* c22 c21))) c7) (* (- (* (* (* (+ (* (+ c18 c17) (- (* c16 c15) c14)) c13) c12) c11) c10) c9) c8)) c19) c20))) +(assert (= y (div (+ (div (+ z c1) c2) c3) (+ (+ (+ c24 (* (+ (+ c23 (* c22 c21)) (+ (* (- (+ x c20) c19) (* (- (* (* (* (+ (* (+ c18 c17) (- (* c16 c15) c14)) c13) c12) c11) c10) c9) c8)) c7)) c6)) c5) c4)))) +#end + +#begin +(declare-const z Real) +(declare-const x Real) +(declare-const y Real) +(declare-const c24 Real) +(declare-const c23 Real) +(declare-const c22 Real) +(declare-const c21 Real) +(declare-const c20 Real) +(declare-const c19 Real) +(declare-const c18 Real) +(declare-const c17 Real) +(declare-const c16 Real) +(declare-const c15 Real) +(declare-const c14 Real) +(declare-const c13 Real) +(declare-const c12 Real) +(declare-const c11 Real) +(declare-const c10 Real) +(declare-const c9 Real) +(declare-const c8 Real) +(declare-const c7 Real) +(declare-const c6 Real) +(declare-const c5 Real) +(declare-const c4 Real) +(declare-const c3 Real) +(declare-const c2 Real) +(declare-const c1 Real) +(assert (= z (- (+ x (+ c24 (* c23 (+ (+ (/ (- (+ (+ c22 (/ c21 (* c20 c19))) (/ y (/ (* (/ (+ (+ c18 (* (- (+ (- (* c17 (/ (/ c16 c15) c14)) c13) c12) c11) c10)) c9) c8) c7) c6))) c5) c4) c3) c2)))) c1))) +(assert (= x (- (+ z c1) (+ c24 (* c23 (+ (+ (/ (- (+ (+ c22 (/ c21 (* c20 c19))) (/ y (/ (* (/ (+ (+ c18 (* (- (+ (- (* c17 (/ (/ c16 c15) c14)) c13) c12) c11) c10)) c9) c8) c7) c6))) c5) c4) c3) c2)))))) +(assert (= y (* (- (+ (* (- (- (/ (- (- (+ z c1) x) c24) c23) c2) c3) c4) c5) (+ c22 (/ c21 (* c20 c19)))) (/ (* (/ (+ (+ c18 (* (- (+ (- (* c17 (/ (/ c16 c15) c14)) c13) c12) c11) c10)) c9) c8) c7) c6)))) +#end + +#begin +(declare-const z Real) +(declare-const x Real) +(declare-const y Real) +(declare-const c24 Real) +(declare-const c23 Real) +(declare-const c22 Real) +(declare-const c21 Real) +(declare-const c20 Real) +(declare-const c19 Real) +(declare-const c18 Real) +(declare-const c17 Real) +(declare-const c16 Real) +(declare-const c15 Real) +(declare-const c14 Real) +(declare-const c13 Real) +(declare-const c12 Real) +(declare-const c11 Real) +(declare-const c10 Real) +(declare-const c9 Real) +(declare-const c8 Real) +(declare-const c7 Real) +(declare-const c6 Real) +(declare-const c5 Real) +(declare-const c4 Real) +(declare-const c3 Real) +(declare-const c2 Real) +(declare-const c1 Real) +(assert (= z (+ c24 (/ (* (/ c23 c22) c21) (+ (/ c20 c19) (/ (/ (- (* x (+ (- (* c18 c17) c16) (+ (* c15 (+ (+ (* (+ (- (+ c14 c13) c12) (- (- (+ (+ c11 c10) y) c9) c8)) c7) c6) c5)) c4))) c3) c2) c1)))))) +(assert (= x (/ (+ (* (* (- (/ (- z c24) (* (/ c23 c22) c21)) (/ c20 c19)) c1) c2) c3) (+ (- (* c18 c17) c16) (+ (* c15 (+ (+ (* (+ (- (+ c14 c13) c12) (- (- (+ (+ c11 c10) y) c9) c8)) c7) c6) c5)) c4))))) +(assert (= y (- (+ (+ (- (/ (- (- (/ (- (- (/ (+ (* (* (- (/ (- z c24) (* (/ c23 c22) c21)) (/ c20 c19)) c1) c2) c3) x) (- (* c18 c17) c16)) c4) c15) c5) c6) c7) (- (+ c14 c13) c12)) c8) c9) (+ c11 c10)))) +#end + +#begin +(declare-const z Int) +(declare-const x Int) +(declare-const y Int) +(declare-const c24 Int) +(declare-const c23 Int) +(declare-const c22 Int) +(declare-const c21 Int) +(declare-const c20 Int) +(declare-const c19 Int) +(declare-const c18 Int) +(declare-const c17 Int) +(declare-const c16 Int) +(declare-const c15 Int) +(declare-const c14 Int) +(declare-const c13 Int) +(declare-const c12 Int) +(declare-const c11 Int) +(declare-const c10 Int) +(declare-const c9 Int) +(declare-const c8 Int) +(declare-const c7 Int) +(declare-const c6 Int) +(declare-const c5 Int) +(declare-const c4 Int) +(declare-const c3 Int) +(declare-const c2 Int) +(declare-const c1 Int) +(assert (= z (- (- c24 (+ (- c23 (* (* (* (+ c22 (+ c21 (- (- (- x c20) (- c19 (* c18 (- (+ (+ (+ (+ c17 (* (+ (- (* c16 (- (* c15 c14) c13)) c12) c11) c10)) c9) c8) c7) c6)))) c5))) c4) c3) y)) c2)) c1))) +(assert (= x (+ (+ (+ (- (- (div (div (div (- c23 (- (- c24 (+ z c1)) c2)) y) c3) c4) c22) c21) c5) (- c19 (* c18 (- (+ (+ (+ (+ c17 (* (+ (- (* c16 (- (* c15 c14) c13)) c12) c11) c10)) c9) c8) c7) c6)))) c20))) +(assert (= y (div (- c23 (- (- c24 (+ z c1)) c2)) (* (* (+ c22 (+ c21 (- (- (- x c20) (- c19 (* c18 (- (+ (+ (+ (+ c17 (* (+ (- (* c16 (- (* c15 c14) c13)) c12) c11) c10)) c9) c8) c7) c6)))) c5))) c4) c3)))) +#end + +#begin +(declare-const z Int) +(declare-const x Int) +(declare-const y Int) +(declare-const c24 Int) +(declare-const c23 Int) +(declare-const c22 Int) +(declare-const c21 Int) +(declare-const c20 Int) +(declare-const c19 Int) +(declare-const c18 Int) +(declare-const c17 Int) +(declare-const c16 Int) +(declare-const c15 Int) +(declare-const c14 Int) +(declare-const c13 Int) +(declare-const c12 Int) +(declare-const c11 Int) +(declare-const c10 Int) +(declare-const c9 Int) +(declare-const c8 Int) +(declare-const c7 Int) +(declare-const c6 Int) +(declare-const c5 Int) +(declare-const c4 Int) +(declare-const c3 Int) +(declare-const c2 Int) +(declare-const c1 Int) +(assert (= z (* c24 (* (- (* (* (+ (- (* (+ (* c23 (* (- c22 (- (+ (- (+ c21 (* c20 (* x c19))) (* (* c18 (* c17 (- (* (- (+ c16 c15) y) c14) c13))) c12)) c11) c10)) c9)) c8) c7) c6) c5) c4) c3) c2) c1)))) +(assert (= x (div (div (- (+ (- (+ (- c22 (div (div (- (div (+ (- (div (div (+ (div (div z c24) c1) c2) c3) c4) c5) c6) c7) c8) c23) c9)) c10) c11) (* (* c18 (* c17 (- (* (- (+ c16 c15) y) c14) c13))) c12)) c21) c20) c19))) +(assert (= y (- (+ c16 c15) (div (+ (div (div (div (- (+ c21 (* c20 (* x c19))) (- (+ (- c22 (div (div (- (div (+ (- (div (div (+ (div (div z c24) c1) c2) c3) c4) c5) c6) c7) c8) c23) c9)) c10) c11)) c12) c18) c17) c13) c14)))) +#end + +#begin +(declare-const z Bool) +(declare-const x Bool) +(declare-const y Bool) +(declare-const c17 Bool) +(declare-const c16 Bool) +(declare-const c15 Bool) +(declare-const c14 Bool) +(declare-const c13 Bool) +(declare-const c12 Bool) +(declare-const c11 Bool) +(declare-const c10 Bool) +(declare-const c9 Bool) +(declare-const c8 Bool) +(declare-const c7 Bool) +(declare-const c6 Bool) +(declare-const c5 Bool) +(declare-const c4 Bool) +(declare-const c3 Bool) +(declare-const c2 Bool) +(declare-const c1 Bool) +(assert (= z (not (xor (xor (xor (xor c17 c16) c15) (not c14)) (xor (not c13) (xor c12 (xor c11 (not (xor (xor (not (not x)) c10) (xor c9 (xor c8 (xor (not c7) (not (xor c6 (not (not (xor c5 (not (xor c4 (not (xor c3 (not (xor (xor c2 c1) y))))))))))))))))))))))) +(assert (= x (not (not (xor c10 (xor (xor c9 (xor c8 (xor (not c7) (not (xor c6 (not (not (xor c5 (not (xor c4 (not (xor c3 (not (xor (xor c2 c1) y)))))))))))))) (not (xor c11 (xor c12 (xor (not c13) (xor (xor (xor (xor c17 c16) c15) (not c14)) (not z)))))))))))) +(assert (= y (xor (xor c2 c1) (not (xor c3 (not (xor c4 (not (xor c5 (not (not (xor c6 (not (xor (not c7) (xor c8 (xor c9 (xor (xor (not (not x)) c10) (not (xor c11 (xor c12 (xor (not c13) (xor (xor (xor (xor c17 c16) c15) (not c14)) (not z))))))))))))))))))))))) +#end + +#begin +(declare-const z Int) +(declare-const x Int) +(declare-const y Int) +(declare-const c24 Int) +(declare-const c23 Int) +(declare-const c22 Int) +(declare-const c21 Int) +(declare-const c20 Int) +(declare-const c19 Int) +(declare-const c18 Int) +(declare-const c17 Int) +(declare-const c16 Int) +(declare-const c15 Int) +(declare-const c14 Int) +(declare-const c13 Int) +(declare-const c12 Int) +(declare-const c11 Int) +(declare-const c10 Int) +(declare-const c9 Int) +(declare-const c8 Int) +(declare-const c7 Int) +(declare-const c6 Int) +(declare-const c5 Int) +(declare-const c4 Int) +(declare-const c3 Int) +(declare-const c2 Int) +(declare-const c1 Int) +(assert (= z (* (- (+ c24 c23) c22) (+ (+ (* (- x (* (+ c21 (- c20 (* c19 (- (- (+ c18 c17) (- (* (+ (+ c16 (+ (- (- c15 c14) (+ c13 (- (- c12 c11) (- c10 c9)))) c8)) c7) c6) c5)) c4)))) c3)) y) c2) c1)))) +(assert (= x (+ (div (- (- (div z (- (+ c24 c23) c22)) c1) c2) y) (* (+ c21 (- c20 (* c19 (- (- (+ c18 c17) (- (* (+ (+ c16 (+ (- (- c15 c14) (+ c13 (- (- c12 c11) (- c10 c9)))) c8)) c7) c6) c5)) c4)))) c3)))) +(assert (= y (div (- (- (div z (- (+ c24 c23) c22)) c1) c2) (- x (* (+ c21 (- c20 (* c19 (- (- (+ c18 c17) (- (* (+ (+ c16 (+ (- (- c15 c14) (+ c13 (- (- c12 c11) (- c10 c9)))) c8)) c7) c6) c5)) c4)))) c3))))) +#end + +#begin +(declare-const z Int) +(declare-const x Int) +(declare-const y Int) +(declare-const c24 Int) +(declare-const c23 Int) +(declare-const c22 Int) +(declare-const c21 Int) +(declare-const c20 Int) +(declare-const c19 Int) +(declare-const c18 Int) +(declare-const c17 Int) +(declare-const c16 Int) +(declare-const c15 Int) +(declare-const c14 Int) +(declare-const c13 Int) +(declare-const c12 Int) +(declare-const c11 Int) +(declare-const c10 Int) +(declare-const c9 Int) +(declare-const c8 Int) +(declare-const c7 Int) +(declare-const c6 Int) +(declare-const c5 Int) +(declare-const c4 Int) +(declare-const c3 Int) +(declare-const c2 Int) +(declare-const c1 Int) +(assert (= z (- c24 (- c23 (+ c22 (- (+ (* (+ (* (+ c21 (* (+ (+ c20 c19) (* (+ (- (+ (- (+ (- (- (- (- (* (- c18 (+ c17 c16)) c15) c14) c13) c12) c11) c10) c9) x) c8) c7) c6)) y)) c5) c4) c3) c2) c1)))))) +(assert (= x (- (+ (- (div (- (div (- (div (- (div (- (+ (- (- c23 (- c24 z)) c22) c1) c2) c3) c4) c5) c21) y) (+ c20 c19)) c6) c7) c8) (- (+ (- (- (- (- (* (- c18 (+ c17 c16)) c15) c14) c13) c12) c11) c10) c9)))) +(assert (= y (div (- (div (- (div (- (+ (- (- c23 (- c24 z)) c22) c1) c2) c3) c4) c5) c21) (+ (+ c20 c19) (* (+ (- (+ (- (+ (- (- (- (- (* (- c18 (+ c17 c16)) c15) c14) c13) c12) c11) c10) c9) x) c8) c7) c6))))) +#end + +#begin +(declare-const z Real) +(declare-const x Real) +(declare-const y Real) +(declare-const c24 Real) +(declare-const c23 Real) +(declare-const c22 Real) +(declare-const c21 Real) +(declare-const c20 Real) +(declare-const c19 Real) +(declare-const c18 Real) +(declare-const c17 Real) +(declare-const c16 Real) +(declare-const c15 Real) +(declare-const c14 Real) +(declare-const c13 Real) +(declare-const c12 Real) +(declare-const c11 Real) +(declare-const c10 Real) +(declare-const c9 Real) +(declare-const c8 Real) +(declare-const c7 Real) +(declare-const c6 Real) +(declare-const c5 Real) +(declare-const c4 Real) +(declare-const c3 Real) +(declare-const c2 Real) +(declare-const c1 Real) +(assert (= z (* (- (+ (+ (+ (- (- (+ c24 (+ (- c23 (+ (+ c22 c21) c20)) (/ c19 (/ (+ (- (* c18 c17) (* (+ (/ c16 c15) (+ (- (/ c14 (* c13 (* c12 c11))) c10) c9)) c8)) x) c7)))) c6) c5) c4) c3) c2) y) c1))) +(assert (= x (- (* (/ (- (- (+ (+ (- (- (- (+ (/ z c1) y) c2) c3) c4) c5) c6) c24) (- c23 (+ (+ c22 c21) c20))) c19) c7) (- (* c18 c17) (* (+ (/ c16 c15) (+ (- (/ c14 (* c13 (* c12 c11))) c10) c9)) c8))))) +(assert (= y (- (+ (+ (+ (- (- (+ c24 (+ (- c23 (+ (+ c22 c21) c20)) (/ c19 (/ (+ (- (* c18 c17) (* (+ (/ c16 c15) (+ (- (/ c14 (* c13 (* c12 c11))) c10) c9)) c8)) x) c7)))) c6) c5) c4) c3) c2) (/ z c1)))) +#end + +#begin +(declare-const z Int) +(declare-const x Int) +(declare-const y Int) +(declare-const c24 Int) +(declare-const c23 Int) +(declare-const c22 Int) +(declare-const c21 Int) +(declare-const c20 Int) +(declare-const c19 Int) +(declare-const c18 Int) +(declare-const c17 Int) +(declare-const c16 Int) +(declare-const c15 Int) +(declare-const c14 Int) +(declare-const c13 Int) +(declare-const c12 Int) +(declare-const c11 Int) +(declare-const c10 Int) +(declare-const c9 Int) +(declare-const c8 Int) +(declare-const c7 Int) +(declare-const c6 Int) +(declare-const c5 Int) +(declare-const c4 Int) +(declare-const c3 Int) +(declare-const c2 Int) +(declare-const c1 Int) +(assert (= z (- c24 (- (+ (* c23 (+ (- (* c22 c21) (- (+ c20 c19) (* (* c18 (+ (- (+ (* c17 (- (+ c16 (+ (+ (+ c15 (- (- (- (- c14 (- c13 c12)) x) c11) c10)) c9) c8)) c7)) c6) y) c5)) c4))) c3)) c2) c1)))) +(assert (= x (- (- c14 (- c13 c12)) (+ (+ (- (- (- (- (+ (div (- (+ (- (div (div (- (+ c20 c19) (- (* c22 c21) (- (div (- (+ (- c24 z) c1) c2) c23) c3))) c4) c18) c5) y) c6) c17) c7) c16) c8) c9) c15) c10) c11)))) +(assert (= y (- (+ (* c17 (- (+ c16 (+ (+ (+ c15 (- (- (- (- c14 (- c13 c12)) x) c11) c10)) c9) c8)) c7)) c6) (- (div (div (- (+ c20 c19) (- (* c22 c21) (- (div (- (+ (- c24 z) c1) c2) c23) c3))) c4) c18) c5)))) +#end + +#begin +(declare-const z Bool) +(declare-const x Bool) +(declare-const y Bool) +(declare-const c17 Bool) +(declare-const c16 Bool) +(declare-const c15 Bool) +(declare-const c14 Bool) +(declare-const c13 Bool) +(declare-const c12 Bool) +(declare-const c11 Bool) +(declare-const c10 Bool) +(declare-const c9 Bool) +(declare-const c8 Bool) +(declare-const c7 Bool) +(declare-const c6 Bool) +(declare-const c5 Bool) +(declare-const c4 Bool) +(declare-const c3 Bool) +(declare-const c2 Bool) +(declare-const c1 Bool) +(assert (= z (not (not (xor c17 (not (xor c16 (xor (xor c15 (not (not (xor c14 x)))) (xor (xor c13 (not (not (xor (xor (xor c12 y) c11) (not c10))))) (xor c9 (xor c8 (not (xor c7 (not (not (not (xor (xor (not c6) (xor (xor (xor c5 c4) c3) c2)) c1))))))))))))))))) +(assert (= x (xor c14 (not (not (xor c15 (xor (xor (xor c13 (not (not (xor (xor (xor c12 y) c11) (not c10))))) (xor c9 (xor c8 (not (xor c7 (not (not (not (xor (xor (not c6) (xor (xor (xor c5 c4) c3) c2)) c1))))))))) (xor c16 (not (xor c17 (not (not z)))))))))))) +(assert (= y (xor c12 (xor c11 (xor (not c10) (not (not (xor c13 (xor (xor c9 (xor c8 (not (xor c7 (not (not (not (xor (xor (not c6) (xor (xor (xor c5 c4) c3) c2)) c1)))))))) (xor (xor c15 (not (not (xor c14 x)))) (xor c16 (not (xor c17 (not (not z))))))))))))))) +#end + +#begin +(declare-const z Bool) +(declare-const x Bool) +(declare-const y Bool) +(declare-const c16 Bool) +(declare-const c15 Bool) +(declare-const c14 Bool) +(declare-const c13 Bool) +(declare-const c12 Bool) +(declare-const c11 Bool) +(declare-const c10 Bool) +(declare-const c9 Bool) +(declare-const c8 Bool) +(declare-const c7 Bool) +(declare-const c6 Bool) +(declare-const c5 Bool) +(declare-const c4 Bool) +(declare-const c3 Bool) +(declare-const c2 Bool) +(declare-const c1 Bool) +(assert (= z (xor c16 (not (xor c15 (xor (not (xor c14 c13)) (not (xor (not c12) (not (not (not (xor (not c11) (xor c10 (xor c9 (xor (not x) (not (xor (xor c8 (not (xor (xor (xor (not c7) y) c6) (xor c5 (xor (not (not c4)) c3))))) (xor (not c2) c1)))))))))))))))))) +(assert (= x (not (xor (not (xor (xor c8 (not (xor (xor (xor (not c7) y) c6) (xor c5 (xor (not (not c4)) c3))))) (xor (not c2) c1))) (xor c9 (xor c10 (xor (not c11) (not (not (not (xor (not c12) (not (xor (not (xor c14 c13)) (xor c15 (not (xor c16 z)))))))))))))))) +(assert (= y (xor (not c7) (xor c6 (xor (xor c5 (xor (not (not c4)) c3)) (not (xor c8 (xor (xor (not c2) c1) (not (xor (not x) (xor c9 (xor c10 (xor (not c11) (not (not (not (xor (not c12) (not (xor (not (xor c14 c13)) (xor c15 (not (xor c16 z)))))))))))))))))))))) +#end + +#begin +(declare-const z Int) +(declare-const x Int) +(declare-const y Int) +(declare-const c24 Int) +(declare-const c23 Int) +(declare-const c22 Int) +(declare-const c21 Int) +(declare-const c20 Int) +(declare-const c19 Int) +(declare-const c18 Int) +(declare-const c17 Int) +(declare-const c16 Int) +(declare-const c15 Int) +(declare-const c14 Int) +(declare-const c13 Int) +(declare-const c12 Int) +(declare-const c11 Int) +(declare-const c10 Int) +(declare-const c9 Int) +(declare-const c8 Int) +(declare-const c7 Int) +(declare-const c6 Int) +(declare-const c5 Int) +(declare-const c4 Int) +(declare-const c3 Int) +(declare-const c2 Int) +(declare-const c1 Int) +(assert (= z (* (+ (* (+ (+ c24 (- c23 (+ (* (+ (- (- (+ (- (- (* (- (* (- (* c22 (* (- (- (- (* (- x c21) c20) c19) c18) c17) c16)) c15) c14) c13) c12) c11) c10) c9) c8) c7) y) c6) c5))) c4) c3) c2) c1))) +(assert (= x (+ (div (+ (+ (+ (div (div (+ (div (+ (div (+ (+ (- (+ (+ (- (div (- (- c23 (- (- (div (- (div z c1) c2) c3) c4) c24)) c5) c6) y) c7) c8) c9) c10) c11) c12) c13) c14) c15) c22) c16) c17) c18) c19) c20) c21))) +(assert (= y (- (div (- (- c23 (- (- (div (- (div z c1) c2) c3) c4) c24)) c5) c6) (- (- (+ (- (- (* (- (* (- (* c22 (* (- (- (- (* (- x c21) c20) c19) c18) c17) c16)) c15) c14) c13) c12) c11) c10) c9) c8) c7)))) +#end + +#begin +(declare-const z Real) +(declare-const x Real) +(declare-const y Real) +(declare-const c24 Real) +(declare-const c23 Real) +(declare-const c22 Real) +(declare-const c21 Real) +(declare-const c20 Real) +(declare-const c19 Real) +(declare-const c18 Real) +(declare-const c17 Real) +(declare-const c16 Real) +(declare-const c15 Real) +(declare-const c14 Real) +(declare-const c13 Real) +(declare-const c12 Real) +(declare-const c11 Real) +(declare-const c10 Real) +(declare-const c9 Real) +(declare-const c8 Real) +(declare-const c7 Real) +(declare-const c6 Real) +(declare-const c5 Real) +(declare-const c4 Real) +(declare-const c3 Real) +(declare-const c2 Real) +(declare-const c1 Real) +(assert (= z (/ x (* (- c24 c23) (- (/ c22 (+ (- c21 c20) (- (- c19 (/ c18 c17)) c16))) (/ (+ (+ c15 y) (* c14 c13)) (+ (* c12 (/ (/ (/ c11 (* (* (- (+ c10 (+ (* c9 c8) c7)) c6) c5) c4)) c3) c2)) c1))))))) +(assert (= x (* z (* (- c24 c23) (- (/ c22 (+ (- c21 c20) (- (- c19 (/ c18 c17)) c16))) (/ (+ (+ c15 y) (* c14 c13)) (+ (* c12 (/ (/ (/ c11 (* (* (- (+ c10 (+ (* c9 c8) c7)) c6) c5) c4)) c3) c2)) c1))))))) +(assert (= y (- (- (* (- (/ c22 (+ (- c21 c20) (- (- c19 (/ c18 c17)) c16))) (/ (/ z x) (- c24 c23))) (+ (* c12 (/ (/ (/ c11 (* (* (- (+ c10 (+ (* c9 c8) c7)) c6) c5) c4)) c3) c2)) c1)) (* c14 c13)) c15))) +#end + +#begin +(declare-const z Bool) +(declare-const x Bool) +(declare-const y Bool) +(declare-const c16 Bool) +(declare-const c15 Bool) +(declare-const c14 Bool) +(declare-const c13 Bool) +(declare-const c12 Bool) +(declare-const c11 Bool) +(declare-const c10 Bool) +(declare-const c9 Bool) +(declare-const c8 Bool) +(declare-const c7 Bool) +(declare-const c6 Bool) +(declare-const c5 Bool) +(declare-const c4 Bool) +(declare-const c3 Bool) +(declare-const c2 Bool) +(declare-const c1 Bool) +(assert (= z (xor (not (not c16)) (xor (xor c15 (xor (not (not c14)) x)) (not (xor (not (not c13)) (xor (not y) (xor c12 (xor (not c11) (not (xor c10 (xor (xor (not c9) (xor (not (xor (not (xor (xor c8 (xor (not (xor c7 (not c6))) c5)) c4)) c3)) c2)) c1)))))))))))) +(assert (= x (xor (not (not c14)) (xor c15 (xor (not (xor (not (not c13)) (xor (not y) (xor c12 (xor (not c11) (not (xor c10 (xor (xor (not c9) (xor (not (xor (not (xor (xor c8 (xor (not (xor c7 (not c6))) c5)) c4)) c3)) c2)) c1)))))))) (xor (not (not c16)) z)))))) +(assert (= y (not (xor (xor c12 (xor (not c11) (not (xor c10 (xor (xor (not c9) (xor (not (xor (not (xor (xor c8 (xor (not (xor c7 (not c6))) c5)) c4)) c3)) c2)) c1))))) (xor (not (not c13)) (not (xor (xor c15 (xor (not (not c14)) x)) (xor (not (not c16)) z)))))))) +#end + +#begin +(declare-const z Bool) +(declare-const x Bool) +(declare-const y Bool) +(declare-const c14 Bool) +(declare-const c13 Bool) +(declare-const c12 Bool) +(declare-const c11 Bool) +(declare-const c10 Bool) +(declare-const c9 Bool) +(declare-const c8 Bool) +(declare-const c7 Bool) +(declare-const c6 Bool) +(declare-const c5 Bool) +(declare-const c4 Bool) +(declare-const c3 Bool) +(declare-const c2 Bool) +(declare-const c1 Bool) +(assert (= z (not (not (not (xor (xor c14 x) (xor (not c13) (not (not (not (not (not (not (xor y (xor c12 (not (xor (xor (not (not c11)) c10) (xor (xor (xor c9 c8) (xor (not (xor c7 (not c6))) (not c5))) (xor c4 (not (not (not (xor c3 (xor c2 c1)))))))))))))))))))))))) +(assert (= x (xor c14 (xor (xor (not c13) (not (not (not (not (not (not (xor y (xor c12 (not (xor (xor (not (not c11)) c10) (xor (xor (xor c9 c8) (xor (not (xor c7 (not c6))) (not c5))) (xor c4 (not (not (not (xor c3 (xor c2 c1)))))))))))))))))) (not (not (not z))))))) +(assert (= y (xor (xor c12 (not (xor (xor (not (not c11)) c10) (xor (xor (xor c9 c8) (xor (not (xor c7 (not c6))) (not c5))) (xor c4 (not (not (not (xor c3 (xor c2 c1)))))))))) (not (not (not (not (not (not (xor (not c13) (xor (xor c14 x) (not (not (not z)))))))))))))) +#end + +#begin +(declare-const z Bool) +(declare-const x Bool) +(declare-const y Bool) +(declare-const c14 Bool) +(declare-const c13 Bool) +(declare-const c12 Bool) +(declare-const c11 Bool) +(declare-const c10 Bool) +(declare-const c9 Bool) +(declare-const c8 Bool) +(declare-const c7 Bool) +(declare-const c6 Bool) +(declare-const c5 Bool) +(declare-const c4 Bool) +(declare-const c3 Bool) +(declare-const c2 Bool) +(declare-const c1 Bool) +(assert (= z (xor c14 (not (xor (xor c13 (not c12)) (not (not (not (xor c11 (not (xor (xor c10 (not c9)) (not (not (xor c8 (xor (not c7) (not (not (xor (not (not (xor (xor c6 c5) (xor (not c4) (not c3))))) (xor (xor (not c2) (not (xor x y))) (not c1)))))))))))))))))))) +(assert (= x (xor y (not (xor (not c2) (xor (not c1) (xor (not (not (xor (xor c6 c5) (xor (not c4) (not c3))))) (not (not (xor (not c7) (xor c8 (not (not (xor (xor c10 (not c9)) (not (xor c11 (not (not (not (xor (xor c13 (not c12)) (not (xor c14 z)))))))))))))))))))))) +(assert (= y (xor x (not (xor (not c2) (xor (not c1) (xor (not (not (xor (xor c6 c5) (xor (not c4) (not c3))))) (not (not (xor (not c7) (xor c8 (not (not (xor (xor c10 (not c9)) (not (xor c11 (not (not (not (xor (xor c13 (not c12)) (not (xor c14 z)))))))))))))))))))))) +#end + +#begin +(declare-const z Bool) +(declare-const x Bool) +(declare-const y Bool) +(declare-const c15 Bool) +(declare-const c14 Bool) +(declare-const c13 Bool) +(declare-const c12 Bool) +(declare-const c11 Bool) +(declare-const c10 Bool) +(declare-const c9 Bool) +(declare-const c8 Bool) +(declare-const c7 Bool) +(declare-const c6 Bool) +(declare-const c5 Bool) +(declare-const c4 Bool) +(declare-const c3 Bool) +(declare-const c2 Bool) +(declare-const c1 Bool) +(assert (= z (xor c15 (not (not (xor c14 (not (not (not (not (not (not (not (xor (xor c13 (xor c12 (xor c11 c10))) (not (xor c9 (xor (not c8) (xor (not c7) (xor (xor (xor (xor x c6) (not y)) c5) (not (not (not (xor c4 (xor c3 (xor (not c2) c1))))))))))))))))))))))))) +(assert (= x (xor c6 (xor (not y) (xor c5 (xor (not (not (not (xor c4 (xor c3 (xor (not c2) c1)))))) (xor (not c7) (xor (not c8) (xor c9 (not (xor (xor c13 (xor c12 (xor c11 c10))) (not (not (not (not (not (not (not (xor c14 (not (not (xor c15 z)))))))))))))))))))))) +(assert (= y (not (xor (xor x c6) (xor c5 (xor (not (not (not (xor c4 (xor c3 (xor (not c2) c1)))))) (xor (not c7) (xor (not c8) (xor c9 (not (xor (xor c13 (xor c12 (xor c11 c10))) (not (not (not (not (not (not (not (xor c14 (not (not (xor c15 z)))))))))))))))))))))) +#end + +#begin +(declare-const z Real) +(declare-const x Real) +(declare-const y Real) +(declare-const c24 Real) +(declare-const c23 Real) +(declare-const c22 Real) +(declare-const c21 Real) +(declare-const c20 Real) +(declare-const c19 Real) +(declare-const c18 Real) +(declare-const c17 Real) +(declare-const c16 Real) +(declare-const c15 Real) +(declare-const c14 Real) +(declare-const c13 Real) +(declare-const c12 Real) +(declare-const c11 Real) +(declare-const c10 Real) +(declare-const c9 Real) +(declare-const c8 Real) +(declare-const c7 Real) +(declare-const c6 Real) +(declare-const c5 Real) +(declare-const c4 Real) +(declare-const c3 Real) +(declare-const c2 Real) +(declare-const c1 Real) +(assert (= z (/ (- (+ x (/ (+ (/ (* (/ (/ c24 (/ (/ c23 c22) (* (- (* (* (+ (+ c21 (* (+ (+ (/ c20 c19) (* c18 (/ (/ (/ c17 c16) c15) c14))) c13) y)) c12) c11) c10) c9) c8))) c7) c6) c5) c4) c3)) c2) c1))) +(assert (= x (- (+ (* z c1) c2) (/ (+ (/ (* (/ (/ c24 (/ (/ c23 c22) (* (- (* (* (+ (+ c21 (* (+ (+ (/ c20 c19) (* c18 (/ (/ (/ c17 c16) c15) c14))) c13) y)) c12) c11) c10) c9) c8))) c7) c6) c5) c4) c3)))) +(assert (= y (/ (- (- (/ (/ (+ (/ (/ (/ (* (/ (* (- (* (- (+ (* z c1) c2) x) c3) c4) c5) c6) c7) c24) (/ c23 c22)) c8) c9) c10) c11) c12) c21) (+ (+ (/ c20 c19) (* c18 (/ (/ (/ c17 c16) c15) c14))) c13)))) +#end + +#begin +(declare-const z Int) +(declare-const x Int) +(declare-const y Int) +(declare-const c24 Int) +(declare-const c23 Int) +(declare-const c22 Int) +(declare-const c21 Int) +(declare-const c20 Int) +(declare-const c19 Int) +(declare-const c18 Int) +(declare-const c17 Int) +(declare-const c16 Int) +(declare-const c15 Int) +(declare-const c14 Int) +(declare-const c13 Int) +(declare-const c12 Int) +(declare-const c11 Int) +(declare-const c10 Int) +(declare-const c9 Int) +(declare-const c8 Int) +(declare-const c7 Int) +(declare-const c6 Int) +(declare-const c5 Int) +(declare-const c4 Int) +(declare-const c3 Int) +(declare-const c2 Int) +(declare-const c1 Int) +(assert (= z (- (- (- (- (+ (- (+ (* (- (- (* (* (- c24 (- (+ (+ (+ c23 x) y) c22) (* (+ (- c21 (- (* (* (- (+ c20 c19) c18) c17) c16) c15)) c14) c13))) c12) c11) c10) c9) c8) c7) c6) c5) c4) c3) c2) c1))) +(assert (= x (- (- (- (+ (- c24 (div (div (+ (+ (div (- (+ (- (+ (+ (+ (+ z c1) c2) c3) c4) c5) c6) c7) c8) c9) c10) c11) c12)) (* (+ (- c21 (- (* (* (- (+ c20 c19) c18) c17) c16) c15)) c14) c13)) c22) y) c23))) +(assert (= y (- (- (+ (- c24 (div (div (+ (+ (div (- (+ (- (+ (+ (+ (+ z c1) c2) c3) c4) c5) c6) c7) c8) c9) c10) c11) c12)) (* (+ (- c21 (- (* (* (- (+ c20 c19) c18) c17) c16) c15)) c14) c13)) c22) (+ c23 x)))) +#end + +#begin +(declare-const z Int) +(declare-const x Int) +(declare-const y Int) +(declare-const c24 Int) +(declare-const c23 Int) +(declare-const c22 Int) +(declare-const c21 Int) +(declare-const c20 Int) +(declare-const c19 Int) +(declare-const c18 Int) +(declare-const c17 Int) +(declare-const c16 Int) +(declare-const c15 Int) +(declare-const c14 Int) +(declare-const c13 Int) +(declare-const c12 Int) +(declare-const c11 Int) +(declare-const c10 Int) +(declare-const c9 Int) +(declare-const c8 Int) +(declare-const c7 Int) +(declare-const c6 Int) +(declare-const c5 Int) +(declare-const c4 Int) +(declare-const c3 Int) +(declare-const c2 Int) +(declare-const c1 Int) +(assert (= z (* (* (- x c24) c23) (+ (+ (- (+ (- (- c22 (* (- (* c21 (- (* (* (- (+ (- (- c20 (* c19 (- c18 c17))) c16) (+ (* (- c15 c14) (+ c13 c12)) c11)) c10) c9) c8) c7)) c6) y)) c5) c4) c3) c2) c1)))) +(assert (= x (+ (div (div z (+ (+ (- (+ (- (- c22 (* (- (* c21 (- (* (* (- (+ (- (- c20 (* c19 (- c18 c17))) c16) (+ (* (- c15 c14) (+ c13 c12)) c11)) c10) c9) c8) c7)) c6) y)) c5) c4) c3) c2) c1)) c23) c24))) +(assert (= y (div (- c22 (+ (- (+ (- (- (div z (* (- x c24) c23)) c1) c2) c3) c4) c5)) (- (* c21 (- (* (* (- (+ (- (- c20 (* c19 (- c18 c17))) c16) (+ (* (- c15 c14) (+ c13 c12)) c11)) c10) c9) c8) c7)) c6)))) +#end + +#begin +(declare-const z Bool) +(declare-const x Bool) +(declare-const y Bool) +(declare-const c12 Bool) +(declare-const c11 Bool) +(declare-const c10 Bool) +(declare-const c9 Bool) +(declare-const c8 Bool) +(declare-const c7 Bool) +(declare-const c6 Bool) +(declare-const c5 Bool) +(declare-const c4 Bool) +(declare-const c3 Bool) +(declare-const c2 Bool) +(declare-const c1 Bool) +(assert (= z (xor (xor (not (xor (not (xor c12 c11)) (xor c10 (xor c9 (not (xor (not (not x)) (not (not (not (not (not c8))))))))))) c7) (not (not (not (not (not (not (not (xor (xor c6 (xor (xor c5 y) c4)) (not (xor c3 (not (not (xor c2 (not (not (not c1))))))))))))))))))) +(assert (= x (not (not (xor (not (not (not (not (not c8))))) (not (xor c9 (xor c10 (xor (not (xor c12 c11)) (not (xor c7 (xor (not (not (not (not (not (not (not (xor (xor c6 (xor (xor c5 y) c4)) (not (xor c3 (not (not (xor c2 (not (not (not c1)))))))))))))))) z)))))))))))) +(assert (= y (xor c5 (xor c4 (xor c6 (xor (not (xor c3 (not (not (xor c2 (not (not (not c1)))))))) (not (not (not (not (not (not (not (xor (xor (not (xor (not (xor c12 c11)) (xor c10 (xor c9 (not (xor (not (not x)) (not (not (not (not (not c8))))))))))) c7) z)))))))))))))) +#end + +#begin +(declare-const z Int) +(declare-const x Int) +(declare-const y Int) +(declare-const c24 Int) +(declare-const c23 Int) +(declare-const c22 Int) +(declare-const c21 Int) +(declare-const c20 Int) +(declare-const c19 Int) +(declare-const c18 Int) +(declare-const c17 Int) +(declare-const c16 Int) +(declare-const c15 Int) +(declare-const c14 Int) +(declare-const c13 Int) +(declare-const c12 Int) +(declare-const c11 Int) +(declare-const c10 Int) +(declare-const c9 Int) +(declare-const c8 Int) +(declare-const c7 Int) +(declare-const c6 Int) +(declare-const c5 Int) +(declare-const c4 Int) +(declare-const c3 Int) +(declare-const c2 Int) +(declare-const c1 Int) +(assert (= z (+ c24 (+ (* (- x (- (* (* (* (+ (* c23 c22) (- (+ c21 (* (+ (- (- (+ (- (- (- (- c20 c19) (- (* (* c18 (+ c17 c16)) c15) c14)) c13) c12) y) c11) c10) c9) c8)) c7)) c6) c5) c4) c3)) c2) c1)))) +(assert (= x (+ (div (- (- z c24) c1) c2) (- (* (* (* (+ (* c23 c22) (- (+ c21 (* (+ (- (- (+ (- (- (- (- c20 c19) (- (* (* c18 (+ c17 c16)) c15) c14)) c13) c12) y) c11) c10) c9) c8)) c7)) c6) c5) c4) c3)))) +(assert (= y (- (+ (+ (- (div (- (+ (- (div (div (div (+ (- x (div (- (- z c24) c1) c2)) c3) c4) c5) c6) (* c23 c22)) c7) c21) c8) c9) c10) c11) (- (- (- (- c20 c19) (- (* (* c18 (+ c17 c16)) c15) c14)) c13) c12)))) +#end + diff --git a/bugs/z3/nra-1.smt2 b/bugs/z3/nra-1.smt2 new file mode 100644 index 0000000..bda3a9b --- /dev/null +++ b/bugs/z3/nra-1.smt2 @@ -0,0 +1,25 @@ +; config-1 +; not triggered with (set-logic NRA) +(declare-fun a () Real) +(declare-fun b () Real) +(declare-fun c () Real) +(declare-fun d () Real) +(assert + (forall + ((e Real)) + (and + (< c 0) + (= 0 (- e d (* a e e))) + (= b (- e d (* a e e))) + (= b + (* + (+ 1 (- (* d 160)) (- 2 (/ (- (- 33 c)) (- 49) 2))) + (+ 1 (- (* d 160)) (- 2 (/ (- (- 33 c)) (- 49) 2))) + ) + ) + ) + ) +) +(assert (= 0 0)) +; also triggered by (= 1 1) and (= 2 2), not by (= 3 3) +(check-sat) From 5587bf7f1c2701784bbb64014fbd3d5170cf8acc Mon Sep 17 00:00:00 2001 From: Lucas Weitzendorf Date: Tue, 10 May 2022 02:01:37 +0200 Subject: [PATCH 2/3] Added README with overview --- .gitignore | 7 ++++--- bugs/README.md | 5 +++++ bugs/z3/nra-1.smt2 | 1 - 3 files changed, 9 insertions(+), 4 deletions(-) create mode 100644 bugs/README.md diff --git a/.gitignore b/.gitignore index bb46050..a83f16b 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ -.idea -__pycache__ +.idea/ +.vscode/ +__pycache__/ *.dot -out +out/ diff --git a/bugs/README.md b/bugs/README.md new file mode 100644 index 0000000..5452a14 --- /dev/null +++ b/bugs/README.md @@ -0,0 +1,5 @@ +# Discovered bugs +## Z3 +| Input | Configuration | Date | +|------------------------|--------------------------|----------| +| [NRA 1](z3/nra-1.smt2) | [config-1](config-1.txt) | 30/04/22 | diff --git a/bugs/z3/nra-1.smt2 b/bugs/z3/nra-1.smt2 index bda3a9b..38f7e7f 100644 --- a/bugs/z3/nra-1.smt2 +++ b/bugs/z3/nra-1.smt2 @@ -1,4 +1,3 @@ -; config-1 ; not triggered with (set-logic NRA) (declare-fun a () Real) (declare-fun b () Real) From 5a6c8f044b56193ee9a7cc0b944654618a44868c Mon Sep 17 00:00:00 2001 From: Lucas Weitzendorf Date: Tue, 10 May 2022 14:02:35 +0200 Subject: [PATCH 3/3] Add issue link to bug README --- bugs/README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/bugs/README.md b/bugs/README.md index 5452a14..26d0613 100644 --- a/bugs/README.md +++ b/bugs/README.md @@ -1,5 +1,5 @@ # Discovered bugs ## Z3 -| Input | Configuration | Date | -|------------------------|--------------------------|----------| -| [NRA 1](z3/nra-1.smt2) | [config-1](config-1.txt) | 30/04/22 | +| Input | Configuration | Issue | Date | +|------------------------|--------------------------|-----------------------------------------------------------------------------|----------| +| [NRA 1](z3/nra-1.smt2) | [config-1](config-1.txt) | [#2650](https://github.com/Z3Prover/z3/issues/2650#issuecomment-1113448263) | 30/04/22 |