diff --git a/src/ast/euf/euf_justification.h b/src/ast/euf/euf_justification.h
index dff67a4d5..68d7d214f 100644
--- a/src/ast/euf/euf_justification.h
+++ b/src/ast/euf/euf_justification.h
@@ -53,6 +53,7 @@ namespace euf {
         
         bool   is_external() const { return m_kind == external_t; }
         bool   is_congruence() const { return m_kind == congruence_t; }
+        bool   is_commutative() const { return m_comm; }
         template <typename T>
         T*  ext() const { SASSERT(is_external()); return static_cast<T*>(m_external); }            
     };
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index df11184a4..e9d02611e 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -1855,8 +1855,8 @@ seq_util::rex::info seq_util::rex::info::diff(seq_util::rex::info const& rhs) co
 seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) const {
     if (is_known()) {
         if (i.is_known()) {
-            unsigned ite_min_length = std::min(min_length, i.min_length);
-            lbool ite_nullable = (nullable == i.nullable ? nullable : l_undef);
+            // unsigned ite_min_length = std::min(min_length, i.min_length);
+            // lbool ite_nullable = (nullable == i.nullable ? nullable : l_undef);
             //TBD: whether ite is interpreted or not depends on whether the condition is interpreted and both branches are interpreted
             return info(false, false, false, false, normalized && i.normalized, monadic && i.monadic, singleton && i.singleton, nullable, min_length, std::max(star_height, i.star_height));
         }