Baier D.
Baier D.
Only parsing (Its in the SMT-LIB2 Standard as :global-declarations ) No not yet. We asked ~1 year ago for this as we need it for other methods as well but...
I've asked if there are any updates on the methods we asked for.
We won't be getting the API features we want because, quote Mathias Preiner: "Boolector is in maintenance mode and won't be extended for new features. We are currently working on...
The API of Bitwuzla is pretty much feature complete and stable. There is however no API documentation at the moment.
Update 3.2.2 added new methods, one of which, get_value() allows us to create a value copy for a model. Boolector still does not provide methods to traverse asserted formulas. Hence...
I've added some tests in `ModelTest` to check for problems in the Boolector model (and others). Boolector tends to have some unwanted behavior when dumping formulas. Using the `boolector_dump_smt2()` method,...
There seems to be a problem when using Boolector in the CPAchecker currently. Now that there is a Model, the CPAchecker wants to access the model in one thread and...
I have just tested it on a new Windows environment and it works without any issues.
We have to provide the GMP library additionally, but yes that should simplify it immensely. I will check the script against the provided dll and report back.
GMP is statically linked in the provided Yices2 Windows binary, so that solves that. But we would still need it when compiling the wrapper, as it is a needed dependency...