/* * Program from Example 6 of * 2014WST - Leike, Heizmann - Geometric Series as Nontermination Arguments for Linear Lasso Programs * * Date: 2014-06-29 * Author: Jan Leike */ extern int __VERIFIER_nondet_int(void); int main() { int a = __VERIFIER_nondet_int(); int b = __VERIFIER_nondet_int(); while (a >= 1 && b >= 1) { a = 2*a; b = 3*b; } return 0; }