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 

  using [[linarith_split_limit=n]]

For this particular proof, n=12 gets rid of the warnings, and also of a
few more subgoals.

Best regards,
Tjark







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.