(nlsat.shuffle_vars=true rewriter.eq2ineq=true)

[wintered]

[550] % z3release small.smt2
sat
[551] % cvc4 -q small.smt2
sat
[552] % z3release nlsat.shuffle_vars=true rewriter.eq2ineq=true small.smt2
unsat
[553] % 
[553] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun g () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun j () Real)
(declare-fun h () Real)
(assert
 (not
 (exists ((i Real))
  (=> (>= b 0)
  (> f (+ j (* b b) (* (+ (/ c d) 1) b)) a g 0)
  (= e 0)
  (not (= f j h))))))
(check-sat)
[554] %

Commit: 020e639

[zhendongsu]

Another quantifier-free instance:

[547] % z3release small.smt2
sat
[548] % cvc4 -q small.smt2
sat
[549] % z3release nlsat.shuffle_vars=true rewriter.eq2ineq=true small.smt2
unsat
[550] % 
[550] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (> (* a (+ 1 (ite (> a 1) (* a (- (* a 2) 1)) 0))) 1))
(assert (= (- (* a a) 1) 1 b c))
(check-sat)
[551] % 

[zhendongsu]

Another quantifier-free instance:

[610] % z3release small.smt2
sat
[611] % z3release nlsat.shuffle_vars=true nlsat.simplify_conflicts=false small.smt2
unsat
[612] % z3release nlsat.shuffle_vars=true rewriter.eq2ineq=true small.smt2
unsat
[613] % 
[613] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (> a 0))
(assert (> b 0))
(assert (= (+ a 1) (* a (- a 1)) (* b b)))
(assert (not (= c 0)))
(assert (<= (/ c c) 1))
(check-sat)
[614] % 

Commit: c0e74f9

[NikolajBjorner]

duplicate #2650