Baier D.
Baier D.
@daniel-raffler found a minimal query triggering this problem. Thank you! ``` (set-option :produce-models true) (declare-fun a () (_ BitVec 32)) (declare-fun d () (Array (_ BitVec 32) Float64)) (declare-fun *d...
Thank you very much! A new MathSAT version has been published that addresses this. Related: #556
I'll start some tests. Note: i'll need to adapt CPAchecker to our new changes first ;D slight delay.
Thanks! That looks promising! I started additional CPAchecker runs for the current `master` for SV-COMP, SymEx, Predicate Abstraction and IMC.
Sorry for the late reply. We disable Z3s loading mechanism in JavaSMT, as it only loads `libz3java`, but not `libz3`. Hence when we try to load everything ourselves. Which Z3...
> This works flawlessly when using the Z3 java bindings from the Z3 repo. Please define what works and what does not work more precisely. Could you load JavaSMT with...
Note: Version 6 will be the last mayor release for Java 11. We will move to Java 17 soon after and aim to adopt Java 21 in 2026. Changelog (WIP):...
We simply disable support for theories/logics that are handled "better" in the up-to-date Z3 versions. The main purpose of the solver is interpolation support, so everything not included in that...
@kfriedberger the SMTLIB2 standard defines the size of an FP as mantissa + exponent with the mantissa including the sign bit. Our current implementation excludes it, and we do not...
Do we want to document the typical returns of solvers for special FP numbers? There are multiple well defined return values for NaN as bitvector for example.