mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
remove unneeded assertion fix #5131
This commit is contained in:
parent
dfb696becf
commit
6bdf377e11
|
@ -3072,7 +3072,6 @@ public:
|
|||
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);
|
||||
|
|
Loading…
Reference in a new issue