diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 17d3e7ecd..26ca34c6f 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -659,7 +659,7 @@ namespace polysat {
         LOG(assignment_pp(*this, v, val) << " by " << j);
         SASSERT(m_viable.is_viable(v, val));
         SASSERT(j.is_decision() || j.is_propagation());
-        SASSERT(j.level() == m_level);
+        SASSERT(j.level() <= m_level);
         SASSERT(!is_assigned(v));
         SASSERT(all_of(assignment(), [v](auto p) { return p.first != v; }));
         m_value[v] = val;
diff --git a/src/test/hashtable.cpp b/src/test/hashtable.cpp
index befd0b8e9..57860a294 100644
--- a/src/test/hashtable.cpp
+++ b/src/test/hashtable.cpp
@@ -26,7 +26,7 @@ Revision History:
 
 struct int_hash_proc { unsigned operator()(int x) const { return x * 3; } };
 typedef int_hashtable<int_hash_proc, default_eq<int> > int_set;
-typedef std::unordered_set<int, std::hash_compare<int, std::less<int> > > safe_int_set;
+typedef std::unordered_set<int> safe_int_set;
 // typedef safe_int_set int_set;
 
 inline bool contains(int_set & h, int i) {