Commit 72a097de authored by Marek Chalupa's avatar Marek Chalupa
Browse files

bself: try using also constant cmp as assumptions 

If found that it holds in more consecutive states.
parent 2b01c229

slowbeast/bse/bself.py

+4 −0
Original line number Diff line number Diff line
@@ -128,6 +128,7 @@ def _overapprox_with_assumptions(E, L, S, executor, s, target): 
    yielded = False

    prestates = executor._extend_one_step(L, S)

    if prestates:

        Rc = set(get_const_cmp_relations(S.get_se_state()))

        for p in prestates:

            # check whether the relation from R0 holds in 'p'

            # R1 = set(get_var_relations([p], prevsafe=S))
@@ -135,6 +136,9 @@ def _overapprox_with_assumptions(E, L, S, executor, s, target): 
            rels =  [r0 for r0 in R0 if not intersection(P, r0).is_empty()]

            yielded |= bool(rels)

            yield from _yield_overapprox_with_assumption(E, L, S, executor, rels, s, target)

            # try constant relations too - if they hold in more steps, they may be invariant

            rels =  [rc for rc in Rc if not intersection(P, rc).is_empty()]

            yield from _yield_overapprox_with_assumption(E, L, S, executor, rels, s, target)



    if not yielded:

        yield from _yield_overapprox_with_assumption(E, L, S, executor, R0, s, target)