[isabelle] Isabelle2011 Z3 issue

Hi all,

Isabelle2011's Sledgehammer invokes Z3 by default in addition to Vampire & Co., which is nice because it often finds proofs that are outside the ATPs' reach. Unfortunately, we just found that for some theories, the Z3 problem preparation last "forever" and uses a lot of CPU.

So if you notice that after calling Sledgehammer you get no report from "z3" or "remote_z3" and the "poly" process takes 100% CPU, you might be a victim of this problem. Workaround: Decrease the monomorphization limit by adding

   declare [[smt_monomorph_limit = 2]]

or even "= 1" at the beginning of your theory (or in an included theory), or disable Z3 by adding

   sledgehammer_params [provers = e spass remote_vampire remote_sine_e]

(or whatever values make sense to you). Invoking Sledgehammer in synchronous mode, using

   sledgehammer [blocking]

or (to change the default)

   sledgehammer_params [blocking]

should also do the trick.

I'm sorry for the trouble caused by this issue. Strangely enough, we never had any problems with the 1500 goals from nine theories we used for testing, including the largish Jinja.

If you work with the repository version, expect a fix in the coming days.



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