def test_function_String_rstrip_symbolicStrip():
    b = ast_parse.parse(test3).body
    p = Path(b,source=test3)
    pg = PathGroup(p)

    pg.explore()
    assert len(pg.completed) == 5
    o = [p.state.any_str('x') for p in pg.completed]
    o.sort()
    # 3 cases. 1) both chars miss, 2) one char hit's "t" and the other misses. 3) one hits
    # "t" and the other hits "s"
    assert o == ['te', 'te', 'tes', 'tes', 'testt']

    b = ast_parse.parse(test4).body
    p = Path(b,source=test4)
    pg = PathGroup(p)

    pg.explore()
    assert len(pg.completed) == 9

    # TODO: This is a brittle match..
    o = [p.state.any_str('s') for p in pg.completed]
    # Sort by number of 'x' that appear in the output
    o = sorted(o, key=lambda x: x.count('x'))
    assert not o[0].endswith("x")
    for x in range(1,8):
        assert o[x].endswith("x"*x)

def test_pyObjectManager_List_varInList():
    b = ast_parse.parse(test3).body
    p = Path(b,source=test3)
    pg = PathGroup(p)
    
    pg.explore()
    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_list('l') == [1,2,3,4]

    b = ast_parse.parse(test4).body
    p = Path(b,source=test4)
    pg = PathGroup(p)

    pg.explore()
    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_list('l') == [1,2,[3,4]]


    # NOTE: This is correct behavior. Python resolves the object when creating the list
    # Updating the var later has no affect on the list
    b = ast_parse.parse(test5).body
    p = Path(b,source=test5)
    pg = PathGroup(p)

    pg.explore()
    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_list('l') == [1,2,[3,4]]

    b = ast_parse.parse(test6).body
    p = Path(b,source=test6)
    pg = PathGroup(p)

    pg.explore()
    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_list('l') == [1,2,4,4]

def test_pySym_AugAssign_SafeBitVec():
    # Ensuring that we notice over and underflows

    #######
    # Add #
    #######
    b = ast_parse.parse(test4).body
    p = Path(b,source=test4)
    pg = PathGroup(p)
    pg.explore()
    
    assert len(pg.completed) == 0
    assert len(pg.deadended) == 1

    #######
    # Mul #
    #######
    b = ast_parse.parse(test5).body
    p = Path(b,source=test5)
    pg = PathGroup(p)
    pg.explore()

    assert len(pg.completed) == 0
    assert len(pg.deadended) == 1

    #######
    # Sub #
    #######
    b = ast_parse.parse(test6).body
    p = Path(b,source=test6)
    pg = PathGroup(p)
    pg.explore()
    
    assert len(pg.completed) == 0
    assert len(pg.deadended) == 1

def test_function_range():
    b = ast_parse.parse(test1).body
    p = Path(b,source=test1)
    pg = PathGroup(p)

    pg.explore()

    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_int('out') == 150

    b = ast_parse.parse(test2).body
    p = Path(b,source=test2)
    pg = PathGroup(p)

    pg.explore()
    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_list('l') == [4, 5, 6, 7, 8, 9]

    b = ast_parse.parse(test3).body
    p = Path(b,source=test3)
    pg = PathGroup(p)

    pg.explore()
    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_list('l') == [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11]

def test_pySym_AugAssign_Subscript():
    b = ast_parse.parse(test9).body
    p = Path(b,source=test9)
    pg = PathGroup(p)
    pg.explore()

    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_list('l') == [1,7.7,3]

    b = ast_parse.parse(test10).body
    p = Path(b,source=test10)
    pg = PathGroup(p)
    pg.explore()

    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_list('l') == [1, 127, 3]

    b = ast_parse.parse(test11).body
    p = Path(b,source=test11)
    pg = PathGroup(p)
    pg.explore()

    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_list('l') == [1, 4, 3]

    b = ast_parse.parse(test12).body
    p = Path(b,source=test12)
    pg = PathGroup(p)
    pg.explore()

    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_list('l') == [1, 7, 3]

