Assertion violation at smtrat-modules/SATModule/SATModule.cpp:3137 (mcsat)

[rainoftime]

Hi, for the following formula,

(set-logic QF_NRA)
(declare-fun v0 () Real)
(assert (let ((e1 500)) (let ((e2 872642651)) (let ((e3 61)) (let ((e4 951)) (let ((e5 3249)) (let ((e6 (/ e3 (- e2)))) (let ((e7 (+ e6 v0))) (let ((e8 (* (- e3) e7))) (let ((e9 (- e6))) (let ((e10 (* e8 e9))) (let ((e11 (- e9 e9))) (let ((e12 (/ e1 (- e1)))) (let ((e13 (/ e2 e3))) (let ((e14 (- e13))) (let ((e15 (* e14 e3))) (let ((e16 (- e9))) (let ((e17 (* e13 e13))) (let ((e18 (* e9 (- e4)))) (let ((e19 (- e11 e6))) (let ((e20 (/ e5 e1))) (let ((e21 (= e10 e13))) (let ((e22 (> e12 e12))) (let ((e23 (>= e18 v0))) (let ((e24 (= e10 e15))) (let ((e25 (= e20 e8))) (let ((e26 (< e11 v0))) (let ((e27 (>= v0 e14))) (let ((e28 (<= e17 e11))) (let ((e29 (= e6 v0))) (let ((e30 (>= e17 e10))) (let ((e31 (<= e20 e11))) (let ((e32 (distinct e12 e11))) (let ((e33 (distinct v0 e19))) (let ((e34 (>= e7 e17))) (let ((e35 (> e9 e9))) (let ((e36 (> e15 e20))) (let ((e37 (< v0 e15))) (let ((e38 (distinct e16 e20))) (let ((e39 (ite e36 e6 e9))) (let ((e40 (ite e21 e16 e15))) (let ((e41 (ite e29 e20 e11))) (let ((e42 (ite e27 e12 e8))) (let ((e43 (ite e33 e16 e18))) (let ((e44 (ite e27 e43 e8))) (let ((e45 (ite e24 e10 e20))) (let ((e46 (ite e25 e16 e39))) (let ((e47 (ite e36 e41 e11))) (let ((e48 (ite e28 e17 e40))) (let ((e49 (ite e22 e14 e7))) (let ((e50 (ite e32 v0 e39))) (let ((e51 (ite e35 e49 e20))) (let ((e52 (ite e26 e41 e40))) (let ((e53 (ite e31 e43 e43))) (let ((e54 (ite e37 e19 e39))) (let ((e55 (ite e38 e13 e40))) (let ((e56 (ite e23 e55 e48))) (let ((e57 (ite e34 e10 0.0))) (let ((e58 (ite e36 e13 e10))) (let ((e59 (ite e30 e9 e20))) (let ((e60 (= e43 e45))) (let ((e61 (distinct e42 e48))) (let ((e62 (distinct e9 e12))) (let ((e63 (< e19 e40))) (let ((e64 (<= e56 e59))) (let ((e65 (< v0 e10))) (let ((e66 (<= e13 e51))) (let ((e67 (distinct e55 e53))) (let ((e68 (< e13 e10))) (let ((e69 (<= e42 e58))) (let ((e70 (= e58 e6))) (let ((e71 (= e13 e18))) (let ((e72 (<= e51 e58))) (let ((e73 (<= e53 e7))) (let ((e74 (distinct e17 e12))) (let ((e75 (>= e59 e10))) (let ((e76 (<= e41 e49))) (let ((e77 (< e19 e40))) (let ((e78 (distinct e10 e58))) (let ((e79 (= e12 e42))) (let ((e80 (< 0.0 e15))) (let ((e81 (distinct e41 e13))) (let ((e82 (distinct e53 e18))) (let ((e83 (> e18 e10))) (let ((e84 (<= e19 e42))) (let ((e85 (>= e6 0.0))) (let ((e86 (< e39 e8))) (let ((e87 (> e43 e9))) (let ((e88 (<= e6 e43))) (let ((e89 (< e46 e50))) (let ((e90 (= e6 e10))) (let ((e91 (< e53 e49))) (let ((e92 (= e7 e52))) (let ((e93 (>= e7 e13))) (let ((e94 (> e7 e45))) (let ((e95 (= e41 e11))) (let ((e96 (<= e52 e12))) (let ((e97 (<= e58 e19))) (let ((e98 (distinct e58 e41))) (let ((e99 (distinct e11 e6))) (let ((e100 (> e44 e41))) (let ((e101 (< e51 e13))) (let ((e102 (>= e40 e45))) (let ((e103 (<= e12 e49))) (let ((e104 (<= e44 0.0))) (let ((e105 (distinct e58 e7))) (let ((e106 (= e53 e13))) (let ((e107 (distinct e53 e7))) (let ((e108 (= 0.0 e14))) (let ((e109 (> e58 e48))) (let ((e110 (<= v0 e42))) (let ((e111 (distinct e58 e58))) (let ((e112 (> e39 e58))) (let ((e113 (<= 0.0 e14))) (let ((e114 (< e18 e44))) (let ((e115 (<= e45 e15))) (let ((e116 (> e43 e47))) (let ((e117 (> e48 e40))) (let ((e118 (> e16 e58))) (let ((e119 (> e43 e48))) (let ((e120 (= e49 e17))) (let ((e121 (>= e47 e15))) (let ((e122 (distinct e53 e8))) (let ((e123 (distinct e58 e7))) (let ((e124 (> e43 0.0))) (let ((e125 (distinct e47 e15))) (let ((e126 (distinct v0 e17))) (let ((e127 (distinct e49 e12))) (let ((e128 (<= 0.0 0.0))) (let ((e129 (> e17 e52))) (let ((e130 (distinct e39 e51))) (let ((e131 (> e10 e8))) (let ((e132 (>= e7 e48))) (let ((e133 (<= e15 e19))) (let ((e134 (<= e7 e7))) (let ((e135 (< e9 e55))) (let ((e136 (>= e48 v0))) (let ((e137 (= e11 e11))) (let ((e138 (= e40 e40))) (let ((e139 (distinct e45 e49))) (let ((e140 (> e6 e44))) (let ((e141 (distinct e43 e18))) (let ((e142 (<= e43 e15))) (let ((e143 (> e42 e40))) (let ((e144 (>= e14 e15))) (let ((e145 (> e59 e15))) (let ((e146 (> e9 e17))) (let ((e147 (distinct e48 e52))) (let ((e148 (>= e9 e14))) (let ((e149 (<= e41 e45))) (let ((e150 (> e8 e9))) (let ((e151 (distinct e44 e20))) (let ((e152 (xor e92 e38))) (let ((e153 (not e62))) (let ((e154 (not e72))) (let ((e155 (not e63))) (let ((e156 (ite e122 e70 e79))) (let ((e157 (not e94))) (let ((e158 (ite e78 e117 e121))) (let ((e159 (=> e22 e87))) (let ((e160 (ite e135 e77 e151))) (let ((e161 (=> e91 e131))) (let ((e162 (or e145 e115))) (let ((e163 (= e71 e150))) (let ((e164 (= e119 e29))) (let ((e165 (xor e37 e75))) (let ((e166 (= e28 e126))) (let ((e167 (not e146))) (let ((e168 (=> e34 e163))) (let ((e169 (and e157 e100))) (let ((e170 (xor e147 e167))) (let ((e171 (not e30))) (let ((e172 (not e113))) (let ((e173 (not e164))) (let ((e174 (= e155 e27))) (let ((e175 (ite e133 e128 e106))) (let ((e176 (xor e108 e68))) (let ((e177 (or e98 e143))) (let ((e178 (ite e60 e25 e81))) (let ((e179 (xor e107 e69))) (let ((e180 (or e67 e158))) (let ((e181 (ite e148 e166 e80))) (let ((e182 (=> e136 e134))) (let ((e183 (ite e140 e129 e31))) (let ((e184 (= e130 e123))) (let ((e185 (ite e165 e153 e165))) (let ((e186 (not e175))) (let ((e187 (or e172 e74))) (let ((e188 (xor e161 e21))) (let ((e189 (or e73 e89))) (let ((e190 (= e118 e188))) (let ((e191 (=> e112 e64))) (let ((e192 (or e149 e125))) (let ((e193 (and e192 e132))) (let ((e194 (= e152 e144))) (let ((e195 (=> e104 e33))) (let ((e196 (or e137 e82))) (let ((e197 (not e178))) (let ((e198 (=> e180 e189))) (let ((e199 (= e101 e26))) (let ((e200 (= e65 e197))) (let ((e201 (=> e169 e120))) (let ((e202 (or e76 e162))) (let ((e203 (not e93))) (let ((e204 (=> e127 e182))) (let ((e205 (= e96 e90))) (let ((e206 (and e203 e61))) (let ((e207 (ite e141 e32 e32))) (let ((e208 (or e173 e183))) (let ((e209 (= e168 e177))) (let ((e210 (= e85 e171))) (let ((e211 (or e160 e95))) (let ((e212 (not e205))) (let ((e213 (xor e35 e196))) (let ((e214 (=> e176 e206))) (let ((e215 (xor e97 e187))) (let ((e216 (ite e209 e184 e190))) (let ((e217 (= e110 e154))) (let ((e218 (ite e102 e83 e88))) (let ((e219 (ite e86 e218 e216))) (let ((e220 (=> e36 e124))) (let ((e221 (xor e114 e204))) (let ((e222 (xor e170 e214))) (let ((e223 (xor e84 e217))) (let ((e224 (= e156 e179))) (let ((e225 (= e193 e199))) (let ((e226 (and e186 e159))) (let ((e227 (= e202 e211))) (let ((e228 (not e23))) (let ((e229 (xor e223 e109))) (let ((e230 (not e224))) (let ((e231 (or e194 e219))) (let ((e232 (=> e229 e208))) (let ((e233 (=> e232 e221))) (let ((e234 (xor e174 e230))) (let ((e235 (= e142 e66))) (let ((e236 (not e210))) (let ((e237 (= e195 e234))) (let ((e238 (not e185))) (let ((e239 (and e212 e138))) (let ((e240 (= e111 e235))) (let ((e241 (ite e213 e231 e239))) (let ((e242 (= e139 e181))) (let ((e243 (ite e201 e207 e225))) (let ((e244 (= e99 e99))) (let ((e245 (not e105))) (let ((e246 (ite e242 e245 e220))) (let ((e247 (not e198))) (let ((e248 (= e200 e226))) (let ((e249 (not e241))) (let ((e250 (ite e116 e24 e233))) (let ((e251 (and e246 e246))) (let ((e252 (=> e250 e215))) (let ((e253 (ite e244 e227 e238))) (let ((e254 (not e253))) (let ((e255 (ite e254 e254 e251))) (let ((e256 (ite e243 e240 e249))) (let ((e257 (not e248))) (let ((e258 (or e191 e257))) (let ((e259 (or e252 e103))) (let ((e260 (and e247 e237))) (let ((e261 (xor e222 e228))) (let ((e262 (= e236 e261))) (let ((e263 (and e256 e256))) (let ((e264 (= e255 e260))) (let ((e265 (or e264 e262))) (let ((e266 (not e263))) (let ((e267 (ite e265 e258 e265))) (let ((e268 (= e259 e259))) (let ((e269 (xor e268 e266))) (let ((e270 (not e267))) (let ((e271 (not e270))) (let ((e272 (= e271 e271))) (let ((e273 (= e272 e272))) (let ((e274 (= e269 e273))) e274)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

smtrat 0e70dd2

smtrat-shared: /home/peisen/test/tofuzz/smtrat/src/smtrat-modules/SATModule/SATModule.cpp:3137: void smtrat::SATModule<Settings>::handleConflict(Minisat::CRef) [with Settings = smtrat::SATSettingsMCSATFMICPVSOC; Minisat::CRef = unsigned int]: Assertion `assumptions.size() <= backtrack_level' failed.

set(SMTRAT_Strategy "MCSATFMICPVSOC" CACHE STRING "Used strategy in the solver")