diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index b073728cc..0d6e83f35 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -421,6 +421,8 @@ namespace polysat {
         m_dedup.m_quot_rem_expr.insert(args, { q.var(), r.var() });
         m_dedup.m_div_rem_list.push_back({ a, b, q.var(), r.var() });
 
+        LOG("quot_rem(" << a << ", " << b << ") = (" << q << ", " << r << ")");
+
         // Axioms for quotient/remainder:
         //      a = b*q + r
         //      multiplication does not overflow in b*q
@@ -443,8 +445,10 @@ namespace polysat {
 #endif
 
         auto c_eq = eq(b);
-        s.add_clause("[axiom] quot_rem 4", {  c_eq, ult(r, b)  }, false);
-        s.add_clause("[axiom] quot_rem 5", { ~c_eq, eq(q + 1)  }, false);
+        if (!c_eq.is_always_true())
+            s.add_clause("[axiom] quot_rem 4", {  c_eq, ult(r, b)  }, false);
+        if (!c_eq.is_always_false())
+            s.add_clause("[axiom] quot_rem 5", { ~c_eq, eq(q + 1)  }, false);
 
         return {std::move(q), std::move(r)};
     }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 67e70015f..633761b73 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1387,9 +1387,9 @@ namespace polysat {
 
     clause_ref solver::mk_clause(char const* name, unsigned n, signed_constraint const* cs, bool is_redundant) {
         clause_builder cb(*this, name);
+        cb.set_redundant(is_redundant);
         for (unsigned i = 0; i < n; ++i)
             cb.insert(cs[i]);
-        cb.set_redundant(is_redundant);
         return cb.build();
     }