def test_pySym_nestedWhile():
    b = ast_parse.parse(test3).body
    p = Path(b,source=test3)
    pg = PathGroup(p)

    assert pg.explore(find=14)
    assert pg.found[0].state.any_int('z') == 45

    b = ast_parse.parse(test4).body
    p = Path(b,source=test4)
    pg = PathGroup(p)
    assert pg.explore(find=14)
    assert pg.found[0].state.any_int('z') == 45

def test_function_List_insert():
    b = ast_parse.parse(test1).body
    p = Path(b,source=test1)
    pg = PathGroup(p)

    pg.explore()

    # [5.15, 'c', 's\x00\x00\x00\x00\x00', 14, 'test', [1, 2, 4, 5], 1.234, 0, 1, 2, 3]
    assert len(pg.completed) == 1

    s = pg.completed[0].state.copy()

    l = s.getVar('l')
    
    assert type(l[0]) == Real
    assert type(l[1]) == String and len(l[1]) == 1
    assert type(l[2]) == String
    assert type(l[3]) == BitVec
    my_list = s.any_list(l)
    assert my_list[0] == 5.15
    assert my_list[1] == "c"
    assert my_list[2].startswith("s")
    assert my_list[3] == 14
    assert my_list[4] == "test"
    assert my_list[5] == [1,2,4,5]
    assert my_list[6] == 1.234
    assert my_list[7:] == [0,1,2,3]

def test_var_used_in_z3_ignore():
    b = ast_parse.parse(test10).body
    p = Path(b,source=test10)
    pg = PathGroup(p)
    
    pg.explore()

    assert len(pg.completed) == 1

    s = pg.completed[0].state.copy()
    i = s.getVar('i')
    z3_obj = i.getZ3Object()

    # Not in here to begin with
    #assert not z3Helpers.varIsUsedInSolver(z3_obj,s.solver)
    assert not s.var_in_solver(z3_obj)

    # Now it will be in there
    s.addConstraint(z3_obj > 3)
    #assert z3Helpers.varIsUsedInSolver(z3_obj,s.solver)
    assert s.var_in_solver(z3_obj)

    # Now try ignoring it
    s.remove_constraints(z3_obj > 3)
    s.addConstraint(z3_obj > 3)
    assert not s.var_in_solver(z3_obj, ignore=[z3_obj > 3])
    assert not s.var_in_solver(z3_obj, ignore=z3_obj > 3)

def test_pySym_complicated():
    b = ast_parse.parse(test5).body
    p = Path(b,source=test5)
    pg = PathGroup(p)
    
    assert pg.explore(find=19)
    assert pg.found[0].state.any_int('z') == 26

def test_pyState_AssignListFromSubscript():
    b = ast_parse.parse(test4).body
    p = Path(b,source=test4)
    pg = PathGroup(p)
    
    pg.explore()
    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_list('x') == [4,5]

    b = ast_parse.parse(test5).body
    p = Path(b,source=test5)
    pg = PathGroup(p)
    
    pg.explore()
    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_list('x') == [5,6,7]

def test_pyState_Subscript_negative_slices():
    b = ast_parse.parse(test14).body
    p = Path(b,source=test14)
    pg = PathGroup(p)
    
    pg.explore()

    assert len(pg.completed) == 1
    
    s = pg.completed[0].state.copy()

    a = s.getVar('a')
    b = s.getVar('b')
    x = s.getVar('x')
    y = s.getVar('y')

    assert a.mustBe("test"[-1:])
    assert b.mustBe("test"[-3:-1])
    
    assert len(x) == 1
    assert x[0].mustBe(4)

    assert len(y) == 2
    assert y[0].mustBe(2)
    assert y[1].mustBe(3)

def test_pySym_functionNestingTwo():
    # More intense nesting
    b = ast_parse.parse(test7).body
    p = Path(b,source=test7)
    pg = PathGroup(p)
    pg.explore()
    assert pg.completed[0].state.any_int('x') == 7

def test_function_pyState_BVS_ret_as_list():
    b = ast_parse.parse(test2).body
    p = Path(b,source=test2)
    pg = PathGroup(p)

    pg.explore()
    assert len(pg.completed) == 1

