// This file is part of the SV-Benchmarks collection of verification tasks:
// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
//
// SPDX-FileCopyrightText: 2021 DynamiTe team <https://github.com/letonchanh/dynamite>
//
// SPDX-License-Identifier: Apache-2.0

/*
  A nonlinear termination benchmark program from the OOPSLA'20 paper 
  "DynamiTe: Dynamic termination and non-termination proofs"
  by Ton Chanh Le, Timos Antonopoulos, Parisa Fathololumi, Eric Koskinen, ThanhVu Nguyen.
  Adapted from the original nonlinear benchmark nla-digbench. 
*/

/* Compute the floor of the square root, by Dijkstra */
extern int __VERIFIER_nondet_int(void);

int main() {
    unsigned int n, p, q, r, h;

    n = __VERIFIER_nondet_int();

    p = 0;
    q = 1;
    r = n;
    h = 0;
    while (q <= n && q <= 1000000000) { // Ensure q does not exceed a large bound
        q = 4 * q;
    }
    while (r >= 2 * p + q) {
        q = q / 4;
        h = p + q;
        p = p / 2;
        if (r >= h) {
            p = p + q;
            r = r - h;
        }
    }
    return 0;
}