(smt.arith.eager_eq_axioms, consequence) Assertion error at src/smt/smt_consequences.cpp:662

[rainoftime]

Hi, for the following formula
z3 7b3a587

(set-option :smt.arith.eager_eq_axioms false)
(declare-fun z () Int)
(declare-fun y () Int)
(declare-fun x () Int)
(declare-fun named3 () Bool)
(declare-fun named5 () Bool)
(declare-fun named6 () Bool)
(declare-fun named7 () Bool)
(assert (and (= y (+ x 1)) (= 1 (* z z))))
(assert (or named6 (not named3)))
(assert (or (not named5) (= y 0)))
(assert (or named7 (= z y)))
(get-consequences (named5) (named3 named7))

z3 delta.out.smt2 
ASSERTION VIOLATION
File: ../src/smt/smt_consequences.cpp
Line: 662
is_sat != l_false
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB