Debug branch, emonics: segfault LRA

[wintered]

Hi,
on the following formula Z3 throws a segfault

(declare-fun a () Real)
(assert
 (forall ((b Real) (c Real))
  (or
   (and (>= (+ (/ 2 c) b (* 3 a)) (- 50))
    (not (= (+ (* (- 100) c) (/ 5 a)) 0))
    (not (= (- (- b) (* 100 a)) 5)))
   (and (<= (+ (- (* (- 100) c) (* 50 b)) (* (- 100) a)) 8)
    (= (+ (* (- 20 c) (* 10 b)) (/ 80 a)) 4)
    (not (= (+ (- b) (/ 3 a)) 0))))))
(check-sat)

OS: Ubuntu 18.04
Commit: e0411c1

[NikolajBjorner]

it asserts in emonics.
The logic dealing with push/pop and how equivalence classes are managed seems not right.:
I see a pop triggers a merge while the union-find structure gets updated. This is should not happen..
Debugging this isn't not straight-forward: the expectation is that pop doesn't create new equalities, so we could add some state to the union-find structure or to emons that it doesn't trigger a merge during pop.

[NikolajBjorner]

emons was rewritten. This one is stale