fp.rem not working with mathsat

[Tony Sloane]

I'm using aterm1 % aterm2 to produce a term using fp.rem:

(= %10@1 (fp.rem (_ +zero 11 53) %1@1))

but Mathsat (5.5.2 and 5.5.1 at least) gives an error:

Message is :ErrorResponse(StringLiteral(unknown symbol: fp.rem (line: 46)))

[Franck Cassez]

Yes it is not supported by MathSat 5.5.1/5.5.2 see this paper

[Franck Cassez]

@inkytonik Closing this issue. Solution was to use parallel solvers.