Karlheinz Friedberger
Karlheinz Friedberger
The same problem appears with our configurations of Ant/Ivy. We need to provide example projects and let them build.
As we never communicate towards the user, that formulae are structured as how they are build, I do not see a problem with merging this PR. There are more solvers...
Then we need to either exclude this symol from being defined in the SMTLIB header or ask MathSAT to not export this symbol. Could you take a look, if other...
Where does this need to be fixed? If MathSAT dumps `pi` in SMTLIB, that might be the bug. Does MathSAT dump other functions (except pi) in SMTLIB? I think not.
Yes, then it looks like a missing case in the parser of MathSAT5. Can you provide SMTLIB input for a crashing example with `pi`?
oh, I did not think of that simple query. thanks.
Actually, the behaviour of MathSAT is correct: the symbol is defined and never actively printed. The reported issue is already discussed [in CPAchecker](https://gitlab.com/sosy-lab/software/cpachecker/-/issues/239), where symbols are not properly escaped. This...
Further investigation required: Why does MathSAT fail for the commandline in the Buildbot table mentioned above? There is no `pi` in the parser query, but only `true`. CPAchecker uses only...
Yes, still relevant, but minor priority. because there is a bug, it is just hidden.
Is FP_AS_IEEEBV deifned in the SMTLIB standard or is it optional? Can you provide a minimal SMTLIB query for using this? Does the latest nightly build (from website) of MathSAT5...