na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Sep 10, 2020 · f4e8205 · f4e8205
1 parent cfa7c73
commit f4e8205
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 7 deletions.
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
@@ -169,7 +169,7 @@ namespace euf {
             e = m_var2expr[l.var()];
             n = m_egraph.find(e);
             SASSERT(n);
-            SASSERT(m.is_bool(n->get_owner()));
+            SASSERT(m.is_bool(n->get_expr()));
             m_egraph.explain_eq<size_t>(m_explain, n, (l.sign() ? mk_false() : mk_true()));
             break;
         default:

diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
@@ -165,13 +165,11 @@ namespace smt {
 
         void del_eh(ast_manager & m, bool update_children_parent = true);
 
-        app * get_owner() const { 
-            return m_owner; 
-        }
+        app * get_owner() const { return m_owner; }
+        app * get_expr() const { return m_owner; }
 
-        unsigned get_owner_id() const {
-            return m_owner->get_id();
-        }
+        unsigned get_owner_id() const { return m_owner->get_id(); }
+        unsigned get_expr_id() const { return m_owner->get_id(); }
 
         func_decl * get_decl() const {
             return m_owner->get_decl();