How to use the mythril.laser.smt.And function in mythril

def test_concat_extract_assignment():
    inp1 = symbol_factory.BitVecSym("input1", 256)
    inp2 = symbol_factory.BitVecSym("input2", 256)
    output1 = symbol_factory.BitVecFuncSym(
        "Keccak[input]", size=256, func_name="keccak256", input_=Concat(inp1, inp2)
    )
    output = Concat(output1, symbol_factory.BitVecVal(0, 256))
    cond = And(output1 == inp2, inp1 == inp2)
    Extract(511, 256, output).potential_input_cond = cond

    assert Extract(511, 256, output).potential_input_cond == cond

def test_keccak_complex_eq():
    """
    check for keccak(keccak(b)*2) == keccak(keccak(a)*2) && a != b
    :return:
    """
    s = Solver()
    a = symbol_factory.BitVecSym("a", 160)
    b = symbol_factory.BitVecSym("b", 160)
    o1, c1 = keccak_function_manager.create_keccak(a)
    o2, c2 = keccak_function_manager.create_keccak(b)
    s.add(And(c1, c2))
    two = symbol_factory.BitVecVal(2, 256)
    o1 = two * o1
    o2 = two * o2
    o1, c1 = keccak_function_manager.create_keccak(o1)
    o2, c2 = keccak_function_manager.create_keccak(o2)

    s.add(And(c1, c2))
    s.add(o1 == o2)
    s.add(a != b)

    assert s.check() == z3.unsat

def test_keccak_symbol_and_val():
    """
    check keccak(100) == keccak(n) && n == 10
    :return:
    """
    s = Solver()
    hundred = symbol_factory.BitVecVal(100, 256)
    n = symbol_factory.BitVecSym("n", 256)
    o1, c1 = keccak_function_manager.create_keccak(hundred)
    o2, c2 = keccak_function_manager.create_keccak(n)
    s.add(And(c1, c2))
    s.add(o1 == o2)
    s.add(n == symbol_factory.BitVecVal(10, 256))
    assert s.check() == z3.unsat

def test_concat_extract_assignment_nested():
    inp1 = symbol_factory.BitVecSym("input1", 256)
    o1 = symbol_factory.BitVecFuncSym(
        "Keccak[inp1]",
        size=256,
        func_name="keccak256",
        input_=Concat(inp1, symbol_factory.BitVecVal(0, 256)),
    )
    output1 = symbol_factory.BitVecFuncSym(
        "Keccak[Concat(o1, 0)]",
        size=256,
        func_name="keccak256",
        input_=Concat(o1, symbol_factory.BitVecVal(0, 256)),
    )
    cond = And(output1 == o1, inp1 == inp1)
    Extract(511, 256, Extract(511, 256, output1.input_).input_).potential_input_cond = cond

    assert Extract(
        511, 256, Extract(511, 256, output1.input_).input_
    ).potential_input_cond == cond

symbol_factory.Bool(True),
            symbol_factory.Bool(True),
        )
        same_constraints = Constraints()
        for key in dict1:
            if key not in dict2:
                c1 = And(c1, key)
                if Not(key) not in dict2:
                    new_constraint1 = And(new_constraint1, key)
            else:
                same_constraints.append(key)
        for key in dict2:
            if key not in dict1:
                c2 = And(c2, key)
                if Not(key) not in dict1:
                    new_constraint2 = And(new_constraint2, key)
            else:
                same_constraints.append(key)
        merge_constraints = same_constraints + [Or(new_constraint1, new_constraint2)]
        return merge_constraints, c1, c2

c1, c2 = symbol_factory.Bool(True), symbol_factory.Bool(True)
        new_constraint1, new_constraint2 = (
            symbol_factory.Bool(True),
            symbol_factory.Bool(True),
        )
        same_constraints = Constraints()
        for key in dict1:
            if key not in dict2:
                c1 = And(c1, key)
                if Not(key) not in dict2:
                    new_constraint1 = And(new_constraint1, key)
            else:
                same_constraints.append(key)
        for key in dict2:
            if key not in dict1:
                c2 = And(c2, key)
                if Not(key) not in dict1:
                    new_constraint2 = And(new_constraint2, key)
            else:
                same_constraints.append(key)
        merge_constraints = same_constraints + [Or(new_constraint1, new_constraint2)]
        return merge_constraints, c1, c2

Extract(511, 256, key.input_).potential_input == pseudo_input,
                    )
                    Extract(511, 256, key.input_).potential_input_cond = calldata_cond
                    if not is_true(simplify(Extract(511, 256, key.input_).potential_input_cond != calldata_cond)):
                        print(key.input_, Extract(511, 256, key.input_).concat_args)
                    assert Extract(511, 256, key.input_).potential_input_cond == calldata_cond
                    print(Extract(511, 256, key.input_), calldata_cond, "CONDED")
        for actor in ACTOR_ADDRESSES:
            try:
                models_tuple.append(
                    (
                        get_model(
                            constraints=global_state.mstate.constraints
                            + [sender == actor, calldata_cond]
                        ),
                        And(calldata_cond, sender == actor),
                    )
                )
                sat = True
            except UnsatError:
                models_tuple.append((None, And(calldata_cond, sender == actor)))

        if not sat:
            return [False]

        for account in global_state.world_state.accounts.values():
            account.storage.concretize(models_tuple)

constraints1: Constraints, constraints2: Constraints
    ) -> Tuple[Constraints, Bool, Bool]:
        dict1, dict2 = {}, {}
        for constraint in constraints1:
            dict1[constraint] = True
        for constraint in constraints2:
            dict2[constraint] = True
        c1, c2 = symbol_factory.Bool(True), symbol_factory.Bool(True)
        new_constraint1, new_constraint2 = (
            symbol_factory.Bool(True),
            symbol_factory.Bool(True),
        )
        same_constraints = Constraints()
        for key in dict1:
            if key not in dict2:
                c1 = And(c1, key)
                if Not(key) not in dict2:
                    new_constraint1 = And(new_constraint1, key)
            else:
                same_constraints.append(key)
        for key in dict2:
            if key not in dict1:
                c2 = And(c2, key)
                if Not(key) not in dict1:
                    new_constraint2 = And(new_constraint2, key)
            else:
                same_constraints.append(key)
        merge_constraints = same_constraints + [Or(new_constraint1, new_constraint2)]
        return merge_constraints, c1, c2