na

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Aug 24, 2020 · 6beec7b · 6beec7b
1 parent dc1783a
commit 6beec7b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git 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
@@ -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));
         }