diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp
index b8b5384fc..c5b1fc80e 100644
--- a/src/math/polysat/op_constraint.cpp
+++ b/src/math/polysat/op_constraint.cpp
@@ -183,8 +183,6 @@ namespace polysat {
         case code::lshr_op:
             break;
         case code::shl_op:
-            // TODO: if shift amount is constant p << k, then add p << k == p*2^k
-            //       NOTE: we do that now as simplification in constraint_manager::shl
             break;
         case code::and_op:
             // handle masking of high order bits
@@ -643,7 +641,7 @@ namespace polysat {
         if (rv.is_zero())
             return s.mk_clause(~invc, ~s.eq(r()), s.eq(p()), true);
 
-        // p assigned  ==>  r = pseudo_inverse(eval(p))
+        // forward propagation: p assigned  ==>  r = pseudo_inverse(eval(p))
         // TODO: (later) this should be propagated instead of adding a clause
         if (pv.is_val() && !rv.is_val())
             return s.mk_clause(~invc, ~s.eq(p(), pv), s.eq(r(), pv.val().pseudo_inverse(m.power_of_2())), true);
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 8942dd160..43707e395 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1229,7 +1229,7 @@ namespace polysat {
     clause_ref solver::mk_clause(unsigned n, signed_constraint const* cs, bool is_redundant) {
         clause_builder cb(*this);
         for (unsigned i = 0; i < n; ++i)
-            cb.insert(cs[i]);
+            cb.insert_try_eval(cs[i]);
         cb.set_redundant(is_redundant);
         return cb.build();
     }