Timout on alive-tv

[Ralender]

define i16 @src(i16 %y, i16 %0) {
entry1:
  %1 = shl i16 %y, 1
  %2 = mul i16 %1, %0
  ret i16 %2
}
define i16 @tgt(i16 %y, i16 %0) {
entry:
  %1 = freeze i16 %0
  %2 = freeze i16 %y
  %3 = mul i16 %1, %2
  %4 = icmp eq i16 %2, %1
  %5 = zext i1 %4 to i16
  %6 = icmp ult i16 %5, %2
  %7 = zext i1 %6 to i16
  %8 = icmp sgt i16 %3, %7
  %9 = zext i1 %8 to i16
  %10 = select i1 %8, i16 2, i16 0
  %11 = or i16 %10, %9
  %12 = sub nsw i16 1, %10
  %13 = icmp ugt i16 %11, %12
  %14 = select i1 %13, i16 %1, i16 0
  %15 = sub i16 %3, %14
  %16 = shl i16 %15, 1
  ret i16 %16
}

alive-tv out.ll -smt-to=7200000

I have tried to increase the timeout up to 2h but this still timeout. is this normal or some kind of infinite loop ?

[regehr]

the potential presence of undef values makes Alive's queries dramatatically more difficult for Z3 to solve. if you disable them by marking your function arguments noundef or using the --disable-undef-input to alive-tv, that should help

[Ralender]

it still times out with --disable-undef-input

[regehr]

I recommend making the timeout longer and just waiting. there's not much we can do about this sort of thing from the Alive side, Z3 is where the time is going

[Ralender]

ok, it seemed a very very long time for a simple program to me but ok.