From 8f51d131fedcd80db21f204a0b2447e70b1e88ea Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Mon, 21 Sep 2015 16:12:03 -0400 Subject: [PATCH] Fix for sets segfault (reported by Ravi Kandhadai) fix involves sets getModelValue handling the case when element theory doesn't have model --- src/theory/sets/theory_sets_private.cpp | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 565a5cd69..4054f3e21 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -593,11 +593,16 @@ EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) { // The terms are implied to be dis-equal return EQUALITY_FALSE; } - if( d_external.d_valuation.getModelValue(a) == d_external.d_valuation.getModelValue(b) ) { - // Ther term are true in current model + Node aModelValue = d_external.d_valuation.getModelValue(a); + if(aModelValue.isNull()) { return EQUALITY_UNKNOWN; } + Node bModelValue = d_external.d_valuation.getModelValue(b); + if(bModelValue.isNull()) { return EQUALITY_UNKNOWN; } + if( aModelValue == bModelValue ) { + // The term are true in current model return EQUALITY_TRUE_IN_MODEL; + } else { + return EQUALITY_FALSE_IN_MODEL; } - return EQUALITY_FALSE_IN_MODEL; // } // //TODO: can we be more precise sometimes? // return EQUALITY_UNKNOWN; @@ -1561,7 +1566,9 @@ Node TheorySetsPrivate::TermInfoManager::getModelValue(TNode n) if(e.isConst()) { elements_const.insert(e); } else { - elements_const.insert(d_theory.d_external.d_valuation.getModelValue(e)); + Node eModelValue = d_theory.d_external.d_valuation.getModelValue(e); + if( eModelValue.isNull() ) return eModelValue; + elements_const.insert(eModelValue); } } Node v = d_theory.elementsToShape(elements_const, n.getType()); -- 2.30.2