diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index 49aeb1ec6..ebc79cffb 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -496,7 +496,6 @@ namespace arith { return; if (x->get_root() == y->get_root()) return; - SASSERT(a.is_numeral(y->get_expr())); reset_evidence(); set_evidence(ci1, m_core, m_eqs); set_evidence(ci2, m_core, m_eqs);