*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Linear Arithmetic Split Limit Exceeded*From*: Tjark Weber <webertj at in.tum.de>*Date*: Thu, 07 Feb 2013 15:30:03 +0100*Cc*: Alfio Martini <alfio.martini at acm.org>*In-reply-to*: <alpine.LNX.2.00.1302071428330.28301@macbroy21.informatik.tu-muenchen.de>*References*: <CAAPnxw0uTzaLgEqj99ap8YNDyZiJxwWkgkEwK+81JsrTaUFxyA@mail.gmail.com> <alpine.LNX.2.00.1302071428330.28301@macbroy21.informatik.tu-muenchen.de>

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

**Follow-Ups**:**Re: [isabelle] Linear Arithmetic Split Limit Exceeded***From:*Alfio Martini

**References**:**[isabelle] Linear Arithmetic Split Limit Exceeded***From:*Alfio Martini

**Re: [isabelle] Linear Arithmetic Split Limit Exceeded***From:*Makarius

- Previous by Date: Re: [isabelle] Common options in ROOT
- Next by Date: Re: [isabelle] Isabelle2013-RC3 available for testing
- Previous by Thread: Re: [isabelle] Linear Arithmetic Split Limit Exceeded
- Next by Thread: Re: [isabelle] Linear Arithmetic Split Limit Exceeded
- Cl-isabelle-users February 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list