Efficiency regression on verifying non-linear arithmetic properties between 4.11.2 and 4.12.2

[rahxephon89]

Hi, we are observing a regression on verifying programs using non-linear arithmetic operations such as division and multiplication when switching from 4.11.2 to 4.12.2. I am wondering if there are some changes on options that may cause this? Thanks.

[NikolajBjorner]

try setting smt.arith.solver=2

[rahxephon89]

Thanks Nikola. Setting smt.arith.solver to 2 reduces the time but the verification fails. Is there anything else I can try?

[NikolajBjorner]

1. some improvements will go into the non-linear in the coming months so it could change the situation.
2. arith.solver=2 is incomplete so will often produce unknown for non-linear reals (and of course integers).

[rahxephon89]

Thanks Nikola!