Commit fd07e4ca authored by Marek Chalupa's avatar Marek Chalupa
Browse files

rels: do not yield unsat parts of disjunctions

parent a0c27592

slowbeast/kindse/relations.py

+2 −1
Original line number Diff line number Diff line
@@ -257,6 +257,7 @@ def get_const_subs_relations(state): 
                        continue

                if nexpr.isOr():

                    for c in nexpr.children():

                        if state.is_sat(c): # only a part of the disjunction may be unsat in the state

                            yield AssertAnnotation(c, subs, EM)

                else:

                    yield AssertAnnotation(nexpr, subs, EM)