mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
remove redundant assertion
This commit is contained in:
parent
5cc29bec14
commit
2fdb703865
|
@ -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);
|
||||
|
|
Loading…
Reference in a new issue