mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

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

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-27 07:51:02 -07:00
parent cfffb0b3c5
commit 50d334e4e9
1 changed files with 1 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/muz/rel/dl_mk_simple_joins.cpp
View file

@ -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);
}