[541] % z3release model_validate=true small.smt2
sat
[542] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unexpected SAT
ASSERTION VIOLATION
File: ../src/sat/smt/sat_dual_solver.cpp
Line: 144
UNEXPECTED CODE WAS REACHED.
Z3 4.8.13.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[543] % 
[543] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun i () Real)
(assert (distinct (= c 0 0 e 0 f d)))
(assert
 (not
  (exists ((g Real))
   (=>
    (distinct
     (not
      (exists ((h Real))
       (=> (= c 0) (= (= (= h 0) (= 0 c)) (= b 0)))))
     (= 0 i a))
    (= 0 d)))))
(check-sat)
[544] %