Treat nonlinear multiplication as only a warning when Z3 is used (closes #16).

In this case Z3 may return 'unknown' but I was not able to find any
simple examples that illustrated this. Currently such a response would
cause an exception in JKind. When we find an example, we can give it
better behavior.