diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/auflia/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/auflia/fuzz05.smt | 183 | ||||
-rw-r--r-- | test/regress/regress0/uflra/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/uflra/fuzz01.smt | 257 |
4 files changed, 444 insertions, 2 deletions
diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am index ed810eaeb..e35f24d13 100644 --- a/test/regress/regress0/auflia/Makefile.am +++ b/test/regress/regress0/auflia/Makefile.am @@ -18,7 +18,8 @@ TESTS = \ fuzz01.delta01.smt \ fuzz02.smt \ fuzz03.smt \ - fuzz04.smt + fuzz04.smt \ + fuzz05.smt EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/auflia/fuzz05.smt b/test/regress/regress0/auflia/fuzz05.smt new file mode 100644 index 000000000..538f86ece --- /dev/null +++ b/test/regress/regress0/auflia/fuzz05.smt @@ -0,0 +1,183 @@ +(benchmark fuzzsmt +:logic QF_AUFLIA +:status sat +:extrafuns ((f0 Int Int Int)) +:extrafuns ((f1 Array Array Array Array)) +:extrapreds ((p0 Int)) +:extrapreds ((p1 Array Array Array)) +:extrafuns ((v0 Int)) +:extrafuns ((v1 Int)) +:extrafuns ((v2 Int)) +:extrafuns ((v3 Array)) +:formula +(let (?e4 2) +(let (?e5 (- v2 v2)) +(let (?e6 (f0 v1 v0)) +(let (?e7 (* ?e6 ?e4)) +(let (?e8 (ite (p0 v2) 1 0)) +(let (?e9 (f1 v3 v3 v3)) +(flet ($e10 (p1 ?e9 v3 v3)) +(flet ($e11 (> ?e7 v1)) +(flet ($e12 (<= ?e8 ?e6)) +(flet ($e13 (p0 ?e8)) +(flet ($e14 (>= v2 v0)) +(flet ($e15 (p0 ?e5)) +(let (?e16 (ite $e12 v3 ?e9)) +(let (?e17 (ite $e15 ?e16 v3)) +(let (?e18 (ite $e11 ?e17 ?e16)) +(let (?e19 (ite $e14 ?e9 ?e9)) +(let (?e20 (ite $e13 ?e16 v3)) +(let (?e21 (ite $e12 v3 ?e19)) +(let (?e22 (ite $e10 ?e16 v3)) +(let (?e23 (ite $e15 ?e5 v0)) +(let (?e24 (ite $e12 v1 ?e6)) +(let (?e25 (ite $e11 ?e6 v0)) +(let (?e26 (ite $e15 ?e25 ?e23)) +(let (?e27 (ite $e12 v1 v0)) +(let (?e28 (ite $e14 ?e23 ?e24)) +(let (?e29 (ite $e10 ?e6 ?e23)) +(let (?e30 (ite $e13 v2 ?e29)) +(let (?e31 (ite $e12 ?e7 ?e25)) +(let (?e32 (ite $e12 ?e8 ?e8)) +(let (?e33 (store v3 ?e27 ?e7)) +(let (?e34 (select ?e21 ?e30)) +(let (?e35 (f1 ?e9 ?e21 ?e18)) +(let (?e36 (f1 ?e9 ?e17 v3)) +(let (?e37 (f1 ?e18 ?e21 ?e19)) +(let (?e38 (f1 ?e33 ?e18 ?e35)) +(let (?e39 (f1 ?e22 ?e22 v3)) +(let (?e40 (f1 ?e18 ?e20 ?e22)) +(let (?e41 (f1 ?e16 ?e33 ?e36)) +(let (?e42 (f0 ?e31 ?e26)) +(let (?e43 (+ ?e25 ?e5)) +(let (?e44 (f0 ?e42 v0)) +(let (?e45 (ite (p0 ?e24) 1 0)) +(let (?e46 (f0 ?e8 v0)) +(let (?e47 (ite (p0 v1) 1 0)) +(let (?e48 (+ ?e23 ?e26)) +(let (?e49 (~ ?e28)) +(let (?e50 (ite (p0 ?e27) 1 0)) +(let (?e51 (~ ?e46)) +(let (?e52 (~ ?e32)) +(let (?e53 (* (~ ?e4) ?e30)) +(let (?e54 (~ ?e29)) +(let (?e55 (- ?e48 ?e31)) +(let (?e56 (* ?e4 ?e7)) +(let (?e57 (f0 ?e29 ?e24)) +(let (?e58 (+ ?e34 v2)) +(let (?e59 (f0 ?e26 ?e50)) +(let (?e60 (f0 ?e6 ?e54)) +(flet ($e61 (p1 ?e38 ?e19 ?e9)) +(flet ($e62 (p1 ?e41 ?e18 ?e40)) +(flet ($e63 (p1 ?e21 ?e35 ?e40)) +(flet ($e64 (p1 ?e16 ?e37 ?e19)) +(flet ($e65 (p1 ?e33 ?e38 ?e18)) +(flet ($e66 (p1 ?e39 ?e20 ?e35)) +(flet ($e67 (p1 ?e38 ?e36 ?e40)) +(flet ($e68 (p1 ?e21 ?e35 ?e20)) +(flet ($e69 (p1 ?e9 ?e33 ?e19)) +(flet ($e70 (p1 ?e18 ?e18 ?e35)) +(flet ($e71 (p1 v3 ?e18 ?e41)) +(flet ($e72 (p1 ?e39 ?e35 v3)) +(flet ($e73 (p1 ?e37 ?e22 ?e38)) +(flet ($e74 (p1 ?e16 ?e9 ?e16)) +(flet ($e75 (p1 ?e17 ?e9 ?e37)) +(flet ($e76 (= ?e53 ?e32)) +(flet ($e77 (>= ?e26 ?e55)) +(flet ($e78 (distinct ?e23 ?e7)) +(flet ($e79 (< ?e28 ?e5)) +(flet ($e80 (<= ?e42 ?e30)) +(flet ($e81 (>= ?e58 ?e50)) +(flet ($e82 (= ?e45 ?e46)) +(flet ($e83 (<= ?e59 ?e32)) +(flet ($e84 (p0 ?e56)) +(flet ($e85 (p0 v2)) +(flet ($e86 (p0 ?e31)) +(flet ($e87 (> ?e25 ?e32)) +(flet ($e88 (= ?e44 ?e54)) +(flet ($e89 (< ?e60 ?e23)) +(flet ($e90 (p0 ?e29)) +(flet ($e91 (distinct v2 ?e6)) +(flet ($e92 (<= ?e59 ?e58)) +(flet ($e93 (= ?e43 ?e47)) +(flet ($e94 (distinct ?e54 v2)) +(flet ($e95 (> ?e8 ?e5)) +(flet ($e96 (distinct ?e59 ?e8)) +(flet ($e97 (distinct ?e48 ?e23)) +(flet ($e98 (> ?e24 ?e60)) +(flet ($e99 (>= ?e34 ?e44)) +(flet ($e100 (< ?e49 ?e7)) +(flet ($e101 (distinct ?e51 ?e53)) +(flet ($e102 (<= ?e52 ?e23)) +(flet ($e103 (<= v1 ?e57)) +(flet ($e104 (>= ?e48 ?e52)) +(flet ($e105 (distinct ?e32 ?e29)) +(flet ($e106 (p0 ?e46)) +(flet ($e107 (<= v0 v0)) +(flet ($e108 (= ?e27 ?e43)) +(flet ($e109 (and $e67 $e107)) +(flet ($e110 (or $e75 $e69)) +(flet ($e111 (implies $e15 $e76)) +(flet ($e112 (xor $e98 $e96)) +(flet ($e113 (and $e78 $e62)) +(flet ($e114 (or $e100 $e77)) +(flet ($e115 (xor $e83 $e12)) +(flet ($e116 (and $e13 $e71)) +(flet ($e117 (xor $e116 $e112)) +(flet ($e118 (not $e86)) +(flet ($e119 (or $e81 $e64)) +(flet ($e120 (iff $e72 $e70)) +(flet ($e121 (iff $e108 $e114)) +(flet ($e122 (or $e88 $e74)) +(flet ($e123 (xor $e105 $e118)) +(flet ($e124 (xor $e103 $e104)) +(flet ($e125 (implies $e93 $e119)) +(flet ($e126 (or $e102 $e90)) +(flet ($e127 (iff $e126 $e89)) +(flet ($e128 (if_then_else $e66 $e109 $e106)) +(flet ($e129 (implies $e85 $e101)) +(flet ($e130 (xor $e110 $e128)) +(flet ($e131 (iff $e63 $e11)) +(flet ($e132 (not $e84)) +(flet ($e133 (not $e68)) +(flet ($e134 (or $e124 $e113)) +(flet ($e135 (if_then_else $e82 $e121 $e94)) +(flet ($e136 (iff $e132 $e80)) +(flet ($e137 (or $e95 $e131)) +(flet ($e138 (and $e129 $e122)) +(flet ($e139 (or $e92 $e135)) +(flet ($e140 (xor $e133 $e139)) +(flet ($e141 (if_then_else $e140 $e91 $e130)) +(flet ($e142 (implies $e117 $e117)) +(flet ($e143 (implies $e14 $e79)) +(flet ($e144 (not $e97)) +(flet ($e145 (and $e120 $e143)) +(flet ($e146 (xor $e134 $e87)) +(flet ($e147 (iff $e125 $e111)) +(flet ($e148 (iff $e147 $e146)) +(flet ($e149 (not $e99)) +(flet ($e150 (or $e145 $e148)) +(flet ($e151 (iff $e149 $e141)) +(flet ($e152 (and $e61 $e61)) +(flet ($e153 (if_then_else $e10 $e142 $e152)) +(flet ($e154 (and $e73 $e115)) +(flet ($e155 (or $e138 $e150)) +(flet ($e156 (and $e127 $e136)) +(flet ($e157 (and $e123 $e137)) +(flet ($e158 (if_then_else $e151 $e155 $e155)) +(flet ($e159 (and $e65 $e153)) +(flet ($e160 (not $e144)) +(flet ($e161 (implies $e156 $e156)) +(flet ($e162 (not $e161)) +(flet ($e163 (if_then_else $e162 $e157 $e159)) +(flet ($e164 (implies $e158 $e154)) +(flet ($e165 (or $e160 $e163)) +(flet ($e166 (not $e164)) +(flet ($e167 (iff $e165 $e165)) +(flet ($e168 (and $e166 $e166)) +(flet ($e169 (and $e168 $e168)) +(flet ($e170 (not $e169)) +(flet ($e171 (iff $e167 $e170)) +$e171 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index 352161466..60b3109f1 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -37,7 +37,8 @@ SMT_TESTS = \ incorrect1.delta01.smt \ incorrect1.delta02.smt \ error1.smt \ - neq-deltacomp.smt + neq-deltacomp.smt \ + fuzz01.smt # Regression tests for SMT2 inputs SMT2_TESTS = diff --git a/test/regress/regress0/uflra/fuzz01.smt b/test/regress/regress0/uflra/fuzz01.smt new file mode 100644 index 000000000..2c6286e3a --- /dev/null +++ b/test/regress/regress0/uflra/fuzz01.smt @@ -0,0 +1,257 @@ +(benchmark fuzzsmt +:logic QF_UFLRA +:status sat +:extrafuns ((f0 Real Real)) +:extrafuns ((f1 Real Real Real Real)) +:extrapreds ((p0 Real Real Real)) +:extrafuns ((v0 Real)) +:extrafuns ((v1 Real)) +:extrafuns ((v2 Real)) +:formula +(let (?e3 5) +(let (?e4 2) +(let (?e5 0) +(let (?e6 (f1 v0 v1 v0)) +(let (?e7 (f0 v0)) +(let (?e8 (ite (p0 v1 ?e7 v0) 1 0)) +(let (?e9 (ite (p0 ?e8 v1 v0) 1 0)) +(let (?e10 (- ?e9 ?e9)) +(let (?e11 (~ v1)) +(let (?e12 (ite (p0 v0 ?e8 v2) 1 0)) +(let (?e13 (/ ?e5 ?e4)) +(let (?e14 (/ ?e4 ?e4)) +(let (?e15 (~ v0)) +(let (?e16 (* ?e6 (~ ?e3))) +(flet ($e17 (< ?e8 ?e8)) +(flet ($e18 (<= v0 v1)) +(flet ($e19 (distinct ?e16 ?e15)) +(flet ($e20 (distinct ?e13 ?e12)) +(flet ($e21 (> ?e11 ?e11)) +(flet ($e22 (= v0 ?e11)) +(flet ($e23 (p0 ?e16 ?e13 ?e11)) +(flet ($e24 (> ?e16 ?e12)) +(flet ($e25 (= ?e13 ?e12)) +(flet ($e26 (<= ?e12 ?e12)) +(flet ($e27 (p0 ?e12 ?e12 ?e14)) +(flet ($e28 (distinct ?e7 ?e12)) +(flet ($e29 (>= ?e9 ?e13)) +(flet ($e30 (< v2 v0)) +(flet ($e31 (> v2 v1)) +(flet ($e32 (p0 ?e9 v1 ?e6)) +(flet ($e33 (= ?e16 v2)) +(flet ($e34 (p0 ?e7 ?e12 ?e14)) +(flet ($e35 (distinct ?e12 ?e15)) +(flet ($e36 (>= ?e9 ?e15)) +(flet ($e37 (< ?e11 ?e10)) +(let (?e38 (ite $e24 ?e9 ?e14)) +(let (?e39 (ite $e24 ?e12 ?e6)) +(let (?e40 (ite $e30 ?e15 ?e11)) +(let (?e41 (ite $e32 v1 v2)) +(let (?e42 (ite $e36 v1 ?e39)) +(let (?e43 (ite $e33 ?e10 ?e15)) +(let (?e44 (ite $e19 ?e8 ?e16)) +(let (?e45 (ite $e26 v0 ?e12)) +(let (?e46 (ite $e36 ?e7 ?e14)) +(let (?e47 (ite $e20 ?e40 ?e14)) +(let (?e48 (ite $e26 ?e15 ?e9)) +(let (?e49 (ite $e22 ?e13 ?e13)) +(let (?e50 (ite $e31 ?e16 ?e47)) +(let (?e51 (ite $e30 ?e41 ?e11)) +(let (?e52 (ite $e17 ?e6 ?e9)) +(let (?e53 (ite $e18 ?e46 v2)) +(let (?e54 (ite $e19 ?e9 ?e9)) +(let (?e55 (ite $e37 ?e51 v2)) +(let (?e56 (ite $e28 ?e14 ?e46)) +(let (?e57 (ite $e29 ?e12 ?e14)) +(let (?e58 (ite $e17 ?e47 ?e7)) +(let (?e59 (ite $e34 ?e46 v2)) +(let (?e60 (ite $e21 ?e55 ?e51)) +(let (?e61 (ite $e24 ?e14 ?e50)) +(let (?e62 (ite $e17 ?e47 ?e61)) +(let (?e63 (ite $e30 ?e45 ?e12)) +(let (?e64 (ite $e35 ?e45 ?e47)) +(let (?e65 (ite $e25 v1 ?e38)) +(let (?e66 (ite $e23 ?e16 ?e59)) +(let (?e67 (ite $e26 ?e61 ?e38)) +(let (?e68 (ite $e27 ?e57 ?e50)) +(flet ($e69 (> v0 ?e12)) +(flet ($e70 (p0 ?e8 ?e66 ?e43)) +(flet ($e71 (<= ?e64 ?e8)) +(flet ($e72 (> ?e49 ?e43)) +(flet ($e73 (>= v0 ?e46)) +(flet ($e74 (<= v1 ?e49)) +(flet ($e75 (< ?e11 ?e38)) +(flet ($e76 (>= v2 ?e10)) +(flet ($e77 (= ?e51 ?e40)) +(flet ($e78 (>= ?e14 ?e50)) +(flet ($e79 (> ?e49 ?e8)) +(flet ($e80 (= ?e47 ?e12)) +(flet ($e81 (> ?e64 ?e54)) +(flet ($e82 (<= ?e48 ?e57)) +(flet ($e83 (> ?e57 ?e54)) +(flet ($e84 (p0 ?e44 ?e39 ?e65)) +(flet ($e85 (< ?e51 ?e11)) +(flet ($e86 (distinct ?e51 ?e53)) +(flet ($e87 (= ?e57 ?e46)) +(flet ($e88 (p0 ?e6 ?e47 ?e41)) +(flet ($e89 (<= ?e58 ?e14)) +(flet ($e90 (>= ?e67 v1)) +(flet ($e91 (<= ?e39 ?e59)) +(flet ($e92 (>= ?e10 v1)) +(flet ($e93 (> ?e10 ?e10)) +(flet ($e94 (<= ?e57 ?e10)) +(flet ($e95 (< ?e47 ?e42)) +(flet ($e96 (>= ?e41 ?e63)) +(flet ($e97 (<= ?e9 ?e14)) +(flet ($e98 (distinct v0 ?e64)) +(flet ($e99 (distinct ?e49 ?e61)) +(flet ($e100 (p0 ?e61 ?e52 v1)) +(flet ($e101 (>= ?e12 ?e6)) +(flet ($e102 (p0 ?e59 ?e57 ?e62)) +(flet ($e103 (distinct ?e66 ?e15)) +(flet ($e104 (<= ?e46 ?e50)) +(flet ($e105 (>= ?e57 ?e46)) +(flet ($e106 (= ?e44 ?e58)) +(flet ($e107 (p0 ?e6 ?e8 ?e40)) +(flet ($e108 (distinct ?e12 ?e58)) +(flet ($e109 (>= ?e56 ?e15)) +(flet ($e110 (< ?e62 ?e44)) +(flet ($e111 (distinct v2 ?e14)) +(flet ($e112 (< ?e44 ?e39)) +(flet ($e113 (= ?e40 ?e11)) +(flet ($e114 (= ?e55 ?e56)) +(flet ($e115 (p0 ?e66 ?e40 ?e62)) +(flet ($e116 (= ?e13 ?e14)) +(flet ($e117 (> ?e59 ?e68)) +(flet ($e118 (p0 ?e45 ?e50 ?e6)) +(flet ($e119 (p0 ?e67 v2 v1)) +(flet ($e120 (= v2 ?e15)) +(flet ($e121 (< ?e42 ?e12)) +(flet ($e122 (distinct ?e52 ?e40)) +(flet ($e123 (= v1 ?e14)) +(flet ($e124 (< ?e13 ?e66)) +(flet ($e125 (= ?e12 ?e61)) +(flet ($e126 (>= ?e66 v0)) +(flet ($e127 (> ?e58 ?e13)) +(flet ($e128 (distinct ?e41 ?e41)) +(flet ($e129 (>= ?e47 ?e16)) +(flet ($e130 (p0 v2 ?e59 ?e62)) +(flet ($e131 (<= ?e12 ?e41)) +(flet ($e132 (> ?e68 ?e51)) +(flet ($e133 (>= ?e59 ?e38)) +(flet ($e134 (< ?e65 ?e13)) +(flet ($e135 (< ?e39 ?e45)) +(flet ($e136 (>= ?e54 ?e16)) +(flet ($e137 (>= ?e62 ?e54)) +(flet ($e138 (p0 ?e59 ?e54 ?e41)) +(flet ($e139 (p0 ?e53 ?e12 ?e45)) +(flet ($e140 (distinct ?e52 ?e14)) +(flet ($e141 (= ?e51 ?e63)) +(flet ($e142 (p0 ?e65 ?e59 ?e64)) +(flet ($e143 (<= ?e52 ?e45)) +(flet ($e144 (p0 ?e49 ?e12 ?e63)) +(flet ($e145 (> ?e39 ?e7)) +(flet ($e146 (>= ?e60 ?e8)) +(flet ($e147 (if_then_else $e78 $e34 $e87)) +(flet ($e148 (iff $e28 $e83)) +(flet ($e149 (or $e19 $e107)) +(flet ($e150 (not $e29)) +(flet ($e151 (or $e25 $e113)) +(flet ($e152 (implies $e82 $e133)) +(flet ($e153 (or $e120 $e30)) +(flet ($e154 (not $e81)) +(flet ($e155 (xor $e26 $e99)) +(flet ($e156 (not $e105)) +(flet ($e157 (xor $e122 $e126)) +(flet ($e158 (implies $e70 $e97)) +(flet ($e159 (iff $e21 $e150)) +(flet ($e160 (iff $e37 $e33)) +(flet ($e161 (if_then_else $e149 $e139 $e129)) +(flet ($e162 (iff $e96 $e18)) +(flet ($e163 (if_then_else $e116 $e36 $e160)) +(flet ($e164 (implies $e125 $e17)) +(flet ($e165 (iff $e74 $e98)) +(flet ($e166 (and $e159 $e110)) +(flet ($e167 (implies $e152 $e31)) +(flet ($e168 (if_then_else $e141 $e86 $e124)) +(flet ($e169 (and $e80 $e118)) +(flet ($e170 (implies $e22 $e154)) +(flet ($e171 (xor $e84 $e153)) +(flet ($e172 (and $e102 $e77)) +(flet ($e173 (and $e164 $e100)) +(flet ($e174 (if_then_else $e134 $e76 $e90)) +(flet ($e175 (and $e157 $e138)) +(flet ($e176 (or $e92 $e158)) +(flet ($e177 (xor $e103 $e130)) +(flet ($e178 (or $e73 $e101)) +(flet ($e179 (if_then_else $e104 $e174 $e27)) +(flet ($e180 (and $e156 $e172)) +(flet ($e181 (implies $e93 $e176)) +(flet ($e182 (xor $e121 $e32)) +(flet ($e183 (and $e148 $e112)) +(flet ($e184 (and $e165 $e165)) +(flet ($e185 (iff $e72 $e162)) +(flet ($e186 (if_then_else $e151 $e23 $e171)) +(flet ($e187 (or $e111 $e94)) +(flet ($e188 (xor $e144 $e177)) +(flet ($e189 (implies $e185 $e188)) +(flet ($e190 (not $e167)) +(flet ($e191 (xor $e115 $e155)) +(flet ($e192 (and $e95 $e179)) +(flet ($e193 (iff $e180 $e182)) +(flet ($e194 (or $e88 $e131)) +(flet ($e195 (iff $e123 $e168)) +(flet ($e196 (xor $e106 $e194)) +(flet ($e197 (iff $e170 $e191)) +(flet ($e198 (iff $e196 $e117)) +(flet ($e199 (and $e71 $e197)) +(flet ($e200 (or $e119 $e108)) +(flet ($e201 (not $e163)) +(flet ($e202 (iff $e183 $e201)) +(flet ($e203 (implies $e178 $e91)) +(flet ($e204 (or $e142 $e175)) +(flet ($e205 (not $e145)) +(flet ($e206 (and $e146 $e132)) +(flet ($e207 (if_then_else $e173 $e147 $e20)) +(flet ($e208 (or $e195 $e166)) +(flet ($e209 (and $e35 $e79)) +(flet ($e210 (if_then_else $e69 $e75 $e184)) +(flet ($e211 (not $e199)) +(flet ($e212 (iff $e204 $e143)) +(flet ($e213 (xor $e161 $e89)) +(flet ($e214 (iff $e114 $e114)) +(flet ($e215 (not $e214)) +(flet ($e216 (xor $e186 $e189)) +(flet ($e217 (implies $e212 $e24)) +(flet ($e218 (xor $e136 $e202)) +(flet ($e219 (not $e213)) +(flet ($e220 (iff $e135 $e198)) +(flet ($e221 (iff $e169 $e128)) +(flet ($e222 (implies $e207 $e187)) +(flet ($e223 (or $e219 $e211)) +(flet ($e224 (and $e223 $e137)) +(flet ($e225 (and $e205 $e109)) +(flet ($e226 (xor $e200 $e220)) +(flet ($e227 (implies $e208 $e226)) +(flet ($e228 (if_then_else $e193 $e222 $e192)) +(flet ($e229 (xor $e227 $e210)) +(flet ($e230 (and $e216 $e217)) +(flet ($e231 (not $e218)) +(flet ($e232 (implies $e225 $e203)) +(flet ($e233 (xor $e221 $e140)) +(flet ($e234 (xor $e224 $e232)) +(flet ($e235 (if_then_else $e233 $e231 $e181)) +(flet ($e236 (if_then_else $e206 $e228 $e215)) +(flet ($e237 (implies $e236 $e85)) +(flet ($e238 (implies $e229 $e235)) +(flet ($e239 (or $e190 $e237)) +(flet ($e240 (or $e234 $e230)) +(flet ($e241 (iff $e238 $e127)) +(flet ($e242 (not $e240)) +(flet ($e243 (iff $e239 $e241)) +(flet ($e244 (if_then_else $e243 $e242 $e243)) +(flet ($e245 (xor $e244 $e244)) +(flet ($e246 (iff $e209 $e245)) +$e246 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |