Bug: Ultimate Automizer missing an assertion violation when casting to pointer

[salvadorer]

Hi,
I'm working with Ultimate Automizer (Version 0e0057c) and noticed that the assertion violation in the following code is missed:

extern unsigned long __VERIFIER_nondet_ulong(void);
extern void __VERIFIER_error(void);

void __ULTIMATE_assert(int cond) {
  if (!(cond)) {
  ERROR:
    __VERIFIER_error();
  }
}

int main(){
  const char* str_ptr = "";
  const char* inv_ptr = (char *) __VERIFIER_nondet_ulong();
  __ULTIMATE_assert(inv_ptr != str_ptr);
}

I invoked Ultimate with ~/UAutomizer-linux/Ultimate.py --architecture 64bit --spec unreach-call.prp --file test0.c
Ultimate outputs:

Execution finished normally
Writing output log to file Ultimate.log
Result:
TRUE

Notice that the same happens if you replace the call to __VERIFIER_nondet_ulong by a concrete address e.g. 0x55a8a2e6b007.

[salvadorer]

By the way, I just noticed that Taipan and Kojak share this seemingly buggy behavior.

[Heizmann]

Thanks for your bug report.
The standard says that the behavior for casts from integers to pointers is implementation-defined. We assume a certain implementation. However, we also think that this is a conceptual problem of our tools and we would like to change that. We are still discussing solutions.

Do you need a fix soon?