From 50d334e4e960300361bddc80cd1b6a8027d7c386 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 27 May 2016 07:51:02 -0700 Subject: [PATCH] fix non-determinism bug in simple joins. Keys were normalized based on pointer equality not object identifier equality. Also some ptr hashtables were used with pointer hashes, and then traversed. reported in issue #619 Signed-off-by: Nikolaj Bjorner --- src/muz/rel/dl_mk_simple_joins.cpp | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/muz/rel/dl_mk_simple_joins.cpp b/src/muz/rel/dl_mk_simple_joins.cpp index ad6173637..e428fdd2e 100644 --- a/src/muz/rel/dl_mk_simple_joins.cpp +++ b/src/muz/rel/dl_mk_simple_joins.cpp @@ -253,17 +253,10 @@ namespace datalog { if (t1n->get_id() > t2n->get_id()) { std::swap(t1n, t2n); } + m_pinned.push_back(t1n); m_pinned.push_back(t2n); - /* - IF_VERBOSE(0, - print_renaming(norm_subst, verbose_stream()); - display_predicate(m_context, t1, verbose_stream()); - display_predicate(m_context, t2, verbose_stream()); - display_predicate(m_context, t1n, verbose_stream()); - display_predicate(m_context, t2n, verbose_stream());); - */ return app_pair(t1n, t2n); }