CBMC never finishes verification when using --floatbv and --smt2

[mikhailramalho]

Hi all,

I'm trying to dump the SMT formula of programs with floating-points and I get the following output:

$ time cbmc round_nondet_true-unreach-call.c --floatbv --smt2
CBMC version 5.8 64-bit x86_64 linux
Parsing round_nondet_true-unreach-call.c
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Converting
Type-checking round_nondet_true-unreach-call
Generating GOTO Program
Adding CPROVER library (x86_64)
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
aborting path on assume(false) at file round_nondet_true-unreach-call.c line 6 function __VERIFIER_assert thread 0
aborting path on assume(false) at file round_nondet_true-unreach-call.c line 6 function __VERIFIER_assert thread 0
aborting path on assume(false) at file round_nondet_true-unreach-call.c line 6 function __VERIFIER_assert thread 0
size of program expression: 578 steps
simple slicing removed 7 assignments
Generated 3 VCC(s), 3 remaining after simplification
Generated 3 VCC(s), 3 remaining after simplification
Passing problem to SMT2 QF_AUFBV using Z3
converting SSA

It's running for a couple of days now.

No crash or high memory usage (~50MB).

It happens in the programs floats-esbmc-regression/nondet.c from SV-COMP.

[tautschnig]

Most likely the same issue as #344. Some bug appears to create a loop in the data structures.

[martin-cs]

It's not a loop in the data structure; it is structural sharing which happens a lot in the floating-point encodings. @mikhailramalho see #344 for the current (and, really correct) work-around. If you just want an SMT formula, use --fpa.

[tautschnig]

@martin-cs Are your sure about the assertion about sharing? I've been running the simple example from #344 now for >570 hours.

[mikhailramalho]

Hi, thank you for the replies. Indeed, it looks like a duplicate of #344.

I tried to debug the formula generation and trying to print result in float_bvt::sticky_right_shift doesn't work after a few iterations (maybe in the last one?).

I hope it helps.

[mikhailramalho]

By 'doesn't work', I mean it hangs in the print call.