diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp
index fd08b1aad..1ea705e6e 100644
--- a/src/muz_qe/pdr_util.cpp
+++ b/src/muz_qe/pdr_util.cpp
@@ -1129,7 +1129,11 @@ namespace pdr {
             if (a.is_numeral(lhs) || a.is_numeral(rhs)) {
                 return test_ineq(e);
             }
-            return test_term(lhs) && test_term(rhs);
+            return 
+                test_term(lhs) && 
+                test_term(rhs) &&
+                !a.is_mul(lhs) &&
+                !a.is_mul(rhs);
         }
 
         bool test_term(expr* e) const {
diff --git a/src/muz_qe/proof_utils.cpp b/src/muz_qe/proof_utils.cpp
index 75c9cbb15..1e837b578 100644
--- a/src/muz_qe/proof_utils.cpp
+++ b/src/muz_qe/proof_utils.cpp
@@ -312,9 +312,10 @@ public:
 };
 
 void proof_utils::reduce_hypotheses(proof_ref& pr) {
-    class reduce_hypotheses reduce(pr.get_manager());
+    ast_manager& m = pr.get_manager();
+    class reduce_hypotheses reduce(m);
     reduce(pr);
-    SASSERT(is_closed(pr.get_manager(), pr));
+    CTRACE("proof_utils", !is_closed(m, pr), tout << mk_pp(pr, m) << "\n";);
 }
 
 class proof_is_closed {