From f4d03edf22c322934568d2581274eee13f013493 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 16 Dec 2018 15:54:30 -0800 Subject: [PATCH] remove unreachable Signed-off-by: Nikolaj Bjorner --- src/math/polynomial/upolynomial_factorization.cpp | 2 +- src/smt/theory_pb.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/math/polynomial/upolynomial_factorization.cpp b/src/math/polynomial/upolynomial_factorization.cpp index 57106e22d..5eaf10c88 100644 --- a/src/math/polynomial/upolynomial_factorization.cpp +++ b/src/math/polynomial/upolynomial_factorization.cpp @@ -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(); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 8a880b1cf..e0ba902b3 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -1187,7 +1187,7 @@ namespace smt { */ void theory_pb::assign_eq(ineq& c, bool is_true) { SASSERT(c.is_eq()); - UNREACHABLE(); + }