def test_simpleIf():
    b = ast_parse.parse(simpleIf).body
    p = Path(b,source=simpleIf)
    # Step through the "if" statement
    p = p.step()[0]
    p = p.step()[0]
    p2 = p.step()
    ifSide = p2[0]
    elseSide = p2[1]
    
    # ifSide's path should now be inside, meaning only the print statement
    assert len(ifSide.state.path) == 1
    # Else should be in the else statement
    assert len(elseSide.state.path) == 2
    
    # Neither have anything to do after the if statement
    assert len(ifSide.state.callStack) == 1
    assert len(elseSide.state.callStack) == 0
    
    # If side should not be possible
    assert not ifSide.state.isSat()
    assert elseSide.state.isSat()
    
    # Track expected number of assertions
    #assert len(ifSide.state.solver.assertions()) == 3
    #assert len(elseSide.state.solver.assertions()) == 3
    
    # Make sure the answer makes sense
    assert ifSide.state.any_int('x') == None
    assert elseSide.state.any_int('x') == 1

def test_pyObjectManager_List_BitVec():
    b = ast_parse.parse(test8).body
    p = Path(b,source=test8)
    pg = PathGroup(p)
    
    pg.explore()
    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_list('l') == [1,2,1337,4]

    b = ast_parse.parse(test9).body
    p = Path(b,source=test9)
    pg = PathGroup(p)
    
    pg.explore()
    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_list('l') == [1,[2,1337],4]

def test_pyObjectManager_List_setitem():
    b = ast_parse.parse(test1).body
    p = Path(b,source=test1)
    pg = PathGroup(p)

    pg.explore()
    assert len(pg.completed) == 1
    
    l = pg.completed[0].state.getVar('l')

    s = pg.completed[0].state

    # Base check
    assert l[1].count == 0
    assert type(l[1]) == Real

    # Assign an Int
    l[1] = Int(varName='x',ctx=0,state=s)
    assert l[1].count == 1
    assert type(l[1]) == Int

    # Assign back to Real
    l[1] = Real(varName='x',ctx=0,state=s)
    assert l[1].count == 2
    assert type(l[1]) == Real
    
    # Assign to BitVec
    l[1] = BitVec(varName='x',ctx=0,size=32,state=s)
    assert l[1].count == 3
    assert type(l[1]) == BitVec
    
    # Assign List
    l[1] = List(varName='x',ctx=0,state=s)
    #assert l[1].count == 4
    assert type(l[1]) == List

def test_pyObjectManager_Char_is_unconstrained():
    b = ast_parse.parse(test2).body
    p = Path(b,source=test2)
    pg = PathGroup(p)

    pg.explore()
    assert len(pg.completed) == 1

    s = pg.completed[0].state.copy()
    c = s.getVar('s')[0]

    assert c.is_unconstrained
    
    # For now, this will add bounded int constraints to the solver...
    z3_obj = c.getZ3Object()
    # Those bounds should not count as constrained
    assert c.is_unconstrained

    # This constraint should eval to True, and not be added
    s.addConstraint(z3_obj > 5)
    assert c.is_unconstrained

    # Try with symbolic
    c = s.getVar('c2')[0]
    
    assert c.is_unconstrained
    
    # For now, this will add bounded int constraints to the solver...
    z3_obj = c.getZ3Object()
    # Those bounds should not count as constrained
    assert c.is_unconstrained

    # This should add a real constraint
    s.addConstraint(z3_obj > 5)
    assert c.is_constrained

def test_pySym_BinOp_Xor():
    b = ast_parse.parse(test4).body
    p = Path(b,source=test4)
    pg = PathGroup(p)
    pg.explore()
    
    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_int('d') == 13

def test_function_int_statesplit():
    b = ast_parse.parse(test3).body
    p = Path(b,source=test3)
    pg = PathGroup(p)

    pg.explore()
    assert len(pg.completed) == 8
    assert set([p.state.any_int('x') for p in pg.completed]) == set(range(8))

def test_pySym_variableSlice():
    b = ast_parse.parse(test4).body
    p = Path(b,source=test4)
    pg = PathGroup(p)

    pg.explore()
    assert len(pg.completed) == 1
    assert pg.completed[0].state.any_int('out') == 104