[isabelle] Isabelle2011 Z3 issue
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
or (to change the default)
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