sym_post_analysis.py

for state in states:
  # Let's filter all the states that are not return statements
  if state.currently_executing != 6:
    continue
  # We want the result to be 10, let's formulate that as a constraint
  result_constraint = (state.result == 10)
  
  # If it is possible to satisfy both the path constraints (these are the constraints collected on each branch)
  # and the result constraint then there must be an input that makes the function return 10
  if is_possible(result_constraint and state.constraints):
    # Using SMT solving we can get an input that will satisfy all the constraints and make the function return 10
    print(give_satisfying_input(result_constraints and state.constraints))