MathSAT5 with FP does not parse PI again

[kfriedberger]

The last column of our Buildbot table contains several exceptions from MathSAT5, where PI is already declared (standard symbol in FP theory?) and parsed again from SMTLIB.
If this is a bug in the parser, we need to report to Alberto.

TODO:
Get a minimal working example in JavaSMT (or even directly in C).

[baierd]

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 of "pi" is Real and not FP (I tested).

I don't think that we can do much here besides not using the name.

[kfriedberger]

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 symbols make such problems as well or how they are handled?
I assume that special tokens like true,false,select,store are not exported by MathSAT5.
If that is correct, I will ask Alberto for also exluding pi.

[baierd]

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 (So same issue as with pi).
I assume all functions/constants (numerals) that are predefined are like this.

[kfriedberger]

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.

[baierd]

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 you meant.

[kfriedberger]

Yes, then it looks like a missing case in the parser of MathSAT5.
Can you provide SMTLIB input for a crashing example with pi?

[baierd]

(define-fun pi () Int) parsed is enough for a crash.

[kfriedberger]

oh, I did not think of that simple query. thanks.

[kfriedberger]

Actually, the behaviour of MathSAT is correct: the symbol is defined and never actively printed.
The reported issue is already discussed in CPAchecker, where symbols are not properly escaped.

This issue can not be fixed in JavaSMT or the underlying solver.