Mikhail R. Gadelha

> @mikhailramalho: can I ask you whether you could run this PR over the SV-COMP benchmarks? I did and the results were worse somehow. This PR only changes so that...

Weird that the base case didn't catch it before the inductive step ran On Sat, 18 Nov 2023, 10:40 Franz Brauße, ***@***.***> wrote: > Another version of this reduction: >...

Please, try this patch: ``` diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index f40d7cbb7..6d05f172b 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -235,6 +237,11 @@ void goto_symext::symex_step(reachability_treet &art) thrown_obj_map.erase(cur_state->source.pc); } + if(instruction.inductive_step_instruction && is_floatbv_type(deref_code.target)) {...

:/ Do you have the previous result?

Hi, ``` $ clang-format -version clang-format version 3.9.1 (tags/RELEASE_391/final) ``` ``` $ python3 --version Python 3.5.3 ``` Processor: Intel® Xeon(R) CPU W3520 @ 2.67GHz × 8 Memory: 23.5 GiB Fedora...

Bear in mind that esbmc has some different names for stuff (e.g, location instead of source_location), so you'll probably need to take a look around to see what's used in...

hey, so cbmc also verifies cpp files, so just create a foo.cpp file and paste your code there. To print the symbol table, run cbmc with --show-symbol-table. I also use...

Reduced test case: ``` _Bool a = 1; _Bool b = 0; int main() { goto c; d: __ESBMC_assert(b, ""); c: b = a; a = 0; goto d; }...

it looks like esbmc finds the loop tho: ``` $ esbmc main.c --show-loops ESBMC version 7.5.0 64-bit x86_64 linux Target: 64-bit little-endian x86_64-unknown-linux with esbmclibc Parsing main.c Converting Generating GOTO...

What if we unset the standard internally and let clang set it? I think it's c++14. I would just advise that before we advertise it, we should support lambdas (and...