Internal bug when analyzing some (simple) code?

[mcarro]

I have the following C code (in a file called sqroot-main.c):

`//----------------------------------------- void main(){

unsigned int x,y,n;

n = VERIFIER_nondet_uint(); VERIFIER_assume(n > 0);

x = n; y = 1;

while (x > y) { x = (x + y) / 2; y = n / x; } __VERIFIER_assert((x x) <= n); __VERIFIER_assert(n < ((x+1)(x+1))); } //-------------------------------------------------`

and duet seems to raise an internal error with several analyses:

`mcarro@mcarro-ThinkPad-X1-Carbon-Gen-10$ ~/src/duet/duet.exe -cra sqroot-main.c Fatal error: exception File "srk/src/wedge.ml", line 2136, characters 16-22: Assertion failed

mcarro@mcarro-ThinkPad-X1-Carbon-Gen-10$ ~/src/duet/duet.exe -termination sqroot-main.c Fatal error: exception File "srk/src/quantifier.ml", line 1144, characters 22-28: Assertion failed`

The compiled duet code seems to pass all tests ('make test' finished successfully).

Perhaps I am doing something wrong, but it seems like this is some kind of internal bug otherwise?

Thanks in advance!

[zkincaid]

Thanks for the report, and sorry for the delay. The bug should be fixed now (although we can't prove anything interesting about this particular program). For programs with non-linear arithmetic, I'd suggest trying "duet.exe -cra -lirr " to use the invariant generator described in our latest paper.