<commit_before>import intrepyd as ip
from intrepyd.engine import EngineResult
import unittest

class TestBr(unittest.TestCase):

    def test_br_01(self):
        context = ip.Context()
        realtype = context.mk_real_type()
        limit = context.mk_number("50", realtype)
        one = context.mk_number("1", realtype)
        counter1 = context.mk_latch("counter1", realtype)
        plusone = context.mk_add(counter1, one)
        context.set_latch_init_next(counter1, one, plusone)
        counter2 = context.mk_latch("counter2", realtype)
        plusone = context.mk_add(counter2, one)
        context.set_latch_init_next(counter2, one, plusone)
        mul = context.mk_mul(counter1, counter2)
        context.mk_output(mul)
        target = context.mk_leq(limit, mul)
        br = context.mk_backward_reach()
        br.add_target(target)
        br.add_watch(counter1)
        br.add_watch(counter2)
        result = br.reach_targets()
        self.assertEquals(EngineResult.REACHABLE, result)
        trace = br.get_last_trace()
        traceDict = trace.get_as_net_dictionary()
        counter1lastValue = traceDict[counter1][-1]
        counter2lastValue = traceDict[counter2][-1]
        self.assertEquals(counter1lastValue, "8.0")
        self.assertEquals(counter2lastValue, "8.0")

if __name__ == '__main__':
    unittest.main()<commit_msg>Updated tests<commit_after>import intrepyd as ip
from intrepyd.engine import EngineResult
import unittest

class TestBr(unittest.TestCase):

    def test_br_01(self):
        context = ip.Context()
        realtype = context.mk_real_type()
        limit = context.mk_number("50", realtype)
        one = context.mk_number("1", realtype)
        counter1 = context.mk_latch("counter1", realtype)
        plusone = context.mk_add(counter1, one)
        context.set_latch_init_next(counter1, one, plusone)
        counter2 = context.mk_latch("counter2", realtype)
        plusone = context.mk_add(counter2, one)
        context.set_latch_init_next(counter2, one, plusone)
        mul = context.mk_mul(counter1, counter2)
        context.mk_output(mul)
        target = context.mk_leq(limit, mul)
        br = context.mk_backward_reach()
        br.add_target(target)
        br.add_watch(counter1)
        br.add_watch(counter2)
        result = br.reach_targets()
        self.assertEquals(EngineResult.REACHABLE, result)
        trace = br.get_last_trace()
        traceDict = trace.get_as_net_dictionary()
        counter1lastValue = traceDict[counter1][-1]
        counter2lastValue = traceDict[counter2][-1]
        self.assertEquals(counter1lastValue, "8.0")
        self.assertEquals(counter2lastValue, "8.0")

    def test_br_02(self):
        context = ip.Context()
        bt = context.mk_boolean_type()
        x = context.mk_input("x", bt)
        y = context.mk_input("y", bt)
        target1 = context.mk_and(x, y)
        target2 = context.mk_and(context.mk_not(x), y)
        br = context.mk_backward_reach()
        br.add_target(target1)
        br.add_target(target2)
        result = br.reach_targets()
        self.assertEquals(EngineResult.REACHABLE, result)
        self.assertEquals(1, len(list(br.get_last_reached_targets())))
        br.remove_last_reached_targets()
        result = br.reach_targets()
        self.assertEquals(EngineResult.REACHABLE, result)
        self.assertEquals(1, len(list(br.get_last_reached_targets())))
        br.remove_last_reached_targets()

if __name__ == '__main__':
    unittest.main()
{'fraction_non_alphanumeric': 0.10901826484018265, 'fraction_numerical': 0.018835616438356163, 'mean_word_length': 3.0102974828375286, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5727444', 'n_tokens_mistral': 1140, 'n_tokens_neox': 1117, 'n_words': 184}