Soundness issue with nlsat.shuffle_vars=true

[wintered]

[808] % z3release small.smt2
sat
[809] % z3release nlsat.shuffle_vars=true rewriter.cache_all=true small.smt2
unsat
[810] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert (forall ((e Real))
  (not (=>
     (= (<= 0 e b) (>= c (* e e)))
     (= c (* (- (+ a 1) d) (- (+ a 1) d)))
     (>= d 0)))))
(check-sat)
[811] %

OS: Ubuntu 18.04
Commit: 03e411c

[NikolajBjorner]

Would be great if you could spare me the triaging for these duplicate bugs #2650

C:\zzz\build>z3 3914.smt2 nlsat.check_lemmas=true
check lemma: b7
check
check lemma: b5 or !b7 or !(x2 < 0)
check
check lemma: b5 or !b7
check
check lemma: b5
check
check lemma: b7 or !(4 x1 < 0)
check
check lemma: b7 or !(x0 + 1 > 0) or !(4 x1 > 0) or !(- x1 + x0^2 + 2 x0 + 1 > 0)
check
check lemma: b7 or !(- x1 + x0^2 + 2 x0 + 1 > 0) or !(x1 = 0)
check
true := l_true
x3 < 0 := l_false
b2 := l_false
x4 - x3 < 0 := l_false
x3^2 - x1 > 0 := l_false
b5 := l_false
x2 < 0 := l_true
b7 := l_false
x2^2 - 2 x0 x2 - 2 x2 - x1 + x0^2 + 2 x0 + 1 = 0 := l_true
b9 := l_true
4 x1 < 0 := l_false
4 x1 > 0 := l_false
- x1 + x0^2 + 2 x0 + 1 > 0 := l_true
x0 + 1 > 0 := l_false
x1 = 0 := l_true
violdated tautology clause: !(x1 = 0) or !(- x1 + x0^2 + 2 x0 + 1 > 0) or !(x2^2 - 2 x0 x2 - 2 x2 - x1 + x0^2 + 2 x0 + 1 = 0) or !(x2 < 0)
ASSERTION VIOLATION
File: ..\src\nlsat\nlsat_solver.cpp
Line: 905
UNREACHABLE CODE WAS REACHED.