Baier D.
Baier D.
Declaring "pi" as a variable always directly results in this exception. The variable "pi" is a pre-declared constant according to Alberto and we have to work around it. The type...
`true` and `false` is fine. `select`, `store` as well as `+`, `-`, `and`, `or`, `not` etc. are built-in functions and you get an exception when declaring something with those names...
Communication hickup on my side. Declaring functions with those names is not possible with `declare-fun`. (As it should be?) `define-fun` works with all of them except `pi`. Thats probably what...
`(define-fun pi () Int)` parsed is enough for a crash.
Is this issue still relevant? You mentioned yesterday that you fixed this in CPAchecker.
All the failed tasks fail in the same way when parsed by Mathsat itself: `(error "unknown symbol: FP_AS_IEEEBV (line: 449)") // With line: xyz being an example` FP_AS_IEEEBV is not...
FP_AS_IEEEBV is not defined in SMTLIB2 but i can find sources that say that Mathsat5 does offer the functionality (and it does so in the regular API) but i can...
Sure can do. I'll add you in CC.
Mathsat5 version 5.6.4 is released and Alberto added the function `fp.as_ieee_bv` for us right away. I tested the function in smtlib2 and it works as expected.