Mikhail R. Gadelha

@kaled-alshmrany, you'll need to add --no-assertions to esbmc, when calling it from fusesbmc.

@kaled-alshmrany @rafaelsamenezes, did you test this patch in fuesbmc?

I don't see why it shouldn't be merged tbh. Em seg., 15 de nov. de 2021 às 11:09, Lucas Cordeiro < ***@***.***> escreveu: > @mikhailramalho and @kaled-alshmrany > : Is...

The latter is an easy fix: there is an extra space in `options.cpp` when defining the flag: ``` {"smt-formula-too ", //

When I created this issue I had the following transformation in mind (several sv-comp benchmarks used to initialize arrays): ``` int foo[bar]; for(int i = 0; i < bar; ++i)...

Two problems here: 1. First there are still a bunch of checks that esbmc does that are just not necessary, since clang already does it for us. If the frontend...

Indeed it looks wrong. It was definitely preprocessed by cseq (not sure which variant). @trucnguyenlam care to join the thread? Do you guys have the original source?

Hi all, Thank you for opening the issue. I should've send the counterexamples for all tasks in my previous emails, sorry about that. The lines are: * loop-industry-pattern/ofuf_1_true-unreach-call.c Violated property:...

Hi, I just created a folder in Dropbox with all the counterexamples generated by our tool. https://www.dropbox.com/sh/q202xpwogyxafeb/AABqeLwXzE1xUrEtbxtq1H8sa?dl=0 It contains only the first and last 32kb of everything esbmc prints, but...

Any progress on this? We just found some property violation in the following benchmarks: ``` ntdrivers/diskperf_true-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref) ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref) ntdrivers/parport_true-unreach-call_true-valid-memsafety.i.cil.c false(valid-deref) ```