Opened 4 years ago

Last modified 4 years ago

#107 assigned defect

unreachable executed: unknown binary operation fp.leq

Reported by: P. Berger Owned by: Henrich Lauko
Priority: minor Milestone: 4.4
Component: DiOS Keywords:


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

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?

Change History (3)

comment:1 Changed 4 years ago by Henrich Lauko

Component: otherDiOS
Owner: changed from mornfall to Henrich Lauko
Status: newassigned


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:

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

Last edited 4 years ago by Henrich Lauko (previous) (diff)

comment:2 Changed 4 years ago by P. Berger

The version I used is exactly the version of SV-COMP 2020 ($ sha1sum

comment:3 Changed 4 years ago by Henrich Lauko

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

Note: See TracTickets for help on using tickets.