OpenSMT 2

Code example: hi-bench/main-bench/funfrog_regression/03_simple/main7.c --show-error-trace --unwind 10

Error:
Checking claims in program...
; Warning: disabling SATElite preprocessing to track proof
; Warning: disabling SATElite preprocessing to track proof
Checking Claim #1 (100%) ...
Last assertion location: 30 / 36 ( 3)

• INLINING function: c::__CPROVER_initialize
• INLINING function: c::main
  Processing a deferred function: c::__CPROVER_initialize
  Processing a deferred function: c::main
• INLINING function: c::strncpy
  Processing a deferred function: c::strncpy
  Unwinding loop c::strncpy.0 iteration 1 file main7.c line 7 function strncpy thread 0
  Unwinding loop c::strncpy.0 iteration 2 file main7.c line 7 function strncpy thread 0
  Unwinding loop c::strncpy.0 iteration 3 file main7.c line 7 function strncpy thread 0
  Unwinding loop c::strncpy.0 iteration 4 file main7.c line 7 function strncpy thread 0
  Unwinding loop c::strncpy.0 iteration 5 file main7.c line 7 function strncpy thread 0
  Unwinding loop c::strncpy.0 iteration 6 file main7.c line 7 function strncpy thread 0
  Unwinding loop c::strncpy.0 iteration 7 file main7.c line 7 function strncpy thread 0
  Unwinding loop c::strncpy.0 iteration 8 file main7.c line 7 function strncpy thread 0
  Unwinding loop c::strncpy.0 iteration 9 file main7.c line 7 function strncpy thread 0
  Unwinding loop c::strncpy.0 iteration 10 file main7.c line 7 function strncpy thread 0
  SYMEX TIME: 0.028
  All SSA steps: 245
  Ignored SSA steps after slice: 164
  SLICER TIME: 0.001
  evolcheck: LRALogic.C:614: void LRALogic::splitTermToVarAndConst(const PTRef&, PTRef&, PTRef&): Assertion `isRealTimes(term) || isRealDiv(term) || isRealVar(term) || isConstant(term)' failed.
  Aborted (core dumped)

This is the code:

• strncpy example */
  //#include <stdio.h>
  //#include <string.h>
  #define LEN 2

char *strncpy (char *dest, const char *src, int n) {
for (int i = 0; i < n; ++i) {
*dest = *src;
if (!*src)
return dest;
++dest;
++src;
}
return dest;
}

int main () {
char str1[]= "To be ";
char str2[LEN];
strncpy (str2,str1,LEN-1);

assert('T' == str1[0]);

//puts (str2);
  return 0;
}

I don't think hifrog-lra can cop with it now, and so I expected to have an error from hifrog (or warning) not from opensmt2. Any idea what could be the reason?

Thanks,
Karine