Rafael Sá Menezes

> I'm not sure this is sound. You're using the unardorned symbol name as key into the map. The array symbol could be touched (e.g. by non-constant index), in which...

> @rafaelsamenezes: we could also move forward with this PR: #1398. > > @Anthonysdu started working on it, but there was not much progress for some reason. Hm, I think...

CMake is now configured to automatically build the non gpl CVC5. We still need to update the API though for the FP stuff though, could you take a look @fbrausse...

> I'm not sure how or whether to enable cvc5 on a macos build. They do have a macos binary on their releases: I recommend avoiding it.

> Implementing the builtin like this: [object-size.patch.txt](https://github.com/esbmc/esbmc/files/14221194/object-size.patch.txt), these still give incorrect-true. Neither the base-case nor the inductive-step generate any VCCs, though: > > ``` > Checking base case, k =...

> > Implementing the builtin like this: [object-size.patch.txt](https://github.com/esbmc/esbmc/files/14221194/object-size.patch.txt), these still give incorrect-true. Neither the base-case nor the inductive-step generate any VCCs, though: > > ``` > > Checking base case,...

> QUERY is an infix formula (! or - for negation, & or space for conjunction, | for disjunction) I would prefer for only one prefix operator per operation. Is...

> I'm currently trying to figure out which kind of queries the CMake build would need to construct and for that I thought it best to have full flexibility with...

Alright, after a bit of investigation I think I root caused it. And... it is a limitation of the method itself in combination of how ESBMC deals with postincrement operation....

> @rafaelsamenezes: Can I ask you whether you had a chance to check this issue? Not yet, I will try to minimize it first.