@NotNull
  private List<PreContract> visitStatements(List<ValueConstraint[]> states, List<LighterASTNode> statements) {
    CodeBlockContracts result = new CodeBlockContracts();
    for (LighterASTNode statement : statements) {
      IElementType type = statement.getTokenType();
      if (type == BLOCK_STATEMENT) {
        result.addAll(visitStatements(states, getStatements(getCodeBlock(statement), myTree)));
      }
      else if (type == IF_STATEMENT) {
        List<PreContract> conditionResults = visitExpression(states, findExpressionChild(myTree, statement));

        List<LighterASTNode> thenElse = getStatements(statement, myTree);
        if (thenElse.size() > 0) {
          result.addAll(visitStatements(antecedentsReturning(conditionResults, returnTrue()), singletonList(thenElse.get(0))));
        }

        List<ValueConstraint[]> falseStates = antecedentsReturning(conditionResults, returnFalse());
        if (thenElse.size() > 1) {
          result.addAll(visitStatements(falseStates, singletonList(thenElse.get(1))));
        } else {
          states = falseStates;
          continue;
        }
      }
      else if (type == WHILE_STATEMENT) {
        states = antecedentsReturning(visitExpression(states, findExpressionChild(myTree, statement)), returnFalse());
        continue;
      }
      else if (type == THROW_STATEMENT) {
        result.addAll(asPreContracts(toContracts(states, fail())));
      }
      else if (type == RETURN_STATEMENT) {
        result.addAll(visitExpression(states, findExpressionChild(myTree, statement)));
      }
      else if (type == ASSERT_STATEMENT) {
        List<PreContract> conditionResults = visitExpression(states, findExpressionChild(myTree, statement));
        result.addAll(asPreContracts(toContracts(antecedentsReturning(conditionResults, returnFalse()), fail())));
      }
      else if (type == DECLARATION_STATEMENT) {
        result.registerDeclaration(statement, myTree, myBody.getStartOffset());
        continue;
      }
      else if (type == DO_WHILE_STATEMENT) {
        result.addAll(visitStatements(states, getStatements(statement, myTree)));
      }

      break; // visit only the first statement unless it's 'if' whose 'then' always returns and the next statement is effectively 'else'
    }
    return result.accumulated;
  }
@NotNull
  private List<PreContract> visitStatements(List<ValueConstraint[]> states, List<LighterASTNode> statements)