From 8fd2d8a636b65ca9e5d13bcc7f327e34ec40a09f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 6 Apr 2018 15:56:05 -0500 Subject: [PATCH] chore(datatype): small fixes --- src/smt/theory_datatype.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index f17bdc3d6..825856e37 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -452,7 +452,7 @@ namespace smt { SASSERT(app->get_root() == root->get_root()); if (app != root) - m_used_eqs.push_back(enode_pair(app, root)); + m_used_eqs.push_back(enode_pair(app, root)); } // start exploring subgraph below `app` @@ -511,7 +511,7 @@ namespace smt { switch (op) { case ENTER: - res = occurs_check_enter(app) || res; + res = occurs_check_enter(app); break; case EXIT: