Jorge Navas
Jorge Navas
I think that the cex you are getting is when `n=0` and the loop body is never taken so the cex generation complains that the cex is too simple. Try...
I still get a cex.
If you just compile with -O0, clang will add the attribute `optnone` to all functions. The BMC engine relies on many LLVM optimizations (included loop unrolling). A function with attribute...
Have you tried to increase the unrolling depth (i.e. `--bound N`) ?
No, it's `--bound N`
As a general comment I'm worried about this change. The whole point of using a radix tree here is to be able to make joins very cheaply because the cost...
`llvm-objdump -D O1_pass.o`: ``` Disassembly of section cf_ebpf_generic: 0000000000000000 : 0: b7 00 00 00 00 00 00 00 r0 = 0 1: 95 00 00 00 00 00 00...
Great, so then prevail behaves as expected. Regarding your question, verify with -O0 and deploy with -O1 or -O2 makes sense assuming we are happy trusting the compiler optimizations. But...