Marco Gario

A test for this was added in a dedicated branch: fnode-non-recursive-pickling https://github.com/pysmt/pysmt/commit/af2bdec37e3a90ff72592298f5e6b085b009b072

This is mostly motivated from trying to normalize expressions. In LRA we cannot have general division or multiplication, except for the cases where we have constant coefficients. For those cases,...

See https://github.com/pysmt/pysmt/pull/636 for a patch in the direction described.

> Then the min logic is computed by applying min on the list. > However both QF_NIRA < QF_UFLIRA and QF_UFLIRA < QF_NIRA are false. Yes, and this is correct...

Those changes were introduced in https://github.com/pysmt/pysmt/pull/714. I would need to dig a bit deeper to understand how to proceed. @mikand any insight?

The general rule of thumb for this was that if an operation is commutative, then its semantics are unambiguous when extended from binary to n-ary. In all other cases, you...

The tests fail. The one for CVC4 should be fixed once #529 is merged (seems to be related to an old SWIG version), but MathSAT seems unable to solve the...

The name of the test is very bad. There should be one test for a simple non linear expression and one for an irrational result. In the second case, I...

The question is why is the test failing. If the logic includes division, then that is a valid example for the logic. Clearly we do not expect this to work...

See FNode.bv_str, for various formatting options. I thought that the default for the printers was decimal + width (e.g. 7_32), since that is much more understandable. I agree that this...