diff --git a/src/math/polysat/mul_ovfl_constraint.h b/src/math/polysat/mul_ovfl_constraint.h
index 075509d3b..8932c10d6 100644
--- a/src/math/polysat/mul_ovfl_constraint.h
+++ b/src/math/polysat/mul_ovfl_constraint.h
@@ -38,8 +38,8 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const override;
         bool is_always_false(bool is_positive) const override;
         void narrow(solver& s, bool is_positive) override;
-        bool is_currently_false(solver & s, bool is_positive) const;
-        bool is_currently_true(solver& s, bool is_positive) const;
+        bool is_currently_false(solver & s, bool is_positive) const override;
+        bool is_currently_true(solver& s, bool is_positive) const override;
         bool is_currently_false(solver& s, assignment_t const& sub, bool is_positive) const override { return false; }
         bool is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const override { return false; }
 
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 44583e735..2f5b7e344 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -144,10 +144,10 @@ namespace polysat {
         // Axioms for quotient/remainder:
         //      a = b*q + r
         //      multiplication does not overflow in b*q
-        //      addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r
+        //      addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r    (TODO: maybe the version with disjunction is easier for the solver; should compare later)
         //      b ≠ 0  ==>  r < b
         //      b = 0  ==>  q = -1
-        add_eq(b * q + r - a);
+        add_eq(a, b * q + r);
         add_noovfl(b, q);
         add_ule(r, b*q+r);
 
@@ -1082,8 +1082,22 @@ namespace polysat {
                 all_ok = all_ok && ok;
             }
         }
+        for (auto clauses : m_constraints.clauses()) {
+            for (auto cl : clauses) {
+                bool clause_ok = false;
+                for (sat::literal lit : *cl) {
+                    bool ok = lit2cnstr(lit).is_currently_true(*this);
+                    if (ok) {
+                        clause_ok = true;
+                        break;
+                    }
+                }
+                LOG((clause_ok ? "PASS" : "FAIL") << ": " << show_deref(cl) << (cl->is_redundant() ? " (redundant)" : ""));
+                all_ok = all_ok && clause_ok;
+            }
+        }
         if (all_ok) LOG("All good!");
-        return true;
+        return all_ok;
     }
 }