unreachable executed: unknown binary operation fp.leq

[P. Berger]

I tested DIVINE on an example program and it fails with the error message: "unreachable executed: unknown binary operation fp.leq".

The program is:

extern void VERIFIER_assume(int);
extern float VERIFIER_nondet_float();

float a;
float VERIFIER_nondet_float();
int main() {

a = VERIFIER_nondet_float();
VERIFIER_assume(a <= 0);

}

The version of DIVINE is DIVINE 4, version 4.4.0+32c9761c4eb1, and my commandline was "./divine check --symbolic --svcomp example.c".

Is this expected behavior?

[Henrich Lauko]

Hi,

The current DIVINE does not provide symbolic verification with floating-point values. If you want to use it, you can try experimental implementation from SV-COMP 2020: ​https://divine.fi.muni.cz/2020/sv-comp/

Floating-point support should be merged into the current in the following weeks.

[P. Berger]

The version I used is exactly the version of SV-COMP 2020 ($ sha1sum divine-binary.zip
4a873bf8b46e2d6ab774e7a6809344c4d6cc77ff divine-binary.zip).

[Henrich Lauko]

You have to run DIVINE with '--solver z3', because DIVINE's default smt solver (STP) does not support floating points.