mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

program the simple joints a bit more defensively per bugs reported by Sean McLaughlin

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-31 10:42:41 -08:00
parent e63724a22d
commit 38865ffe0d
1 changed files with 12 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -11,7 +11,7 @@ Abstract:
Author:
Leonardo de Moura (leonardo) 2010-05-20.
Krystof Hoder 2010-05-20.
Revision History:
@ -301,13 +301,12 @@ namespace datalog {
}
pair_info & get_pair(app_pair key) const {
return *m_costs.find(key);
}
void remove_rule_from_pair(app_pair key, rule * r, unsigned original_len) {
pair_info * ptr = &get_pair(key);
if (ptr->remove_rule(r, original_len)) {
SASSERT(m_costs.contains(key));
SASSERT(m_costs.find(key));
pair_info * ptr = 0;
if (m_costs.find(key, ptr) && ptr &&
ptr->remove_rule(r, original_len)) {
SASSERT(ptr->m_rules.empty());
m_costs.remove(key);
dealloc(ptr);
@ -362,7 +361,12 @@ namespace datalog {
void join_pair(app_pair pair_key) {
app * t1 = pair_key.first;
app * t2 = pair_key.second;
pair_info & inf = get_pair(pair_key);
pair_info* infp = 0;
if (!m_costs.find(pair_key, infp) || !infp) {
UNREACHABLE();
return;
}
pair_info & inf = *infp;
SASSERT(!inf.m_rules.empty());
var_idx_set & output_vars = inf.m_all_nonlocal_vars;
expr_ref_vector args(m);