Baier D.
Baier D.
Thank you for the information. Unfortunately this does not seem useful for us.
So it seems that the problem is the try to get the interpolants back. If you try the following SMTLIB2 example taken from the CPAchecker-Mathsat-Query and parse it in the...
I made a C program illustrating the same example, but either i made a mistake or (more likely) the error is catched by the assertion that fails when you run...
Status: Reported to Alberto
Alberto answered that this is most likely a result of mixing theories (Bv/Array) and we have to live with it. Note: We are checking for the return values in the...
This is of course for the interpolation issue and not the SigSev. The interpolation issue just emerged when trying to find the SigSev. The problem is more that the next...
I'm going to take a look at it. A naive test for feasibility shouldn't be too hard.
Bitwuzla currently has no API to traverse formulas or parse formulas without solving them right away. Also it does not mention any form of reentrant mode/compiliation process currently. Since those...
The Devs answered and term traversal is possible, the API was just not publicly stated in the API website, but its useable and fits our purposes. Also, Bitwuzla is already...
The license under which Bitwuzla is published is the MIT license.