mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
remove unreachable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
2dcf36e96c
commit
f4d03edf22
|
@ -1072,7 +1072,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs,
|
|||
prime_iterator prime_it;
|
||||
scoped_numeral gcd_tmp(nm);
|
||||
unsigned trials = 0;
|
||||
while (trials < params.m_p_trials) {
|
||||
while (trials <= params.m_p_trials) {
|
||||
upm.checkpoint();
|
||||
// construct prime to check
|
||||
uint64_t next_prime = prime_it.next();
|
||||
|
|
|
@ -1187,7 +1187,7 @@ namespace smt {
|
|||
*/
|
||||
void theory_pb::assign_eq(ineq& c, bool is_true) {
|
||||
SASSERT(c.is_eq());
|
||||
UNREACHABLE();
|
||||
|
||||
}
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue