Yices error "non-linear arithmetic is not allowed in logic ALL"

[msaaltink]

I have Yices 2.6.2 installed, and a fairly recent bulld of saw (2e4fc060). Here's an unexpected error from them:

sawscript> prove z3 {{ \ (x:Integer) y -> ((x*y) == 0) == (x==0 \/ y == 0) }}
[14:29:06.691] Valid

sawscript> prove yices {{ \ (x:Integer) y -> ((x*y) == 0) == (x==0 \/ y == 0) }}

*** Data.SBV: Unexpected non-success response from Yices:
***
***    Sent      : (assert s9)
***    Expected  : success
***    Received  : (error "non-linear arithmetic is not allowed in logic ALL")
***
***    Exit code : ExitFailure (-15)
***    Executable: /usr/local/bin/yices-smt2
***    Options   : --incremental
***
***    Reason    : Check solver response for further information. If your code is correct,
***                please report this as an issue either with SBV or the solver itself!

[robdockins]

Yices, run in its standard mode, doesn't have any nonlinear arithmetic support. To enable it you have to use a special command-line flag, and then you have limited theory support. What4 will examine your problem before sending it to the solver to determine if this flag should be set, but SBV doesn't do this.

sawscript> prove (w4_unint_yices []) {{ \ (x:Integer) y -> ((x*y) == 0) == (x==0 \/ y == 0) }}
Calling Yices to check sat
Running check sat
[00:34:34.867] Valid