Re: [isabelle] Linear Arithmetic Split Limit Exceeded
On Thu, 2013-02-07 at 14:31 +0100, Makarius wrote:
> Someone else who understands the "lin_arith" solver needs to explain how
> to switch it off, or how to do these proofs about "mod" in a better way.
The limit exists because repeated splitting leads to an exponential
blow-up of the goal. It can be set, e.g., via
For this particular proof, n=12 gets rid of the warnings, and also of a
few more subgoals.
This archive was generated by a fusion of
Pipermail (Mailman edition) and