Debug branch, emonics, segmentation fault on NRA formula #3203
Description
Hi,
For this formula:
(declare-fun a () Real)
(declare-fun mWoMy_new () Real)
(declare-fun d () Real)
(declare-fun af () Real)
(declare-fun ag () Real)
(declare-fun j () Real)
(declare-fun b () Real)
(declare-fun ah () Real)
(declare-fun c () Real)
(declare-fun aj () Real)
(declare-fun ai () Real)
(declare-fun e () Real)
(declare-fun aa () Real)
(declare-fun ctphm_new () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(declare-fun s () Real)
(declare-fun t () Real)
(declare-fun u () Real)
(declare-fun ep () Real)
(declare-fun v () Real)
(declare-fun w () Real)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun ab () Real)
(declare-fun ak () Real)
(declare-fun ac () Real)
(declare-fun ad () Real)
(declare-fun ae () Real)
(assert
(not
(exists ((o Real))
(or
(and
(or
(and
(or
(and
(or
(and
(distinct (- d) d)
(= (- ai w) 0.0 (- b (- ah o)))
(distinct (/ 7 b (+ 27 ah o)) 2.0) (= p 2.0))
(>= (+ s (* 0 (* 2.0 (- (- 1 aj r))))) 0)
(distinct q 2.0))
(< 0 r ag))
(> 0.0 h))
(<= h u))
(<= 0.0 l)
(> l u))
(>= 0.0 (* af (- j l)))
(<= 0.0 u))
(< 0.0 ep)
(and
(= (* e x) (- g ac))
(> 0.0 (- mWoMy_new (- j)))
(=>
(=>
(or (<= 0.0 o) (<= o (- mWoMy_new (* 9 j l))))
(and
(<= (- ai w) u)
(<= 0.0 (+ (* (+ 41 af) o) m))
(>= (+ (* (- af (/ 76 j l)) o) m) u)
(<= (+ o 0.0) ep)))
(= c 2.0)))))))
(assert
(not
(exists ((f Real))
(=>
(and
(or
(and
(or
(and
(=>
(<= 0.0 (- ctphm_new ep))
(<= (- 5 ctphm_new ep) 0)
(or
(and
(<= 0.0 (+ (* (* (* 6 1.0) ak) (- 255 ctphm_new ep)) (- aa u)))
(<= (+ (* (* 4 ak) (+ 11 ctphm_new ep)) 0) y))
(< ctphm_new ad)))
(<= 0.0 (- a h)))
(<= 0.0 (- aa u)))
(>= (- aa u) y)))
(<= 0.0 (- 8 b n))
(<= n y (+ 9 mWoMy_new i))
(< 0.0 y)
(< 0.0 ad))
(or (= ae 2.0) (<= (/ 91 (* (- (- 1.0) ak) (- a h)) (- aa u)) y))))))
(assert (= a (+ h ac)))
(assert (= mWoMy_new (* i z)))
(assert (= af (+ k z)))
(assert (= j (+ l z)))
(assert (= b (+ n w)))
(assert (= ah (+ o w)))
(assert (= e (/ t x)))
(assert (= aa (+ u ab)))
(assert (= g (/ v ac)))
(check-sat)
Z3 debug branch throws out a segmentation fault.
OS: Ubuntu 18.04
Commit: d68c114