Rafael Sá Menezes

I'd say we can ignore the old-frontends here. Is there any problems in keeping them though? I am asking because it is way easier to remove than adding it back....

> LGTM! Can you just run on SV-COMP before merging? Running at: https://github.com/esbmc/esbmc/actions/runs/2280965649

> IMO the as-of-yet unhandled case that both operands' value-sets are non-empty, a kind of cartesian product would need to get analyzed. Yes, I am still not sure how to...

SV-Comp results: Master ``` Statistics: 15648 Files correct: 8155 correct true: 5078 correct false: 3077 incorrect: 62 incorrect true: 24 incorrect false: 38 unknown: 7431 Score: 11857 (max: 25567) ```...

@fbrausse I mostly agree with your comments, I have a few questions though. > give this API a version separate from ESBMC in order to communicate incompatible changes (semver or...

> This makefile aids a full solver build by building all dependencies as required. I like the idea, the issue is that we are porting esbmc to windows as well...

> INI-like files (sectioned list of var = value assignments with # comments extending to the end of the line) are pretty common. I agree with you, this is something...

Ow, didn't know that INI was a standard of sorts. It seems that even Boost has a parser for it: https://www.boost.org/doc/libs/1_64_0/boost/property_tree/ini_parser.hpp

> toml seems simple and expressive enough: https://toml.io/en/ toml seems quite good for our purposes.

Let's tag any issue/PR that needs to be fixed/merged with the [milestone](https://github.com/esbmc/esbmc/milestone/5)