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();
+        
     }